We will prove order_rel (setprod 2 ω) (0,0) (1,0).
We will prove (setprod 2 ω = R ∧ Rlt (0,0) (1,0)) ∨ (setprod 2 ω = rational_numbers ∧ Rlt (0,0) (1,0)) ∨ (setprod 2 ω = ω ∧ (0,0) ∈ (1,0)) ∨ (setprod 2 ω = ω ∖ {0} ∧ (0,0) ∈ (1,0)) ∨ (setprod 2 ω = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ (0,0) = (i,m) ∧ (1,0) = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) ∨ (setprod 2 ω = setprod R R ∧ ∃a1 a2 b1 b2 : set, (0,0) = (a1,a2) ∧ (1,0) = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) ∨ (ordinal (setprod 2 ω) ∧ setprod 2 ω ≠ R ∧ setprod 2 ω ≠ rational_numbers ∧ setprod 2 ω ≠ setprod 2 ω ∧ setprod 2 ω ≠ setprod R R ∧ (0,0) ∈ (1,0)).
Apply orIL to the current goal.
Apply orIL to the current goal.
Apply orIR to the current goal.
We will prove setprod 2 ω = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ (0,0) = (i,m) ∧ (1,0) = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n)).
Apply andI to the current goal.
Use reflexivity.
We use 0 to witness the existential quantifier.
We use 0 to witness the existential quantifier.
We use 1 to witness the existential quantifier.
We use 0 to witness the existential quantifier.
We prove the intermediate claim Hm0: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim Heq00: (0,0) = (0,0).
Use reflexivity.
We prove the intermediate claim Heq10: (1,0) = (1,0).
Use reflexivity.
We prove the intermediate claim H12: 0 ∈ 2 ∧ 0 ∈ ω.
An exact proof term for the current goal is (andI (0 ∈ 2) (0 ∈ ω) In_0_2 Hm0).
We prove the intermediate claim H123: (0 ∈ 2 ∧ 0 ∈ ω) ∧ 1 ∈ 2.
An exact proof term for the current goal is (andI (0 ∈ 2 ∧ 0 ∈ ω) (1 ∈ 2) H12 In_1_2).
We prove the intermediate claim H1234: ((0 ∈ 2 ∧ 0 ∈ ω) ∧ 1 ∈ 2) ∧ 0 ∈ ω.
An exact proof term for the current goal is (andI ((0 ∈ 2 ∧ 0 ∈ ω) ∧ 1 ∈ 2) (0 ∈ ω) H123 Hm0).
We prove the intermediate claim H12345: (((0 ∈ 2 ∧ 0 ∈ ω) ∧ 1 ∈ 2) ∧ 0 ∈ ω) ∧ (0,0) = (0,0).
An exact proof term for the current goal is (andI (((0 ∈ 2 ∧ 0 ∈ ω) ∧ 1 ∈ 2) ∧ 0 ∈ ω) ((0,0) = (0,0)) H1234 Heq00).
We prove the intermediate claim H123456: ((((0 ∈ 2 ∧ 0 ∈ ω) ∧ 1 ∈ 2) ∧ 0 ∈ ω) ∧ (0,0) = (0,0)) ∧ (1,0) = (1,0).
An exact proof term for the current goal is (andI ((((0 ∈ 2 ∧ 0 ∈ ω) ∧ 1 ∈ 2) ∧ 0 ∈ ω) ∧ (0,0) = (0,0)) ((1,0) = (1,0)) H12345 Heq10).
We prove the intermediate claim Hlex: 0 ∈ 1 ∨ (0 = 1 ∧ 0 ∈ 0).
An exact proof term for the current goal is (orIL (0 ∈ 1) (0 = 1 ∧ 0 ∈ 0) In_0_1).
Apply andI to the current goal.
An exact proof term for the current goal is H123456.
An exact proof term for the current goal is Hlex.
∎