Let a and b be given.
Assume Hab: order_rel (ω ∖ {0}) a b.
We will prove a ∈ b.
Apply (Hab (a ∈ b)) to the current goal.
Assume Hleft6.
Apply (Hleft6 (a ∈ b)) to the current goal.
Assume Hleft.
Apply (Hleft (a ∈ b)) to the current goal.
Assume Hleft2.
Apply (Hleft2 (a ∈ b)) to the current goal.
Assume Hleft3.
Apply (Hleft3 (a ∈ b)) to the current goal.
Assume Hleft4.
Apply (Hleft4 (a ∈ b)) to the current goal.
Assume Hc1: ω ∖ {0} = R ∧ Rlt a b.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: ω ∖ {0} = R.
An exact proof term for the current goal is (andEL (ω ∖ {0} = R) (Rlt a b) Hc1).
We prove the intermediate claim HeqR: R = ω ∖ {0}.
Use symmetry.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (R_neq_omega_nonzero HeqR).
Assume Hc2: ω ∖ {0} = rational_numbers ∧ Rlt a b.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: ω ∖ {0} = rational_numbers.
An exact proof term for the current goal is (andEL (ω ∖ {0} = rational_numbers) (Rlt a b) Hc2).
We prove the intermediate claim HeqQ: rational_numbers = ω ∖ {0}.
Use symmetry.
An exact proof term for the current goal is Heq.
We prove the intermediate claim H0Q: 0 ∈ rational_numbers.
We will prove 0 ∈ rational.
We prove the intermediate claim H0real: 0 ∈ real.
An exact proof term for the current goal is real_0.
We prove the intermediate claim H0omega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim H0int: 0 ∈ int.
An exact proof term for the current goal is (Subq_omega_int 0 H0omega).
We prove the intermediate claim H1omega: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim H1not0: 1 ∉ {0}.
Assume H1: 1 ∈ {0}.
We will prove False.
We prove the intermediate claim Heq10: 1 = 0.
An exact proof term for the current goal is (SingE 0 1 H1).
An exact proof term for the current goal is (neq_1_0 Heq10).
We prove the intermediate claim H1nonzero: 1 ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} 1 H1omega H1not0).
We prove the intermediate claim Heq0: 0 = div_SNo 0 1.
We prove the intermediate claim Hdiv: div_SNo 0 1 = 0.
An exact proof term for the current goal is (div_SNo_0_num 1 SNo_1).
rewrite the current goal using Hdiv (from right to left) at position 1.
Use reflexivity.
We prove the intermediate claim Hex: ∃m ∈ int, ∃n ∈ ω ∖ {0}, 0 = div_SNo m n.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H0int.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H1nonzero.
An exact proof term for the current goal is Heq0.
An exact proof term for the current goal is (SepI real (λx : set ⇒ ∃m ∈ int, ∃n ∈ ω ∖ {0}, x = div_SNo m n) 0 H0real Hex).
We prove the intermediate claim H0NZ: 0 ∈ ω ∖ {0}.
rewrite the current goal using HeqQ (from right to left) at position 1.
An exact proof term for the current goal is H0Q.
We prove the intermediate claim H0not0: 0 ∉ {0}.
An exact proof term for the current goal is (setminusE2 ω {0} 0 H0NZ).
An exact proof term for the current goal is (H0not0 (SingI 0)).
Assume Hc3: ω ∖ {0} = ω ∧ a ∈ b.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: ω ∖ {0} = ω.
An exact proof term for the current goal is (andEL (ω ∖ {0} = ω) (a ∈ b) Hc3).
We prove the intermediate claim H0omega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim H0NZ: 0 ∈ ω ∖ {0}.
rewrite the current goal using Heq (from left to right) at position 1.
An exact proof term for the current goal is H0omega.
We prove the intermediate claim H0not0: 0 ∉ {0}.
An exact proof term for the current goal is (setminusE2 ω {0} 0 H0NZ).
An exact proof term for the current goal is (H0not0 (SingI 0)).
Assume Hc4: ω ∖ {0} = ω ∖ {0} ∧ a ∈ b.
An exact proof term for the current goal is (andER (ω ∖ {0} = ω ∖ {0}) (a ∈ b) Hc4).
Assume Hc5: ω ∖ {0} = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n)).
Apply FalseE to the current goal.
We prove the intermediate claim Heq: ω ∖ {0} = setprod 2 ω.
An exact proof term for the current goal is (andEL (ω ∖ {0} = setprod 2 ω) (∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) Hc5).
We prove the intermediate claim Heq2: setprod 2 ω = ω ∖ {0}.
Use symmetry.
An exact proof term for the current goal is Heq.
We prove the intermediate claim H1omega: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim Hp: (0,1) ∈ setprod 2 ω.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 0 1 In_0_2 H1omega).
We prove the intermediate claim HpNZ: (0,1) ∈ ω ∖ {0}.
rewrite the current goal using Heq2 (from right to left) at position 1.
An exact proof term for the current goal is Hp.
We prove the intermediate claim Hcore: (0,1) ∈ ω ∧ (0,1) ∉ {0}.
An exact proof term for the current goal is (setminusE ω {0} (0,1) HpNZ).
We prove the intermediate claim HpOmega: (0,1) ∈ ω.
An exact proof term for the current goal is (andEL ((0,1) ∈ ω) ((0,1) ∉ {0}) Hcore).
We prove the intermediate claim HSingOmega: {1} ∈ ω.
rewrite the current goal using tuple_0_1_eq_Sing1 (from right to left).
An exact proof term for the current goal is HpOmega.
We prove the intermediate claim HnotTr: ¬ TransSet {1}.
Assume Htr: TransSet {1}.
We will prove False.
We prove the intermediate claim H1inSing1: 1 ∈ {1}.
An exact proof term for the current goal is (SingI 1).
We prove the intermediate claim Hsub: 1 ⊆ {1}.
An exact proof term for the current goal is (Htr 1 H1inSing1).
We prove the intermediate claim H0in1: 0 ∈ 1.
rewrite the current goal using eq_1_Sing0 (from left to right) at position 1.
An exact proof term for the current goal is (SingI 0).
We prove the intermediate claim H0inSing1: 0 ∈ {1}.
An exact proof term for the current goal is (Hsub 0 H0in1).
We prove the intermediate claim Heq01: 0 = 1.
An exact proof term for the current goal is (SingE 1 0 H0inSing1).
An exact proof term for the current goal is (neq_0_1 Heq01).
We prove the intermediate claim HnotInOmega: {1} ∉ ω.
Assume HSing: {1} ∈ ω.
We will prove False.
We prove the intermediate claim Hnat: nat_p {1}.
An exact proof term for the current goal is (omega_nat_p {1} HSing).
We prove the intermediate claim Hord: ordinal {1}.
An exact proof term for the current goal is (nat_p_ordinal {1} Hnat).
We prove the intermediate claim Htr: TransSet {1}.
An exact proof term for the current goal is (ordinal_TransSet {1} Hord).
An exact proof term for the current goal is (HnotTr Htr).
An exact proof term for the current goal is (HnotInOmega HSingOmega).
Assume Hc6: ω ∖ {0} = setprod R R ∧ ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).
Apply FalseE to the current goal.
We prove the intermediate claim Heq: ω ∖ {0} = setprod R R.
An exact proof term for the current goal is (andEL (ω ∖ {0} = setprod R R) (∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) Hc6).
We prove the intermediate claim HeqRR: setprod R R = ω ∖ {0}.
Use symmetry.
An exact proof term for the current goal is Heq.
We prove the intermediate claim HpRR: (0,1) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R 0 1 real_0 real_1).
We prove the intermediate claim HpNZ: (0,1) ∈ ω ∖ {0}.
rewrite the current goal using HeqRR (from right to left) at position 1.
An exact proof term for the current goal is HpRR.
We prove the intermediate claim Hcore: (0,1) ∈ ω ∧ (0,1) ∉ {0}.
An exact proof term for the current goal is (setminusE ω {0} (0,1) HpNZ).
We prove the intermediate claim HpOmega: (0,1) ∈ ω.
An exact proof term for the current goal is (andEL ((0,1) ∈ ω) ((0,1) ∉ {0}) Hcore).
We prove the intermediate claim HSingOmega: {1} ∈ ω.
rewrite the current goal using tuple_0_1_eq_Sing1 (from right to left).
An exact proof term for the current goal is HpOmega.
We prove the intermediate claim HnotTr: ¬ TransSet {1}.
Assume Htr: TransSet {1}.
We will prove False.
We prove the intermediate claim H1inSing1: 1 ∈ {1}.
An exact proof term for the current goal is (SingI 1).
We prove the intermediate claim Hsub: 1 ⊆ {1}.
An exact proof term for the current goal is (Htr 1 H1inSing1).
We prove the intermediate claim H0in1: 0 ∈ 1.
rewrite the current goal using eq_1_Sing0 (from left to right) at position 1.
An exact proof term for the current goal is (SingI 0).
We prove the intermediate claim H0inSing1: 0 ∈ {1}.
An exact proof term for the current goal is (Hsub 0 H0in1).
We prove the intermediate claim Heq01: 0 = 1.
An exact proof term for the current goal is (SingE 1 0 H0inSing1).
An exact proof term for the current goal is (neq_0_1 Heq01).
We prove the intermediate claim HnotInOmega: {1} ∉ ω.
Assume HSing: {1} ∈ ω.
We will prove False.
We prove the intermediate claim Hnat: nat_p {1}.
An exact proof term for the current goal is (omega_nat_p {1} HSing).
We prove the intermediate claim Hord: ordinal {1}.
An exact proof term for the current goal is (nat_p_ordinal {1} Hnat).
We prove the intermediate claim Htr: TransSet {1}.
An exact proof term for the current goal is (ordinal_TransSet {1} Hord).
An exact proof term for the current goal is (HnotTr Htr).
An exact proof term for the current goal is (HnotInOmega HSingOmega).
Assume Hord: ordinal (ω ∖ {0}) ∧ (ω ∖ {0}) ≠ R ∧ (ω ∖ {0}) ≠ rational_numbers ∧ (ω ∖ {0}) ≠ setprod 2 ω ∧ (ω ∖ {0}) ≠ setprod R R ∧ a ∈ b.
Set T to be the term ((((ordinal (ω ∖ {0}) ∧ (ω ∖ {0}) ≠ R) ∧ (ω ∖ {0}) ≠ rational_numbers) ∧ (ω ∖ {0}) ≠ setprod 2 ω) ∧ (ω ∖ {0}) ≠ setprod R R).
An exact proof term for the current goal is (andER T (a ∈ b) Hord).
∎