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	$⊢ O = \{⟨x, y⟩ \| ((x \in R \land y \in R) \land (x (0) < y (0) \lor (x (0) = y (0) \land x (1) < y (1))))\}$
	rrx2plord2.r	$⊢ R = ℝ^{(0 ..^2)}$
	rrx2plordisom.f	$⊢ F = (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩)$
	rrx2plordisom.t	$⊢ T = \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\}$
Assertion	rrx2plordisom	$⊢ F {Isom}_{T, O} (ℝ^{2}, R)$

Proof

Step	Hyp	Ref	Expression
1		rrx2plord.o	$⊢ O = \{⟨x, y⟩ \| ((x \in R \land y \in R) \land (x (0) < y (0) \lor (x (0) = y (0) \land x (1) < y (1))))\}$
2		rrx2plord2.r	$⊢ R = ℝ^{(0 ..^2)}$
3		rrx2plordisom.f	$⊢ F = (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩)$
4		rrx2plordisom.t	$⊢ T = \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\}$
5		eqid	$⊢ (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) = (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩)$
6	2 5	rrx2xpref1o	$⊢ (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) : ℝ^{2} \underset{1-1 onto}{⟶} R$
7		elxpi	$⊢ a \in ℝ^{2} \to \exists c \exists d (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ))$
8		elxpi	$⊢ b \in ℝ^{2} \to \exists e \exists f (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))$
9		df-br	$⊢ a \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} b \leftrightarrow ⟨a, b⟩ \in \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\}$
10		opelxpi	$⊢ (c \in ℝ \land d \in ℝ) \to ⟨c, d⟩ \in ℝ^{2}$
11	10	adantl	$⊢ (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to ⟨c, d⟩ \in ℝ^{2}$
12		eleq1	$⊢ a = ⟨c, d⟩ \to (a \in ℝ^{2} \leftrightarrow ⟨c, d⟩ \in ℝ^{2})$
13	12	adantr	$⊢ (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to (a \in ℝ^{2} \leftrightarrow ⟨c, d⟩ \in ℝ^{2})$
14	11 13	mpbird	$⊢ (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to a \in ℝ^{2}$
15		opelxpi	$⊢ (e \in ℝ \land f \in ℝ) \to ⟨e, f⟩ \in ℝ^{2}$
16	15	adantl	$⊢ (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to ⟨e, f⟩ \in ℝ^{2}$
17		eleq1	$⊢ b = ⟨e, f⟩ \to (b \in ℝ^{2} \leftrightarrow ⟨e, f⟩ \in ℝ^{2})$
18	17	adantr	$⊢ (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to (b \in ℝ^{2} \leftrightarrow ⟨e, f⟩ \in ℝ^{2})$
19	16 18	mpbird	$⊢ (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to b \in ℝ^{2}$
20		fveq2	$⊢ x = a \to 1^{st} (x) = 1^{st} (a)$
21		fveq2	$⊢ y = b \to 1^{st} (y) = 1^{st} (b)$
22	20 21	breqan12d	$⊢ (x = a \land y = b) \to (1^{st} (x) < 1^{st} (y) \leftrightarrow 1^{st} (a) < 1^{st} (b))$
23	20 21	eqeqan12d	$⊢ (x = a \land y = b) \to (1^{st} (x) = 1^{st} (y) \leftrightarrow 1^{st} (a) = 1^{st} (b))$
24		fveq2	$⊢ x = a \to 2^{nd} (x) = 2^{nd} (a)$
25		fveq2	$⊢ y = b \to 2^{nd} (y) = 2^{nd} (b)$
26	24 25	breqan12d	$⊢ (x = a \land y = b) \to (2^{nd} (x) < 2^{nd} (y) \leftrightarrow 2^{nd} (a) < 2^{nd} (b))$
27	23 26	anbi12d	$⊢ (x = a \land y = b) \to ((1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y)) \leftrightarrow (1^{st} (a) = 1^{st} (b) \land 2^{nd} (a) < 2^{nd} (b)))$
28	22 27	orbi12d	$⊢ (x = a \land y = b) \to ((1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))) \leftrightarrow (1^{st} (a) < 1^{st} (b) \lor (1^{st} (a) = 1^{st} (b) \land 2^{nd} (a) < 2^{nd} (b))))$
29	28	opelopab2a	$⊢ (a \in ℝ^{2} \land b \in ℝ^{2}) \to (⟨a, b⟩ \in \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} \leftrightarrow (1^{st} (a) < 1^{st} (b) \lor (1^{st} (a) = 1^{st} (b) \land 2^{nd} (a) < 2^{nd} (b))))$
30	14 19 29	syl2an	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (⟨a, b⟩ \in \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} \leftrightarrow (1^{st} (a) < 1^{st} (b) \lor (1^{st} (a) = 1^{st} (b) \land 2^{nd} (a) < 2^{nd} (b))))$
31	9 30	bitrid	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (a \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} b \leftrightarrow (1^{st} (a) < 1^{st} (b) \lor (1^{st} (a) = 1^{st} (b) \land 2^{nd} (a) < 2^{nd} (b))))$
32		vex	$⊢ c \in V$
33		s2fv0	$⊢ c \in V \to ⟨“ c d ”⟩ (0) = c$
34	32 33	mp1i	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to ⟨“ c d ”⟩ (0) = c$
35		vex	$⊢ e \in V$
36		s2fv0	$⊢ e \in V \to ⟨“ e f ”⟩ (0) = e$
37	35 36	mp1i	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to ⟨“ e f ”⟩ (0) = e$
38	34 37	breq12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (⟨“ c d ”⟩ (0) < ⟨“ e f ”⟩ (0) \leftrightarrow c < e)$
39	34 37	eqeq12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (⟨“ c d ”⟩ (0) = ⟨“ e f ”⟩ (0) \leftrightarrow c = e)$
40		vex	$⊢ d \in V$
41		s2fv1	$⊢ d \in V \to ⟨“ c d ”⟩ (1) = d$
42	40 41	mp1i	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to ⟨“ c d ”⟩ (1) = d$
43		vex	$⊢ f \in V$
44		s2fv1	$⊢ f \in V \to ⟨“ e f ”⟩ (1) = f$
45	43 44	mp1i	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to ⟨“ e f ”⟩ (1) = f$
46	42 45	breq12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (⟨“ c d ”⟩ (1) < ⟨“ e f ”⟩ (1) \leftrightarrow d < f)$
47	39 46	anbi12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to ((⟨“ c d ”⟩ (0) = ⟨“ e f ”⟩ (0) \land ⟨“ c d ”⟩ (1) < ⟨“ e f ”⟩ (1)) \leftrightarrow (c = e \land d < f))$
48	38 47	orbi12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to ((⟨“ c d ”⟩ (0) < ⟨“ e f ”⟩ (0) \lor (⟨“ c d ”⟩ (0) = ⟨“ e f ”⟩ (0) \land ⟨“ c d ”⟩ (1) < ⟨“ e f ”⟩ (1))) \leftrightarrow (c < e \lor (c = e \land d < f)))$
49		eqid	$⊢ (0 ..^2) = (0 ..^2)$
50	49 2	prelrrx2	$⊢ (c \in ℝ \land d \in ℝ) \to ⟨“ c d ”⟩ \in R$
51	50	adantl	$⊢ (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to ⟨“ c d ”⟩ \in R$
52	49 2	prelrrx2	$⊢ (e \in ℝ \land f \in ℝ) \to ⟨“ e f ”⟩ \in R$
53	52	adantl	$⊢ (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to ⟨“ e f ”⟩ \in R$
54	1	rrx2plord	$⊢ (⟨“ c d ”⟩ \in R \land ⟨“ e f ”⟩ \in R) \to (⟨“ c d ”⟩ O ⟨“ e f ”⟩ \leftrightarrow (⟨“ c d ”⟩ (0) < ⟨“ e f ”⟩ (0) \lor (⟨“ c d ”⟩ (0) = ⟨“ e f ”⟩ (0) \land ⟨“ c d ”⟩ (1) < ⟨“ e f ”⟩ (1))))$
55	51 53 54	syl2an	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (⟨“ c d ”⟩ O ⟨“ e f ”⟩ \leftrightarrow (⟨“ c d ”⟩ (0) < ⟨“ e f ”⟩ (0) \lor (⟨“ c d ”⟩ (0) = ⟨“ e f ”⟩ (0) \land ⟨“ c d ”⟩ (1) < ⟨“ e f ”⟩ (1))))$
56	32 40	op1std	$⊢ a = ⟨c, d⟩ \to 1^{st} (a) = c$
57	56	adantr	$⊢ (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to 1^{st} (a) = c$
58	35 43	op1std	$⊢ b = ⟨e, f⟩ \to 1^{st} (b) = e$
59	58	adantr	$⊢ (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to 1^{st} (b) = e$
60	57 59	breqan12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (1^{st} (a) < 1^{st} (b) \leftrightarrow c < e)$
61	57 59	eqeqan12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (1^{st} (a) = 1^{st} (b) \leftrightarrow c = e)$
62	32 40	op2ndd	$⊢ a = ⟨c, d⟩ \to 2^{nd} (a) = d$
63	62	adantr	$⊢ (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to 2^{nd} (a) = d$
64	35 43	op2ndd	$⊢ b = ⟨e, f⟩ \to 2^{nd} (b) = f$
65	64	adantr	$⊢ (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to 2^{nd} (b) = f$
66	63 65	breqan12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (2^{nd} (a) < 2^{nd} (b) \leftrightarrow d < f)$
67	61 66	anbi12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to ((1^{st} (a) = 1^{st} (b) \land 2^{nd} (a) < 2^{nd} (b)) \leftrightarrow (c = e \land d < f))$
68	60 67	orbi12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to ((1^{st} (a) < 1^{st} (b) \lor (1^{st} (a) = 1^{st} (b) \land 2^{nd} (a) < 2^{nd} (b))) \leftrightarrow (c < e \lor (c = e \land d < f)))$
69	48 55 68	3bitr4rd	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to ((1^{st} (a) < 1^{st} (b) \lor (1^{st} (a) = 1^{st} (b) \land 2^{nd} (a) < 2^{nd} (b))) \leftrightarrow ⟨“ c d ”⟩ O ⟨“ e f ”⟩)$
70		fveq2	$⊢ a = ⟨c, d⟩ \to (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (a) = (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (⟨c, d⟩)$
71		df-ov	$⊢ c (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) d = (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (⟨c, d⟩)$
72	70 71	eqtr4di	$⊢ a = ⟨c, d⟩ \to (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (a) = c (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) d$
73		eqidd	$⊢ (c \in ℝ \land d \in ℝ) \to (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) = (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩)$
74		simprl	$⊢ ((c \in ℝ \land d \in ℝ) \land (x = c \land y = d)) \to x = c$
75		simprr	$⊢ ((c \in ℝ \land d \in ℝ) \land (x = c \land y = d)) \to y = d$
76	74 75	s2eqd	$⊢ ((c \in ℝ \land d \in ℝ) \land (x = c \land y = d)) \to ⟨“ x y ”⟩ = ⟨“ c d ”⟩$
77		simpl	$⊢ (c \in ℝ \land d \in ℝ) \to c \in ℝ$
78		simpr	$⊢ (c \in ℝ \land d \in ℝ) \to d \in ℝ$
79	73 76 77 78 50	ovmpod	$⊢ (c \in ℝ \land d \in ℝ) \to c (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) d = ⟨“ c d ”⟩$
80	72 79	sylan9eq	$⊢ (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (a) = ⟨“ c d ”⟩$
81	80	eqcomd	$⊢ (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to ⟨“ c d ”⟩ = (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (a)$
82		fveq2	$⊢ b = ⟨e, f⟩ \to (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (b) = (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (⟨e, f⟩)$
83		df-ov	$⊢ e (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) f = (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (⟨e, f⟩)$
84	82 83	eqtr4di	$⊢ b = ⟨e, f⟩ \to (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (b) = e (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) f$
85		eqidd	$⊢ (e \in ℝ \land f \in ℝ) \to (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) = (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩)$
86		simprl	$⊢ ((e \in ℝ \land f \in ℝ) \land (x = e \land y = f)) \to x = e$
87		simprr	$⊢ ((e \in ℝ \land f \in ℝ) \land (x = e \land y = f)) \to y = f$
88	86 87	s2eqd	$⊢ ((e \in ℝ \land f \in ℝ) \land (x = e \land y = f)) \to ⟨“ x y ”⟩ = ⟨“ e f ”⟩$
89		simpl	$⊢ (e \in ℝ \land f \in ℝ) \to e \in ℝ$
90		simpr	$⊢ (e \in ℝ \land f \in ℝ) \to f \in ℝ$
91	85 88 89 90 52	ovmpod	$⊢ (e \in ℝ \land f \in ℝ) \to e (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) f = ⟨“ e f ”⟩$
92	84 91	sylan9eq	$⊢ (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (b) = ⟨“ e f ”⟩$
93	92	eqcomd	$⊢ (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to ⟨“ e f ”⟩ = (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (b)$
94	81 93	breqan12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (⟨“ c d ”⟩ O ⟨“ e f ”⟩ \leftrightarrow (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (a) O (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (b))$
95	31 69 94	3bitrd	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (a \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} b \leftrightarrow (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (a) O (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (b))$
96	95	expcom	$⊢ (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to (a \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} b \leftrightarrow (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (a) O (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (b)))$
97	96	exlimivv	$⊢ \exists e \exists f (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to (a \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} b \leftrightarrow (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (a) O (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (b)))$
98	97	com12	$⊢ (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to (\exists e \exists f (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to (a \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} b \leftrightarrow (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (a) O (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (b)))$
99	98	exlimivv	$⊢ \exists c \exists d (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to (\exists e \exists f (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to (a \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} b \leftrightarrow (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (a) O (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (b)))$
100	99	imp	$⊢ (\exists c \exists d (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land \exists e \exists f (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (a \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} b \leftrightarrow (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (a) O (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (b))$
101	7 8 100	syl2an	$⊢ (a \in ℝ^{2} \land b \in ℝ^{2}) \to (a \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} b \leftrightarrow (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (a) O (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (b))$
102	101	rgen2	$⊢ \forall a \in ℝ^{2} \forall b \in ℝ^{2} (a \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} b \leftrightarrow (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (a) O (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (b))$
103		df-isom	$⊢ (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) {Isom}_{\{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\}, O} (ℝ^{2}, R) \leftrightarrow ((x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) : ℝ^{2} \underset{1-1 onto}{⟶} R \land \forall a \in ℝ^{2} \forall b \in ℝ^{2} (a \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} b \leftrightarrow (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (a) O (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) (b)))$
104	6 102 103	mpbir2an	$⊢ (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) {Isom}_{\{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\}, O} (ℝ^{2}, R)$
105		isoeq2	$⊢ T = \{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\} \to ((x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) {Isom}_{T, O} (ℝ^{2}, R) \leftrightarrow (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) {Isom}_{\{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\}, O} (ℝ^{2}, R))$
106	4 105	ax-mp	$⊢ (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) {Isom}_{T, O} (ℝ^{2}, R) \leftrightarrow (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) {Isom}_{\{⟨x, y⟩ \| ((x \in ℝ^{2} \land y \in ℝ^{2}) \land (1^{st} (x) < 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) < 2^{nd} (y))))\}, O} (ℝ^{2}, R)$
107	104 106	mpbir	$⊢ (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) {Isom}_{T, O} (ℝ^{2}, R)$
108		isoeq1	$⊢ F = (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) \to (F {Isom}_{T, O} (ℝ^{2}, R) \leftrightarrow (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) {Isom}_{T, O} (ℝ^{2}, R))$
109	3 108	ax-mp	$⊢ F {Isom}_{T, O} (ℝ^{2}, R) \leftrightarrow (x \in ℝ, y \in ℝ ⟼ ⟨“ x y ”⟩) {Isom}_{T, O} (ℝ^{2}, R)$
110	107 109	mpbir	$⊢ F {Isom}_{T, O} (ℝ^{2}, R)$

Metamath Proof Explorer

Theorem rrx2plordisom

Proof