Metamath Proof Explorer

Theorem rrx2plordisom

Description: The set of points in the two dimensional Euclidean plane with the lexicographical ordering is isomorphic to the cartesian product of the real numbers with the lexicographical ordering implied by the ordering of the real numbers. (Contributed by AV, 12-Mar-2023)

Ref Expression
Hypotheses rrx2plord.o ⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) }
rrx2plord2.r ⊢ 𝑅 = ( ℝ ↑m { 1 , 2 } )
rrx2plordisom.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } )
rrx2plordisom.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) }
Assertion rrx2plordisom 𝐹 Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 )

Proof

Step Hyp Ref Expression
1 rrx2plord.o ⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) }
2 rrx2plord2.r ⊢ 𝑅 = ( ℝ ↑m { 1 , 2 } )
3 rrx2plordisom.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } )
4 rrx2plordisom.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) }
5 eqid ⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } )
6 2 5 rrx2xpref1o ⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) : ( ℝ × ℝ ) –1-1-onto→ 𝑅
7 elxpi ⊢ ( 𝑎 ∈ ( ℝ × ℝ ) → ∃ 𝑐 ∃ 𝑑 ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) )
8 elxpi ⊢ ( 𝑏 ∈ ( ℝ × ℝ ) → ∃ 𝑒 ∃ 𝑓 ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) )
9 df-br ⊢ ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } )
10 opelxpi ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ℝ × ℝ ) )
11 10 adantl ⊢ ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ℝ × ℝ ) )
12 eleq1 ⊢ ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑎 ∈ ( ℝ × ℝ ) ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ℝ × ℝ ) ) )
13 12 adantr ⊢ ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 𝑎 ∈ ( ℝ × ℝ ) ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ ( ℝ × ℝ ) ) )
14 11 13 mpbird ⊢ ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → 𝑎 ∈ ( ℝ × ℝ ) )
15 opelxpi ⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → ⟨ 𝑒 , 𝑓 ⟩ ∈ ( ℝ × ℝ ) )
16 15 adantl ⊢ ( ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ⟨ 𝑒 , 𝑓 ⟩ ∈ ( ℝ × ℝ ) )
17 eleq1 ⊢ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ → ( 𝑏 ∈ ( ℝ × ℝ ) ↔ ⟨ 𝑒 , 𝑓 ⟩ ∈ ( ℝ × ℝ ) ) )
18 17 adantr ⊢ ( ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ( 𝑏 ∈ ( ℝ × ℝ ) ↔ ⟨ 𝑒 , 𝑓 ⟩ ∈ ( ℝ × ℝ ) ) )
19 16 18 mpbird ⊢ ( ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → 𝑏 ∈ ( ℝ × ℝ ) )
20 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑎 ) )
21 fveq2 ⊢ ( 𝑦 = 𝑏 → ( 1st ‘ 𝑦 ) = ( 1st ‘ 𝑏 ) )
22 20 21 breqan12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ↔ ( 1st ‘ 𝑎 ) < ( 1st ‘ 𝑏 ) ) )
23 20 21 eqeqan12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ↔ ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ) )
24 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑎 ) )
25 fveq2 ⊢ ( 𝑦 = 𝑏 → ( 2nd ‘ 𝑦 ) = ( 2nd ‘ 𝑏 ) )
26 24 25 breqan12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ↔ ( 2nd ‘ 𝑎 ) < ( 2nd ‘ 𝑏 ) ) )
27 23 26 anbi12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ↔ ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) < ( 2nd ‘ 𝑏 ) ) ) )
28 22 27 orbi12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ↔ ( ( 1st ‘ 𝑎 ) < ( 1st ‘ 𝑏 ) ∨ ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) < ( 2nd ‘ 𝑏 ) ) ) ) )
29 28 opelopab2a ⊢ ( ( 𝑎 ∈ ( ℝ × ℝ ) ∧ 𝑏 ∈ ( ℝ × ℝ ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } ↔ ( ( 1st ‘ 𝑎 ) < ( 1st ‘ 𝑏 ) ∨ ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) < ( 2nd ‘ 𝑏 ) ) ) ) )
30 14 19 29 syl2an ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } ↔ ( ( 1st ‘ 𝑎 ) < ( 1st ‘ 𝑏 ) ∨ ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) < ( 2nd ‘ 𝑏 ) ) ) ) )
31 9 30 syl5bb ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 1st ‘ 𝑎 ) < ( 1st ‘ 𝑏 ) ∨ ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) < ( 2nd ‘ 𝑏 ) ) ) ) )
32 1ne2 ⊢ 1 ≠ 2
33 1ex ⊢ 1 ∈ V
34 vex ⊢ 𝑐 ∈ V
35 33 34 fvpr1 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 1 ) = 𝑐 )
36 32 35 mp1i ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 1 ) = 𝑐 )
37 vex ⊢ 𝑒 ∈ V
38 33 37 fvpr1 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 1 ) = 𝑒 )
39 32 38 mp1i ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 1 ) = 𝑒 )
40 36 39 breq12d ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 1 ) < ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 1 ) ↔ 𝑐 < 𝑒 ) )
41 36 39 eqeq12d ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 1 ) = ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 1 ) ↔ 𝑐 = 𝑒 ) )
42 2ex ⊢ 2 ∈ V
43 vex ⊢ 𝑑 ∈ V
44 42 43 fvpr2 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 2 ) = 𝑑 )
45 32 44 mp1i ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 2 ) = 𝑑 )
46 vex ⊢ 𝑓 ∈ V
47 42 46 fvpr2 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 2 ) = 𝑓 )
48 32 47 mp1i ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 2 ) = 𝑓 )
49 45 48 breq12d ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 2 ) < ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 2 ) ↔ 𝑑 < 𝑓 ) )
50 41 49 anbi12d ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 1 ) = ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 1 ) ∧ ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 2 ) < ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 2 ) ) ↔ ( 𝑐 = 𝑒 ∧ 𝑑 < 𝑓 ) ) )
51 40 50 orbi12d ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 1 ) < ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 1 ) ∨ ( ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 1 ) = ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 1 ) ∧ ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 2 ) < ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 2 ) ) ) ↔ ( 𝑐 < 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 < 𝑓 ) ) ) )
52 eqid ⊢ { 1 , 2 } = { 1 , 2 }
53 52 2 prelrrx2 ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ∈ 𝑅 )
54 53 adantl ⊢ ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ∈ 𝑅 )
55 52 2 prelrrx2 ⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ∈ 𝑅 )
56 55 adantl ⊢ ( ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ∈ 𝑅 )
57 1 rrx2plord ⊢ ( ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ∈ 𝑅 ∧ { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ∈ 𝑅 ) → ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } 𝑂 { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ↔ ( ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 1 ) < ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 1 ) ∨ ( ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 1 ) = ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 1 ) ∧ ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 2 ) < ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 2 ) ) ) ) )
58 54 56 57 syl2an ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } 𝑂 { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ↔ ( ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 1 ) < ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 1 ) ∨ ( ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 1 ) = ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 1 ) ∧ ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ‘ 2 ) < ( { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ‘ 2 ) ) ) ) )
59 34 43 op1std ⊢ ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ → ( 1st ‘ 𝑎 ) = 𝑐 )
60 59 adantr ⊢ ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 1st ‘ 𝑎 ) = 𝑐 )
61 37 46 op1std ⊢ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ → ( 1st ‘ 𝑏 ) = 𝑒 )
62 61 adantr ⊢ ( ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ( 1st ‘ 𝑏 ) = 𝑒 )
63 60 62 breqan12d ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( 1st ‘ 𝑎 ) < ( 1st ‘ 𝑏 ) ↔ 𝑐 < 𝑒 ) )
64 60 62 eqeqan12d ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ↔ 𝑐 = 𝑒 ) )
65 34 43 op2ndd ⊢ ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ → ( 2nd ‘ 𝑎 ) = 𝑑 )
66 65 adantr ⊢ ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 2nd ‘ 𝑎 ) = 𝑑 )
67 37 46 op2ndd ⊢ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ → ( 2nd ‘ 𝑏 ) = 𝑓 )
68 67 adantr ⊢ ( ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ( 2nd ‘ 𝑏 ) = 𝑓 )
69 66 68 breqan12d ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( 2nd ‘ 𝑎 ) < ( 2nd ‘ 𝑏 ) ↔ 𝑑 < 𝑓 ) )
70 64 69 anbi12d ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) < ( 2nd ‘ 𝑏 ) ) ↔ ( 𝑐 = 𝑒 ∧ 𝑑 < 𝑓 ) ) )
71 63 70 orbi12d ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( ( 1st ‘ 𝑎 ) < ( 1st ‘ 𝑏 ) ∨ ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) < ( 2nd ‘ 𝑏 ) ) ) ↔ ( 𝑐 < 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 < 𝑓 ) ) ) )
72 51 58 71 3bitr4rd ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( ( 1st ‘ 𝑎 ) < ( 1st ‘ 𝑏 ) ∨ ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) < ( 2nd ‘ 𝑏 ) ) ) ↔ { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } 𝑂 { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ) )
73 fveq2 ⊢ ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑎 ) = ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ ⟨ 𝑐 , 𝑑 ⟩ ) )
74 df-ov ⊢ ( 𝑐 ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) 𝑑 ) = ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ ⟨ 𝑐 , 𝑑 ⟩ )
75 73 74 eqtr4di ⊢ ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑎 ) = ( 𝑐 ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) 𝑑 ) )
76 eqidd ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) )
77 opeq2 ⊢ ( 𝑥 = 𝑐 → ⟨ 1 , 𝑥 ⟩ = ⟨ 1 , 𝑐 ⟩ )
78 77 adantr ⊢ ( ( 𝑥 = 𝑐 ∧ 𝑦 = 𝑑 ) → ⟨ 1 , 𝑥 ⟩ = ⟨ 1 , 𝑐 ⟩ )
79 opeq2 ⊢ ( 𝑦 = 𝑑 → ⟨ 2 , 𝑦 ⟩ = ⟨ 2 , 𝑑 ⟩ )
80 79 adantl ⊢ ( ( 𝑥 = 𝑐 ∧ 𝑦 = 𝑑 ) → ⟨ 2 , 𝑦 ⟩ = ⟨ 2 , 𝑑 ⟩ )
81 78 80 preq12d ⊢ ( ( 𝑥 = 𝑐 ∧ 𝑦 = 𝑑 ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } = { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } )
82 81 adantl ⊢ ( ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ∧ ( 𝑥 = 𝑐 ∧ 𝑦 = 𝑑 ) ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } = { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } )
83 simpl ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → 𝑐 ∈ ℝ )
84 simpr ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → 𝑑 ∈ ℝ )
85 prex ⊢ { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ∈ V
86 85 a1i ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } ∈ V )
87 76 82 83 84 86 ovmpod ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( 𝑐 ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) 𝑑 ) = { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } )
88 75 87 sylan9eq ⊢ ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑎 ) = { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } )
89 88 eqcomd ⊢ ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } = ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑎 ) )
90 fveq2 ⊢ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑏 ) = ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ ⟨ 𝑒 , 𝑓 ⟩ ) )
91 df-ov ⊢ ( 𝑒 ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) 𝑓 ) = ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ ⟨ 𝑒 , 𝑓 ⟩ )
92 90 91 eqtr4di ⊢ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑏 ) = ( 𝑒 ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) 𝑓 ) )
93 eqidd ⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) )
94 opeq2 ⊢ ( 𝑥 = 𝑒 → ⟨ 1 , 𝑥 ⟩ = ⟨ 1 , 𝑒 ⟩ )
95 94 adantr ⊢ ( ( 𝑥 = 𝑒 ∧ 𝑦 = 𝑓 ) → ⟨ 1 , 𝑥 ⟩ = ⟨ 1 , 𝑒 ⟩ )
96 opeq2 ⊢ ( 𝑦 = 𝑓 → ⟨ 2 , 𝑦 ⟩ = ⟨ 2 , 𝑓 ⟩ )
97 96 adantl ⊢ ( ( 𝑥 = 𝑒 ∧ 𝑦 = 𝑓 ) → ⟨ 2 , 𝑦 ⟩ = ⟨ 2 , 𝑓 ⟩ )
98 95 97 preq12d ⊢ ( ( 𝑥 = 𝑒 ∧ 𝑦 = 𝑓 ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } = { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } )
99 98 adantl ⊢ ( ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ∧ ( 𝑥 = 𝑒 ∧ 𝑦 = 𝑓 ) ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } = { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } )
100 simpl ⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → 𝑒 ∈ ℝ )
101 simpr ⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → 𝑓 ∈ ℝ )
102 prex ⊢ { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ∈ V
103 102 a1i ⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ∈ V )
104 93 99 100 101 103 ovmpod ⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → ( 𝑒 ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) 𝑓 ) = { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } )
105 92 104 sylan9eq ⊢ ( ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑏 ) = { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } )
106 105 eqcomd ⊢ ( ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } = ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑏 ) )
107 89 106 breqan12d ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( { ⟨ 1 , 𝑐 ⟩ , ⟨ 2 , 𝑑 ⟩ } 𝑂 { ⟨ 1 , 𝑒 ⟩ , ⟨ 2 , 𝑓 ⟩ } ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑏 ) ) )
108 31 72 107 3bitrd ⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑏 ) ) )
109 108 expcom ⊢ ( ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑏 ) ) ) )
110 109 exlimivv ⊢ ( ∃ 𝑒 ∃ 𝑓 ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑏 ) ) ) )
111 110 com12 ⊢ ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ∃ 𝑒 ∃ 𝑓 ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑏 ) ) ) )
112 111 exlimivv ⊢ ( ∃ 𝑐 ∃ 𝑑 ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ∃ 𝑒 ∃ 𝑓 ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑏 ) ) ) )
113 112 imp ⊢ ( ( ∃ 𝑐 ∃ 𝑑 ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ∃ 𝑒 ∃ 𝑓 ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑏 ) ) )
114 7 8 113 syl2an ⊢ ( ( 𝑎 ∈ ( ℝ × ℝ ) ∧ 𝑏 ∈ ( ℝ × ℝ ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑏 ) ) )
115 114 rgen2 ⊢ ∀ 𝑎 ∈ ( ℝ × ℝ ) ∀ 𝑏 ∈ ( ℝ × ℝ ) ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑏 ) )
116 df-isom ⊢ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) Isom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) : ( ℝ × ℝ ) –1-1-onto→ 𝑅 ∧ ∀ 𝑎 ∈ ( ℝ × ℝ ) ∀ 𝑏 ∈ ( ℝ × ℝ ) ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) ‘ 𝑏 ) ) ) )
117 6 115 116 mpbir2an ⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) Isom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } , 𝑂 ( ( ℝ × ℝ ) , 𝑅 )
118 isoeq2 ⊢ ( 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) ↔ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) Isom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) ) )
119 4 118 ax-mp ⊢ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) ↔ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) Isom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) )
120 117 119 mpbir ⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 )
121 isoeq1 ⊢ ( 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) → ( 𝐹 Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) ↔ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) ) )
122 3 121 ax-mp ⊢ ( 𝐹 Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) ↔ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ { ⟨ 1 , 𝑥 ⟩ , ⟨ 2 , 𝑦 ⟩ } ) Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) )
123 120 122 mpbir ⊢ 𝐹 Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 )