Assume H0: ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_Reals x0 x1 x2 x3 x4 x5 ⟶ equip omega {x6 ∈ x0|c3146.. x0 x1 x2 x3 x4 x5 x6}.

Claim L1: equip omega {x0 ∈ real|c3146.. real 0 1 add_SNo mul_SNo SNoLe x0}

Apply H0 with real, 0, 1, add_SNo, mul_SNo, SNoLe.

The subproof is completed by applying explicit_Reals_real.

Claim L2: {x0 ∈ real|c3146.. real 0 1 add_SNo mul_SNo SNoLe x0} = real

Apply unknownprop_9008f8f2ade63c16b95ce9874af844e7e3d8eff775b1a6fdc91615ef20cc18c1 with real, 0, 1, add_SNo, mul_SNo, SNoLe.

The subproof is completed by applying explicit_OrderedField_real.

Apply real_uncountable.

Apply L2 with λ x0 x1 . equip omega x0.

The subproof is completed by applying L1.

■

Proofgold Proof