Let x0 of type ι be given.

Let x1 of type ο be given.

Assume H1: RealsStruct_Q x0 ⊆ field0 x0 ⟶ (∀ x2 . x2 ∈ RealsStruct_Q x0 ⟶ ∀ x3 : ο . (x2 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ RealsStruct_Z x0 ⟶ ∀ x5 . x5 ∈ RealsStruct_Npos x0 ⟶ field2b x0 x5 x2 = x4 ⟶ x3) ⟶ x3) ⟶ (∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Z x0 ⟶ ∀ x4 . x4 ∈ RealsStruct_Npos x0 ⟶ field2b x0 x4 x2 = x3 ⟶ x2 ∈ RealsStruct_Q x0) ⟶ x1.

Apply explicit_OrderedField_Q_props with field0 x0, field4 x0, RealsStruct_one x0, field1b x0, field2b x0, RealsStruct_leq x0, x1 leaving 2 subgoals.

Apply explicit_OrderedField_of_RealsStruct with x0.

The subproof is completed by applying H0.

Apply unknownprop_61f0c5d21af7f4f8b3f1e5a3770aff1383293d12248b741378bc8934dec531c5 with x0, λ x2 x3 . x2 ⊆ field0 x0 ⟶ (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 : ο . (x4 ∈ field0 x0 ⟶ ∀ x6 . x6 ∈ {x7 ∈ field0 x0|or (or (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x7 ∈ RealsStruct_Npos x0) (x7 = field4 x0)) (x7 ∈ RealsStruct_Npos x0)} ⟶ ∀ x7 . x7 ∈ RealsStruct_Npos x0 ⟶ field2b x0 x7 x4 = x6 ⟶ x5) ⟶ x5) ⟶ (∀ x4 . x4 ∈ field0 x0 ⟶ ∀ x5 . x5 ∈ {x6 ∈ field0 x0|or (or (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x6 ∈ RealsStruct_Npos x0) (x6 = field4 x0)) (x6 ∈ RealsStruct_Npos x0)} ⟶ ∀ x6 . x6 ∈ RealsStruct_Npos x0 ⟶ field2b x0 x6 x4 = x5 ⟶ x4 ∈ x2) ⟶ x1 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply unknownprop_87925c67a03b35d7e2b95672013636ce0205b3bb767f5d1c0c78f69cadaeb3e9 with x0, λ x2 x3 . RealsStruct_Q x0 ⊆ field0 x0 ⟶ (∀ x4 . x4 ∈ RealsStruct_Q x0 ⟶ ∀ x5 : ο . (x4 ∈ field0 x0 ⟶ ∀ x6 . x6 ∈ x2 ⟶ ∀ x7 . x7 ∈ RealsStruct_Npos x0 ⟶ field2b x0 x7 x4 = x6 ⟶ x5) ⟶ x5) ⟶ (∀ x4 . x4 ∈ field0 x0 ⟶ ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ RealsStruct_Npos x0 ⟶ field2b x0 x6 x4 = x5 ⟶ x4 ∈ RealsStruct_Q x0) ⟶ x1 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

■

Proofgold Proof