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 (1) < y (1) \lor (x (1) = y (1) \land x (2) < y (2))))\}$
	rrx2plord2.r	$⊢ R = ℝ^{\{1, 2\}}$
	rrx2plordisom.f	$⊢ F = (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, 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 (1) < y (1) \lor (x (1) = y (1) \land x (2) < y (2))))\}$
2		rrx2plord2.r	$⊢ R = ℝ^{\{1, 2\}}$
3		rrx2plordisom.f	$⊢ F = (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, 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 ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) = (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\})$
6	2 5	rrx2xpref1o	$⊢ (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, 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		1ne2	$⊢ 1 \neq 2$
33		1ex	$⊢ 1 \in V$
34		vex	$⊢ c \in V$
35	33 34	fvpr1	$⊢ 1 \neq 2 \to \{⟨1, c⟩, ⟨2, d⟩\} (1) = c$
36	32 35	mp1i	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to \{⟨1, c⟩, ⟨2, d⟩\} (1) = c$
37		vex	$⊢ e \in V$
38	33 37	fvpr1	$⊢ 1 \neq 2 \to \{⟨1, e⟩, ⟨2, f⟩\} (1) = e$
39	32 38	mp1i	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to \{⟨1, e⟩, ⟨2, f⟩\} (1) = e$
40	36 39	breq12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (\{⟨1, c⟩, ⟨2, d⟩\} (1) < \{⟨1, e⟩, ⟨2, f⟩\} (1) \leftrightarrow c < e)$
41	36 39	eqeq12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (\{⟨1, c⟩, ⟨2, d⟩\} (1) = \{⟨1, e⟩, ⟨2, f⟩\} (1) \leftrightarrow c = e)$
42		2ex	$⊢ 2 \in V$
43		vex	$⊢ d \in V$
44	42 43	fvpr2	$⊢ 1 \neq 2 \to \{⟨1, c⟩, ⟨2, d⟩\} (2) = d$
45	32 44	mp1i	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to \{⟨1, c⟩, ⟨2, d⟩\} (2) = d$
46		vex	$⊢ f \in V$
47	42 46	fvpr2	$⊢ 1 \neq 2 \to \{⟨1, e⟩, ⟨2, f⟩\} (2) = f$
48	32 47	mp1i	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to \{⟨1, e⟩, ⟨2, f⟩\} (2) = f$
49	45 48	breq12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (\{⟨1, c⟩, ⟨2, d⟩\} (2) < \{⟨1, e⟩, ⟨2, f⟩\} (2) \leftrightarrow d < f)$
50	41 49	anbi12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to ((\{⟨1, c⟩, ⟨2, d⟩\} (1) = \{⟨1, e⟩, ⟨2, f⟩\} (1) \land \{⟨1, c⟩, ⟨2, d⟩\} (2) < \{⟨1, e⟩, ⟨2, f⟩\} (2)) \leftrightarrow (c = e \land d < f))$
51	40 50	orbi12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to ((\{⟨1, c⟩, ⟨2, d⟩\} (1) < \{⟨1, e⟩, ⟨2, f⟩\} (1) \lor (\{⟨1, c⟩, ⟨2, d⟩\} (1) = \{⟨1, e⟩, ⟨2, f⟩\} (1) \land \{⟨1, c⟩, ⟨2, d⟩\} (2) < \{⟨1, e⟩, ⟨2, f⟩\} (2))) \leftrightarrow (c < e \lor (c = e \land d < f)))$
52		eqid	$⊢ \{1, 2\} = \{1, 2\}$
53	52 2	prelrrx2	$⊢ (c \in ℝ \land d \in ℝ) \to \{⟨1, c⟩, ⟨2, d⟩\} \in R$
54	53	adantl	$⊢ (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to \{⟨1, c⟩, ⟨2, d⟩\} \in R$
55	52 2	prelrrx2	$⊢ (e \in ℝ \land f \in ℝ) \to \{⟨1, e⟩, ⟨2, f⟩\} \in R$
56	55	adantl	$⊢ (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to \{⟨1, e⟩, ⟨2, f⟩\} \in R$
57	1	rrx2plord	$⊢ (\{⟨1, c⟩, ⟨2, d⟩\} \in R \land \{⟨1, e⟩, ⟨2, f⟩\} \in R) \to (\{⟨1, c⟩, ⟨2, d⟩\} O \{⟨1, e⟩, ⟨2, f⟩\} \leftrightarrow (\{⟨1, c⟩, ⟨2, d⟩\} (1) < \{⟨1, e⟩, ⟨2, f⟩\} (1) \lor (\{⟨1, c⟩, ⟨2, d⟩\} (1) = \{⟨1, e⟩, ⟨2, f⟩\} (1) \land \{⟨1, c⟩, ⟨2, d⟩\} (2) < \{⟨1, e⟩, ⟨2, f⟩\} (2))))$
58	54 56 57	syl2an	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (\{⟨1, c⟩, ⟨2, d⟩\} O \{⟨1, e⟩, ⟨2, f⟩\} \leftrightarrow (\{⟨1, c⟩, ⟨2, d⟩\} (1) < \{⟨1, e⟩, ⟨2, f⟩\} (1) \lor (\{⟨1, c⟩, ⟨2, d⟩\} (1) = \{⟨1, e⟩, ⟨2, f⟩\} (1) \land \{⟨1, c⟩, ⟨2, d⟩\} (2) < \{⟨1, e⟩, ⟨2, f⟩\} (2))))$
59	34 43	op1std	$⊢ a = ⟨c, d⟩ \to 1^{st} (a) = c$
60	59	adantr	$⊢ (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to 1^{st} (a) = c$
61	37 46	op1std	$⊢ b = ⟨e, f⟩ \to 1^{st} (b) = e$
62	61	adantr	$⊢ (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to 1^{st} (b) = e$
63	60 62	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)$
64	60 62	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)$
65	34 43	op2ndd	$⊢ a = ⟨c, d⟩ \to 2^{nd} (a) = d$
66	65	adantr	$⊢ (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to 2^{nd} (a) = d$
67	37 46	op2ndd	$⊢ b = ⟨e, f⟩ \to 2^{nd} (b) = f$
68	67	adantr	$⊢ (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to 2^{nd} (b) = f$
69	66 68	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)$
70	64 69	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))$
71	63 70	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)))$
72	51 58 71	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 \{⟨1, c⟩, ⟨2, d⟩\} O \{⟨1, e⟩, ⟨2, f⟩\})$
73		fveq2	$⊢ a = ⟨c, d⟩ \to (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (a) = (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (⟨c, d⟩)$
74		df-ov	$⊢ c (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) d = (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (⟨c, d⟩)$
75	73 74	eqtr4di	$⊢ a = ⟨c, d⟩ \to (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (a) = c (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) d$
76		eqidd	$⊢ (c \in ℝ \land d \in ℝ) \to (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) = (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\})$
77		opeq2	$⊢ x = c \to ⟨1, x⟩ = ⟨1, c⟩$
78	77	adantr	$⊢ (x = c \land y = d) \to ⟨1, x⟩ = ⟨1, c⟩$
79		opeq2	$⊢ y = d \to ⟨2, y⟩ = ⟨2, d⟩$
80	79	adantl	$⊢ (x = c \land y = d) \to ⟨2, y⟩ = ⟨2, d⟩$
81	78 80	preq12d	$⊢ (x = c \land y = d) \to \{⟨1, x⟩, ⟨2, y⟩\} = \{⟨1, c⟩, ⟨2, d⟩\}$
82	81	adantl	$⊢ ((c \in ℝ \land d \in ℝ) \land (x = c \land y = d)) \to \{⟨1, x⟩, ⟨2, y⟩\} = \{⟨1, c⟩, ⟨2, d⟩\}$
83		simpl	$⊢ (c \in ℝ \land d \in ℝ) \to c \in ℝ$
84		simpr	$⊢ (c \in ℝ \land d \in ℝ) \to d \in ℝ$
85		prex	$⊢ \{⟨1, c⟩, ⟨2, d⟩\} \in V$
86	85	a1i	$⊢ (c \in ℝ \land d \in ℝ) \to \{⟨1, c⟩, ⟨2, d⟩\} \in V$
87	76 82 83 84 86	ovmpod	$⊢ (c \in ℝ \land d \in ℝ) \to c (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) d = \{⟨1, c⟩, ⟨2, d⟩\}$
88	75 87	sylan9eq	$⊢ (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (a) = \{⟨1, c⟩, ⟨2, d⟩\}$
89	88	eqcomd	$⊢ (a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \to \{⟨1, c⟩, ⟨2, d⟩\} = (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (a)$
90		fveq2	$⊢ b = ⟨e, f⟩ \to (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (b) = (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (⟨e, f⟩)$
91		df-ov	$⊢ e (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) f = (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (⟨e, f⟩)$
92	90 91	eqtr4di	$⊢ b = ⟨e, f⟩ \to (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (b) = e (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) f$
93		eqidd	$⊢ (e \in ℝ \land f \in ℝ) \to (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) = (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\})$
94		opeq2	$⊢ x = e \to ⟨1, x⟩ = ⟨1, e⟩$
95	94	adantr	$⊢ (x = e \land y = f) \to ⟨1, x⟩ = ⟨1, e⟩$
96		opeq2	$⊢ y = f \to ⟨2, y⟩ = ⟨2, f⟩$
97	96	adantl	$⊢ (x = e \land y = f) \to ⟨2, y⟩ = ⟨2, f⟩$
98	95 97	preq12d	$⊢ (x = e \land y = f) \to \{⟨1, x⟩, ⟨2, y⟩\} = \{⟨1, e⟩, ⟨2, f⟩\}$
99	98	adantl	$⊢ ((e \in ℝ \land f \in ℝ) \land (x = e \land y = f)) \to \{⟨1, x⟩, ⟨2, y⟩\} = \{⟨1, e⟩, ⟨2, f⟩\}$
100		simpl	$⊢ (e \in ℝ \land f \in ℝ) \to e \in ℝ$
101		simpr	$⊢ (e \in ℝ \land f \in ℝ) \to f \in ℝ$
102		prex	$⊢ \{⟨1, e⟩, ⟨2, f⟩\} \in V$
103	102	a1i	$⊢ (e \in ℝ \land f \in ℝ) \to \{⟨1, e⟩, ⟨2, f⟩\} \in V$
104	93 99 100 101 103	ovmpod	$⊢ (e \in ℝ \land f \in ℝ) \to e (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) f = \{⟨1, e⟩, ⟨2, f⟩\}$
105	92 104	sylan9eq	$⊢ (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (b) = \{⟨1, e⟩, ⟨2, f⟩\}$
106	105	eqcomd	$⊢ (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ)) \to \{⟨1, e⟩, ⟨2, f⟩\} = (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (b)$
107	89 106	breqan12d	$⊢ ((a = ⟨c, d⟩ \land (c \in ℝ \land d \in ℝ)) \land (b = ⟨e, f⟩ \land (e \in ℝ \land f \in ℝ))) \to (\{⟨1, c⟩, ⟨2, d⟩\} O \{⟨1, e⟩, ⟨2, f⟩\} \leftrightarrow (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (a) O (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (b))$
108	31 72 107	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 ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (a) O (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (b))$
109	108	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 ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (a) O (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (b)))$
110	109	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 ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (a) O (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (b)))$
111	110	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 ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (a) O (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (b)))$
112	111	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 ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (a) O (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (b)))$
113	112	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 ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (a) O (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (b))$
114	7 8 113	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 ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (a) O (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (b))$
115	114	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 ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (a) O (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (b))$
116		df-isom	$⊢ (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, 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 ℝ ⟼ \{⟨1, x⟩, ⟨2, 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 ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (a) O (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) (b)))$
117	6 115 116	mpbir2an	$⊢ (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, 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)$
118		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 ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) {Isom}_{T, O} (ℝ^{2}, R) \leftrightarrow (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, 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))$
119	4 118	ax-mp	$⊢ (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) {Isom}_{T, O} (ℝ^{2}, R) \leftrightarrow (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, 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)$
120	117 119	mpbir	$⊢ (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) {Isom}_{T, O} (ℝ^{2}, R)$
121		isoeq1	$⊢ F = (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) \to (F {Isom}_{T, O} (ℝ^{2}, R) \leftrightarrow (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) {Isom}_{T, O} (ℝ^{2}, R))$
122	3 121	ax-mp	$⊢ F {Isom}_{T, O} (ℝ^{2}, R) \leftrightarrow (x \in ℝ, y \in ℝ ⟼ \{⟨1, x⟩, ⟨2, y⟩\}) {Isom}_{T, O} (ℝ^{2}, R)$
123	120 122	mpbir	$⊢ F {Isom}_{T, O} (ℝ^{2}, R)$

Metamath Proof Explorer

Theorem rrx2plordisom

Proof