Let i, m, j and n be given.
Assume Hi2 HmO Hj2 HnO Hcmp.
We will prove order_rel (setprod 2 ω) (i,m) (j,n).
We will prove (setprod 2 ω = R ∧ Rlt (i,m) (j,n)) ∨ (setprod 2 ω = rational_numbers ∧ Rlt (i,m) (j,n)) ∨ (setprod 2 ω = ω ∧ (i,m) ∈ (j,n)) ∨ (setprod 2 ω = ω ∖ {0} ∧ (i,m) ∈ (j,n)) ∨ (setprod 2 ω = setprod 2 ω ∧ ∃i0 m0 j0 n0 : set, i0 ∈ 2 ∧ m0 ∈ ω ∧ j0 ∈ 2 ∧ n0 ∈ ω ∧ (i,m) = (i0,m0) ∧ (j,n) = (j0,n0) ∧ (i0 ∈ j0 ∨ (i0 = j0 ∧ m0 ∈ n0))) ∨ (setprod 2 ω = setprod R R ∧ ∃a1 a2 b1 b2 : set, (i,m) = (a1,a2) ∧ (j,n) = (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 ∧ (i,m) ∈ (j,n)).
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 ω ∧ ∃i0 m0 j0 n0 : set, i0 ∈ 2 ∧ m0 ∈ ω ∧ j0 ∈ 2 ∧ n0 ∈ ω ∧ (i,m) = (i0,m0) ∧ (j,n) = (j0,n0) ∧ (i0 ∈ j0 ∨ (i0 = j0 ∧ m0 ∈ n0)).
Apply andI to the current goal.
Use reflexivity.
We use i to witness the existential quantifier.
We use m to witness the existential quantifier.
We use j to witness the existential quantifier.
We use n to witness the existential quantifier.
Apply and7I to the current goal.
An exact proof term for the current goal is Hi2.
An exact proof term for the current goal is HmO.
An exact proof term for the current goal is Hj2.
An exact proof term for the current goal is HnO.
Use reflexivity.
Use reflexivity.
An exact proof term for the current goal is Hcmp.
∎