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	⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ∧ ( ( 𝑥 ‘ 0 ) < ( 𝑦 ‘ 0 ) ∨ ( ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ∧ ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ) ) ) }
	rrx2plord2.r	⊢ 𝑅 = ( ℝ ↑m ( 0 ..^ 2 ) )
	rrx2plordisom.f	⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ )
	rrx2plordisom.t	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) }
Assertion	rrx2plordisom	⊢ 𝐹 Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		rrx2plord.o	⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ∧ ( ( 𝑥 ‘ 0 ) < ( 𝑦 ‘ 0 ) ∨ ( ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ∧ ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ) ) ) }
2		rrx2plord2.r	⊢ 𝑅 = ( ℝ ↑m ( 0 ..^ 2 ) )
3		rrx2plordisom.f	⊢ 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ )
4		rrx2plordisom.t	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) }
5		eqid	⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ )
6	2 5	rrx2xpref1o	⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) : ( ℝ × ℝ ) –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	bitrid	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 1st ‘ 𝑎 ) < ( 1st ‘ 𝑏 ) ∨ ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) < ( 2nd ‘ 𝑏 ) ) ) ) )
32		vex	⊢ 𝑐 ∈ V
33		s2fv0	⊢ ( 𝑐 ∈ V → ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 0 ) = 𝑐 )
34	32 33	mp1i	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 0 ) = 𝑐 )
35		vex	⊢ 𝑒 ∈ V
36		s2fv0	⊢ ( 𝑒 ∈ V → ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 0 ) = 𝑒 )
37	35 36	mp1i	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 0 ) = 𝑒 )
38	34 37	breq12d	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 0 ) < ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 0 ) ↔ 𝑐 < 𝑒 ) )
39	34 37	eqeq12d	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 0 ) = ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 0 ) ↔ 𝑐 = 𝑒 ) )
40		vex	⊢ 𝑑 ∈ V
41		s2fv1	⊢ ( 𝑑 ∈ V → ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 1 ) = 𝑑 )
42	40 41	mp1i	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 1 ) = 𝑑 )
43		vex	⊢ 𝑓 ∈ V
44		s2fv1	⊢ ( 𝑓 ∈ V → ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 1 ) = 𝑓 )
45	43 44	mp1i	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 1 ) = 𝑓 )
46	42 45	breq12d	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 1 ) < ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 1 ) ↔ 𝑑 < 𝑓 ) )
47	39 46	anbi12d	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 0 ) = ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 0 ) ∧ ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 1 ) < ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 1 ) ) ↔ ( 𝑐 = 𝑒 ∧ 𝑑 < 𝑓 ) ) )
48	38 47	orbi12d	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 0 ) < ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 0 ) ∨ ( ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 0 ) = ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 0 ) ∧ ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 1 ) < ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 1 ) ) ) ↔ ( 𝑐 < 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 < 𝑓 ) ) ) )
49		eqid	⊢ ( 0 ..^ 2 ) = ( 0 ..^ 2 )
50	49 2	prelrrx2	⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ⟨“ 𝑐 𝑑 ”⟩ ∈ 𝑅 )
51	50	adantl	⊢ ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ⟨“ 𝑐 𝑑 ”⟩ ∈ 𝑅 )
52	49 2	prelrrx2	⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → ⟨“ 𝑒 𝑓 ”⟩ ∈ 𝑅 )
53	52	adantl	⊢ ( ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ⟨“ 𝑒 𝑓 ”⟩ ∈ 𝑅 )
54	1	rrx2plord	⊢ ( ( ⟨“ 𝑐 𝑑 ”⟩ ∈ 𝑅 ∧ ⟨“ 𝑒 𝑓 ”⟩ ∈ 𝑅 ) → ( ⟨“ 𝑐 𝑑 ”⟩ 𝑂 ⟨“ 𝑒 𝑓 ”⟩ ↔ ( ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 0 ) < ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 0 ) ∨ ( ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 0 ) = ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 0 ) ∧ ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 1 ) < ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 1 ) ) ) ) )
55	51 53 54	syl2an	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ⟨“ 𝑐 𝑑 ”⟩ 𝑂 ⟨“ 𝑒 𝑓 ”⟩ ↔ ( ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 0 ) < ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 0 ) ∨ ( ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 0 ) = ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 0 ) ∧ ( ⟨“ 𝑐 𝑑 ”⟩ ‘ 1 ) < ( ⟨“ 𝑒 𝑓 ”⟩ ‘ 1 ) ) ) ) )
56	32 40	op1std	⊢ ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ → ( 1st ‘ 𝑎 ) = 𝑐 )
57	56	adantr	⊢ ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 1st ‘ 𝑎 ) = 𝑐 )
58	35 43	op1std	⊢ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ → ( 1st ‘ 𝑏 ) = 𝑒 )
59	58	adantr	⊢ ( ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ( 1st ‘ 𝑏 ) = 𝑒 )
60	57 59	breqan12d	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( 1st ‘ 𝑎 ) < ( 1st ‘ 𝑏 ) ↔ 𝑐 < 𝑒 ) )
61	57 59	eqeqan12d	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ↔ 𝑐 = 𝑒 ) )
62	32 40	op2ndd	⊢ ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ → ( 2nd ‘ 𝑎 ) = 𝑑 )
63	62	adantr	⊢ ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 2nd ‘ 𝑎 ) = 𝑑 )
64	35 43	op2ndd	⊢ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ → ( 2nd ‘ 𝑏 ) = 𝑓 )
65	64	adantr	⊢ ( ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ( 2nd ‘ 𝑏 ) = 𝑓 )
66	63 65	breqan12d	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( 2nd ‘ 𝑎 ) < ( 2nd ‘ 𝑏 ) ↔ 𝑑 < 𝑓 ) )
67	61 66	anbi12d	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) < ( 2nd ‘ 𝑏 ) ) ↔ ( 𝑐 = 𝑒 ∧ 𝑑 < 𝑓 ) ) )
68	60 67	orbi12d	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( ( 1st ‘ 𝑎 ) < ( 1st ‘ 𝑏 ) ∨ ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) < ( 2nd ‘ 𝑏 ) ) ) ↔ ( 𝑐 < 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 < 𝑓 ) ) ) )
69	48 55 68	3bitr4rd	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ( ( 1st ‘ 𝑎 ) < ( 1st ‘ 𝑏 ) ∨ ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) < ( 2nd ‘ 𝑏 ) ) ) ↔ ⟨“ 𝑐 𝑑 ”⟩ 𝑂 ⟨“ 𝑒 𝑓 ”⟩ ) )
70		fveq2	⊢ ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑎 ) = ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ ⟨ 𝑐 , 𝑑 ⟩ ) )
71		df-ov	⊢ ( 𝑐 ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) 𝑑 ) = ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ ⟨ 𝑐 , 𝑑 ⟩ )
72	70 71	eqtr4di	⊢ ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑎 ) = ( 𝑐 ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) 𝑑 ) )
73		eqidd	⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) )
74		simprl	⊢ ( ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ∧ ( 𝑥 = 𝑐 ∧ 𝑦 = 𝑑 ) ) → 𝑥 = 𝑐 )
75		simprr	⊢ ( ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ∧ ( 𝑥 = 𝑐 ∧ 𝑦 = 𝑑 ) ) → 𝑦 = 𝑑 )
76	74 75	s2eqd	⊢ ( ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ∧ ( 𝑥 = 𝑐 ∧ 𝑦 = 𝑑 ) ) → ⟨“ 𝑥 𝑦 ”⟩ = ⟨“ 𝑐 𝑑 ”⟩ )
77		simpl	⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → 𝑐 ∈ ℝ )
78		simpr	⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → 𝑑 ∈ ℝ )
79	73 76 77 78 50	ovmpod	⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( 𝑐 ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) 𝑑 ) = ⟨“ 𝑐 𝑑 ”⟩ )
80	72 79	sylan9eq	⊢ ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑎 ) = ⟨“ 𝑐 𝑑 ”⟩ )
81	80	eqcomd	⊢ ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ⟨“ 𝑐 𝑑 ”⟩ = ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑎 ) )
82		fveq2	⊢ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑏 ) = ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ ⟨ 𝑒 , 𝑓 ⟩ ) )
83		df-ov	⊢ ( 𝑒 ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) 𝑓 ) = ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ ⟨ 𝑒 , 𝑓 ⟩ )
84	82 83	eqtr4di	⊢ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑏 ) = ( 𝑒 ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) 𝑓 ) )
85		eqidd	⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) )
86		simprl	⊢ ( ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ∧ ( 𝑥 = 𝑒 ∧ 𝑦 = 𝑓 ) ) → 𝑥 = 𝑒 )
87		simprr	⊢ ( ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ∧ ( 𝑥 = 𝑒 ∧ 𝑦 = 𝑓 ) ) → 𝑦 = 𝑓 )
88	86 87	s2eqd	⊢ ( ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ∧ ( 𝑥 = 𝑒 ∧ 𝑦 = 𝑓 ) ) → ⟨“ 𝑥 𝑦 ”⟩ = ⟨“ 𝑒 𝑓 ”⟩ )
89		simpl	⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → 𝑒 ∈ ℝ )
90		simpr	⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → 𝑓 ∈ ℝ )
91	85 88 89 90 52	ovmpod	⊢ ( ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) → ( 𝑒 ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) 𝑓 ) = ⟨“ 𝑒 𝑓 ”⟩ )
92	84 91	sylan9eq	⊢ ( ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑏 ) = ⟨“ 𝑒 𝑓 ”⟩ )
93	92	eqcomd	⊢ ( ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ⟨“ 𝑒 𝑓 ”⟩ = ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑏 ) )
94	81 93	breqan12d	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( ⟨“ 𝑐 𝑑 ”⟩ 𝑂 ⟨“ 𝑒 𝑓 ”⟩ ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑏 ) ) )
95	31 69 94	3bitrd	⊢ ( ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑏 ) ) )
96	95	expcom	⊢ ( ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑏 ) ) ) )
97	96	exlimivv	⊢ ( ∃ 𝑒 ∃ 𝑓 ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑏 ) ) ) )
98	97	com12	⊢ ( ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ∃ 𝑒 ∃ 𝑓 ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑏 ) ) ) )
99	98	exlimivv	⊢ ( ∃ 𝑐 ∃ 𝑑 ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ∃ 𝑒 ∃ 𝑓 ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑏 ) ) ) )
100	99	imp	⊢ ( ( ∃ 𝑐 ∃ 𝑑 ( 𝑎 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) ∧ ∃ 𝑒 ∃ 𝑓 ( 𝑏 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ ) ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑏 ) ) )
101	7 8 100	syl2an	⊢ ( ( 𝑎 ∈ ( ℝ × ℝ ) ∧ 𝑏 ∈ ( ℝ × ℝ ) ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑏 ) ) )
102	101	rgen2	⊢ ∀ 𝑎 ∈ ( ℝ × ℝ ) ∀ 𝑏 ∈ ( ℝ × ℝ ) ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑏 ) )
103		df-isom	⊢ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) Isom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) : ( ℝ × ℝ ) –1-1-onto→ 𝑅 ∧ ∀ 𝑎 ∈ ( ℝ × ℝ ) ∀ 𝑏 ∈ ( ℝ × ℝ ) ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } 𝑏 ↔ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑎 ) 𝑂 ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) ‘ 𝑏 ) ) ) )
104	6 102 103	mpbir2an	⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) Isom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } , 𝑂 ( ( ℝ × ℝ ) , 𝑅 )
105		isoeq2	⊢ ( 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } → ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) ↔ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) Isom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) ) )
106	4 105	ax-mp	⊢ ( ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) ↔ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) Isom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( ℝ × ℝ ) ∧ 𝑦 ∈ ( ℝ × ℝ ) ) ∧ ( ( 1st ‘ 𝑥 ) < ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) < ( 2nd ‘ 𝑦 ) ) ) ) } , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) )
107	104 106	mpbir	⊢ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 )
108		isoeq1	⊢ ( 𝐹 = ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) → ( 𝐹 Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) ↔ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) ) )
109	3 108	ax-mp	⊢ ( 𝐹 Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) ↔ ( 𝑥 ∈ ℝ , 𝑦 ∈ ℝ ↦ ⟨“ 𝑥 𝑦 ”⟩ ) Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 ) )
110	107 109	mpbir	⊢ 𝐹 Isom 𝑇 , 𝑂 ( ( ℝ × ℝ ) , 𝑅 )