prelrrx2b

Description: An unordered pair of ordered pairs with first components 1 and 2 and real numbers as second components is a point in a real Euclidean space of dimension 2, determined by its coordinates. (Contributed by AV, 7-May-2023)

	Ref	Expression
Hypotheses	prelrrx2.i	$⊢ I = \{1, 2\}$
	prelrrx2.b	$⊢ P = ℝ^{I}$
Assertion	prelrrx2b	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to ((Z \in P \land ((Z (1) = A \land Z (2) = B) \lor (Z (1) = X \land Z (2) = Y))) \leftrightarrow Z \in \{\{⟨1, A⟩, ⟨2, B⟩\}, \{⟨1, X⟩, ⟨2, Y⟩\}\})$

Proof

Step	Hyp	Ref	Expression
1		prelrrx2.i	$⊢ I = \{1, 2\}$
2		prelrrx2.b	$⊢ P = ℝ^{I}$
3	2	eleq2i	$⊢ Z \in P \leftrightarrow Z \in (ℝ^{I})$
4	1	oveq2i	$⊢ ℝ^{I} = ℝ^{\{1, 2\}}$
5	4	eleq2i	$⊢ Z \in (ℝ^{I}) \leftrightarrow Z \in (ℝ^{\{1, 2\}})$
6	3 5	bitri	$⊢ Z \in P \leftrightarrow Z \in (ℝ^{\{1, 2\}})$
7		elmapi	$⊢ Z \in (ℝ^{\{1, 2\}}) \to Z : \{1, 2\} ⟶ ℝ$
8		1ne2	$⊢ 1 \neq 2$
9		1ex	$⊢ 1 \in V$
10		2ex	$⊢ 2 \in V$
11	9 10	fprb	$⊢ 1 \neq 2 \to (Z : \{1, 2\} ⟶ ℝ \leftrightarrow \exists x \in ℝ \exists y \in ℝ Z = \{⟨1, x⟩, ⟨2, y⟩\})$
12	8 11	ax-mp	$⊢ Z : \{1, 2\} ⟶ ℝ \leftrightarrow \exists x \in ℝ \exists y \in ℝ Z = \{⟨1, x⟩, ⟨2, y⟩\}$
13		fveq1	$⊢ Z = \{⟨1, x⟩, ⟨2, y⟩\} \to Z (1) = \{⟨1, x⟩, ⟨2, y⟩\} (1)$
14		vex	$⊢ x \in V$
15	9 14	fvpr1	$⊢ 1 \neq 2 \to \{⟨1, x⟩, ⟨2, y⟩\} (1) = x$
16	8 15	ax-mp	$⊢ \{⟨1, x⟩, ⟨2, y⟩\} (1) = x$
17	13 16	eqtrdi	$⊢ Z = \{⟨1, x⟩, ⟨2, y⟩\} \to Z (1) = x$
18	17	eqeq1d	$⊢ Z = \{⟨1, x⟩, ⟨2, y⟩\} \to (Z (1) = A \leftrightarrow x = A)$
19		fveq1	$⊢ Z = \{⟨1, x⟩, ⟨2, y⟩\} \to Z (2) = \{⟨1, x⟩, ⟨2, y⟩\} (2)$
20		vex	$⊢ y \in V$
21	10 20	fvpr2	$⊢ 1 \neq 2 \to \{⟨1, x⟩, ⟨2, y⟩\} (2) = y$
22	8 21	ax-mp	$⊢ \{⟨1, x⟩, ⟨2, y⟩\} (2) = y$
23	19 22	eqtrdi	$⊢ Z = \{⟨1, x⟩, ⟨2, y⟩\} \to Z (2) = y$
24	23	eqeq1d	$⊢ Z = \{⟨1, x⟩, ⟨2, y⟩\} \to (Z (2) = B \leftrightarrow y = B)$
25	18 24	anbi12d	$⊢ Z = \{⟨1, x⟩, ⟨2, y⟩\} \to ((Z (1) = A \land Z (2) = B) \leftrightarrow (x = A \land y = B))$
26	25	adantl	$⊢ ((((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land (x \in ℝ \land y \in ℝ)) \land Z = \{⟨1, x⟩, ⟨2, y⟩\}) \to ((Z (1) = A \land Z (2) = B) \leftrightarrow (x = A \land y = B))$
27		opeq2	$⊢ x = A \to ⟨1, x⟩ = ⟨1, A⟩$
28	27	adantr	$⊢ (x = A \land y = B) \to ⟨1, x⟩ = ⟨1, A⟩$
29		opeq2	$⊢ y = B \to ⟨2, y⟩ = ⟨2, B⟩$
30	29	adantl	$⊢ (x = A \land y = B) \to ⟨2, y⟩ = ⟨2, B⟩$
31	28 30	preq12d	$⊢ (x = A \land y = B) \to \{⟨1, x⟩, ⟨2, y⟩\} = \{⟨1, A⟩, ⟨2, B⟩\}$
32	31	eqeq2d	$⊢ (x = A \land y = B) \to (Z = \{⟨1, x⟩, ⟨2, y⟩\} \leftrightarrow Z = \{⟨1, A⟩, ⟨2, B⟩\})$
33	32	biimpcd	$⊢ Z = \{⟨1, x⟩, ⟨2, y⟩\} \to ((x = A \land y = B) \to Z = \{⟨1, A⟩, ⟨2, B⟩\})$
34	33	adantl	$⊢ ((((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land (x \in ℝ \land y \in ℝ)) \land Z = \{⟨1, x⟩, ⟨2, y⟩\}) \to ((x = A \land y = B) \to Z = \{⟨1, A⟩, ⟨2, B⟩\})$
35	26 34	sylbid	$⊢ ((((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land (x \in ℝ \land y \in ℝ)) \land Z = \{⟨1, x⟩, ⟨2, y⟩\}) \to ((Z (1) = A \land Z (2) = B) \to Z = \{⟨1, A⟩, ⟨2, B⟩\})$
36	35	ex	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land (x \in ℝ \land y \in ℝ)) \to (Z = \{⟨1, x⟩, ⟨2, y⟩\} \to ((Z (1) = A \land Z (2) = B) \to Z = \{⟨1, A⟩, ⟨2, B⟩\}))$
37	36	rexlimdvva	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (\exists x \in ℝ \exists y \in ℝ Z = \{⟨1, x⟩, ⟨2, y⟩\} \to ((Z (1) = A \land Z (2) = B) \to Z = \{⟨1, A⟩, ⟨2, B⟩\}))$
38	12 37	biimtrid	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (Z : \{1, 2\} ⟶ ℝ \to ((Z (1) = A \land Z (2) = B) \to Z = \{⟨1, A⟩, ⟨2, B⟩\}))$
39	7 38	syl5	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (Z \in (ℝ^{\{1, 2\}}) \to ((Z (1) = A \land Z (2) = B) \to Z = \{⟨1, A⟩, ⟨2, B⟩\}))$
40	6 39	biimtrid	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (Z \in P \to ((Z (1) = A \land Z (2) = B) \to Z = \{⟨1, A⟩, ⟨2, B⟩\}))$
41	40	imp	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z \in P) \to ((Z (1) = A \land Z (2) = B) \to Z = \{⟨1, A⟩, ⟨2, B⟩\})$
42	17	eqeq1d	$⊢ Z = \{⟨1, x⟩, ⟨2, y⟩\} \to (Z (1) = X \leftrightarrow x = X)$
43	23	eqeq1d	$⊢ Z = \{⟨1, x⟩, ⟨2, y⟩\} \to (Z (2) = Y \leftrightarrow y = Y)$
44	42 43	anbi12d	$⊢ Z = \{⟨1, x⟩, ⟨2, y⟩\} \to ((Z (1) = X \land Z (2) = Y) \leftrightarrow (x = X \land y = Y))$
45	44	adantl	$⊢ ((((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land (x \in ℝ \land y \in ℝ)) \land Z = \{⟨1, x⟩, ⟨2, y⟩\}) \to ((Z (1) = X \land Z (2) = Y) \leftrightarrow (x = X \land y = Y))$
46		opeq2	$⊢ x = X \to ⟨1, x⟩ = ⟨1, X⟩$
47	46	adantr	$⊢ (x = X \land y = Y) \to ⟨1, x⟩ = ⟨1, X⟩$
48		opeq2	$⊢ y = Y \to ⟨2, y⟩ = ⟨2, Y⟩$
49	48	adantl	$⊢ (x = X \land y = Y) \to ⟨2, y⟩ = ⟨2, Y⟩$
50	47 49	preq12d	$⊢ (x = X \land y = Y) \to \{⟨1, x⟩, ⟨2, y⟩\} = \{⟨1, X⟩, ⟨2, Y⟩\}$
51	50	eqeq2d	$⊢ (x = X \land y = Y) \to (Z = \{⟨1, x⟩, ⟨2, y⟩\} \leftrightarrow Z = \{⟨1, X⟩, ⟨2, Y⟩\})$
52	51	biimpcd	$⊢ Z = \{⟨1, x⟩, ⟨2, y⟩\} \to ((x = X \land y = Y) \to Z = \{⟨1, X⟩, ⟨2, Y⟩\})$
53	52	adantl	$⊢ ((((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land (x \in ℝ \land y \in ℝ)) \land Z = \{⟨1, x⟩, ⟨2, y⟩\}) \to ((x = X \land y = Y) \to Z = \{⟨1, X⟩, ⟨2, Y⟩\})$
54	45 53	sylbid	$⊢ ((((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land (x \in ℝ \land y \in ℝ)) \land Z = \{⟨1, x⟩, ⟨2, y⟩\}) \to ((Z (1) = X \land Z (2) = Y) \to Z = \{⟨1, X⟩, ⟨2, Y⟩\})$
55	54	ex	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land (x \in ℝ \land y \in ℝ)) \to (Z = \{⟨1, x⟩, ⟨2, y⟩\} \to ((Z (1) = X \land Z (2) = Y) \to Z = \{⟨1, X⟩, ⟨2, Y⟩\}))$
56	55	rexlimdvva	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (\exists x \in ℝ \exists y \in ℝ Z = \{⟨1, x⟩, ⟨2, y⟩\} \to ((Z (1) = X \land Z (2) = Y) \to Z = \{⟨1, X⟩, ⟨2, Y⟩\}))$
57	12 56	biimtrid	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (Z : \{1, 2\} ⟶ ℝ \to ((Z (1) = X \land Z (2) = Y) \to Z = \{⟨1, X⟩, ⟨2, Y⟩\}))$
58	7 57	syl5	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (Z \in (ℝ^{\{1, 2\}}) \to ((Z (1) = X \land Z (2) = Y) \to Z = \{⟨1, X⟩, ⟨2, Y⟩\}))$
59	6 58	biimtrid	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (Z \in P \to ((Z (1) = X \land Z (2) = Y) \to Z = \{⟨1, X⟩, ⟨2, Y⟩\}))$
60	59	imp	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z \in P) \to ((Z (1) = X \land Z (2) = Y) \to Z = \{⟨1, X⟩, ⟨2, Y⟩\})$
61	41 60	orim12d	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z \in P) \to (((Z (1) = A \land Z (2) = B) \lor (Z (1) = X \land Z (2) = Y)) \to (Z = \{⟨1, A⟩, ⟨2, B⟩\} \lor Z = \{⟨1, X⟩, ⟨2, Y⟩\}))$
62	61	imp	$⊢ ((((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z \in P) \land ((Z (1) = A \land Z (2) = B) \lor (Z (1) = X \land Z (2) = Y))) \to (Z = \{⟨1, A⟩, ⟨2, B⟩\} \lor Z = \{⟨1, X⟩, ⟨2, Y⟩\})$
63		elprg	$⊢ Z \in P \to (Z \in \{\{⟨1, A⟩, ⟨2, B⟩\}, \{⟨1, X⟩, ⟨2, Y⟩\}\} \leftrightarrow (Z = \{⟨1, A⟩, ⟨2, B⟩\} \lor Z = \{⟨1, X⟩, ⟨2, Y⟩\}))$
64	63	ad2antlr	$⊢ ((((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z \in P) \land ((Z (1) = A \land Z (2) = B) \lor (Z (1) = X \land Z (2) = Y))) \to (Z \in \{\{⟨1, A⟩, ⟨2, B⟩\}, \{⟨1, X⟩, ⟨2, Y⟩\}\} \leftrightarrow (Z = \{⟨1, A⟩, ⟨2, B⟩\} \lor Z = \{⟨1, X⟩, ⟨2, Y⟩\}))$
65	62 64	mpbird	$⊢ ((((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z \in P) \land ((Z (1) = A \land Z (2) = B) \lor (Z (1) = X \land Z (2) = Y))) \to Z \in \{\{⟨1, A⟩, ⟨2, B⟩\}, \{⟨1, X⟩, ⟨2, Y⟩\}\}$
66	65	expl	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to ((Z \in P \land ((Z (1) = A \land Z (2) = B) \lor (Z (1) = X \land Z (2) = Y))) \to Z \in \{\{⟨1, A⟩, ⟨2, B⟩\}, \{⟨1, X⟩, ⟨2, Y⟩\}\})$
67		elpri	$⊢ Z \in \{\{⟨1, A⟩, ⟨2, B⟩\}, \{⟨1, X⟩, ⟨2, Y⟩\}\} \to (Z = \{⟨1, A⟩, ⟨2, B⟩\} \lor Z = \{⟨1, X⟩, ⟨2, Y⟩\})$
68	1 2	prelrrx2	$⊢ (A \in ℝ \land B \in ℝ) \to \{⟨1, A⟩, ⟨2, B⟩\} \in P$
69	68	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, A⟩, ⟨2, B⟩\}) \to \{⟨1, A⟩, ⟨2, B⟩\} \in P$
70		eleq1	$⊢ Z = \{⟨1, A⟩, ⟨2, B⟩\} \to (Z \in P \leftrightarrow \{⟨1, A⟩, ⟨2, B⟩\} \in P)$
71	70	adantl	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, A⟩, ⟨2, B⟩\}) \to (Z \in P \leftrightarrow \{⟨1, A⟩, ⟨2, B⟩\} \in P)$
72	69 71	mpbird	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, A⟩, ⟨2, B⟩\}) \to Z \in P$
73		simpl	$⊢ (A \in ℝ \land B \in ℝ) \to A \in ℝ$
74	8	a1i	$⊢ (A \in ℝ \land B \in ℝ) \to 1 \neq 2$
75		fvpr1g	$⊢ (1 \in V \land A \in ℝ \land 1 \neq 2) \to \{⟨1, A⟩, ⟨2, B⟩\} (1) = A$
76	9 73 74 75	mp3an2i	$⊢ (A \in ℝ \land B \in ℝ) \to \{⟨1, A⟩, ⟨2, B⟩\} (1) = A$
77		simpr	$⊢ (A \in ℝ \land B \in ℝ) \to B \in ℝ$
78		fvpr2g	$⊢ (2 \in V \land B \in ℝ \land 1 \neq 2) \to \{⟨1, A⟩, ⟨2, B⟩\} (2) = B$
79	10 77 74 78	mp3an2i	$⊢ (A \in ℝ \land B \in ℝ) \to \{⟨1, A⟩, ⟨2, B⟩\} (2) = B$
80	76 79	jca	$⊢ (A \in ℝ \land B \in ℝ) \to (\{⟨1, A⟩, ⟨2, B⟩\} (1) = A \land \{⟨1, A⟩, ⟨2, B⟩\} (2) = B)$
81	80	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, A⟩, ⟨2, B⟩\}) \to (\{⟨1, A⟩, ⟨2, B⟩\} (1) = A \land \{⟨1, A⟩, ⟨2, B⟩\} (2) = B)$
82		fveq1	$⊢ Z = \{⟨1, A⟩, ⟨2, B⟩\} \to Z (1) = \{⟨1, A⟩, ⟨2, B⟩\} (1)$
83	82	eqeq1d	$⊢ Z = \{⟨1, A⟩, ⟨2, B⟩\} \to (Z (1) = A \leftrightarrow \{⟨1, A⟩, ⟨2, B⟩\} (1) = A)$
84		fveq1	$⊢ Z = \{⟨1, A⟩, ⟨2, B⟩\} \to Z (2) = \{⟨1, A⟩, ⟨2, B⟩\} (2)$
85	84	eqeq1d	$⊢ Z = \{⟨1, A⟩, ⟨2, B⟩\} \to (Z (2) = B \leftrightarrow \{⟨1, A⟩, ⟨2, B⟩\} (2) = B)$
86	83 85	anbi12d	$⊢ Z = \{⟨1, A⟩, ⟨2, B⟩\} \to ((Z (1) = A \land Z (2) = B) \leftrightarrow (\{⟨1, A⟩, ⟨2, B⟩\} (1) = A \land \{⟨1, A⟩, ⟨2, B⟩\} (2) = B))$
87	86	adantl	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, A⟩, ⟨2, B⟩\}) \to ((Z (1) = A \land Z (2) = B) \leftrightarrow (\{⟨1, A⟩, ⟨2, B⟩\} (1) = A \land \{⟨1, A⟩, ⟨2, B⟩\} (2) = B))$
88	81 87	mpbird	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, A⟩, ⟨2, B⟩\}) \to (Z (1) = A \land Z (2) = B)$
89	88	orcd	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, A⟩, ⟨2, B⟩\}) \to ((Z (1) = A \land Z (2) = B) \lor (Z (1) = X \land Z (2) = Y))$
90	72 89	jca	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, A⟩, ⟨2, B⟩\}) \to (Z \in P \land ((Z (1) = A \land Z (2) = B) \lor (Z (1) = X \land Z (2) = Y)))$
91	90	ex	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (Z = \{⟨1, A⟩, ⟨2, B⟩\} \to (Z \in P \land ((Z (1) = A \land Z (2) = B) \lor (Z (1) = X \land Z (2) = Y))))$
92	1 2	prelrrx2	$⊢ (X \in ℝ \land Y \in ℝ) \to \{⟨1, X⟩, ⟨2, Y⟩\} \in P$
93	92	ad2antlr	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, X⟩, ⟨2, Y⟩\}) \to \{⟨1, X⟩, ⟨2, Y⟩\} \in P$
94		eleq1	$⊢ Z = \{⟨1, X⟩, ⟨2, Y⟩\} \to (Z \in P \leftrightarrow \{⟨1, X⟩, ⟨2, Y⟩\} \in P)$
95	94	adantl	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, X⟩, ⟨2, Y⟩\}) \to (Z \in P \leftrightarrow \{⟨1, X⟩, ⟨2, Y⟩\} \in P)$
96	93 95	mpbird	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, X⟩, ⟨2, Y⟩\}) \to Z \in P$
97		simpl	$⊢ (X \in ℝ \land Y \in ℝ) \to X \in ℝ$
98	8	a1i	$⊢ (X \in ℝ \land Y \in ℝ) \to 1 \neq 2$
99		fvpr1g	$⊢ (1 \in V \land X \in ℝ \land 1 \neq 2) \to \{⟨1, X⟩, ⟨2, Y⟩\} (1) = X$
100	9 97 98 99	mp3an2i	$⊢ (X \in ℝ \land Y \in ℝ) \to \{⟨1, X⟩, ⟨2, Y⟩\} (1) = X$
101		simpr	$⊢ (X \in ℝ \land Y \in ℝ) \to Y \in ℝ$
102		fvpr2g	$⊢ (2 \in V \land Y \in ℝ \land 1 \neq 2) \to \{⟨1, X⟩, ⟨2, Y⟩\} (2) = Y$
103	10 101 98 102	mp3an2i	$⊢ (X \in ℝ \land Y \in ℝ) \to \{⟨1, X⟩, ⟨2, Y⟩\} (2) = Y$
104	100 103	jca	$⊢ (X \in ℝ \land Y \in ℝ) \to (\{⟨1, X⟩, ⟨2, Y⟩\} (1) = X \land \{⟨1, X⟩, ⟨2, Y⟩\} (2) = Y)$
105	104	ad2antlr	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, X⟩, ⟨2, Y⟩\}) \to (\{⟨1, X⟩, ⟨2, Y⟩\} (1) = X \land \{⟨1, X⟩, ⟨2, Y⟩\} (2) = Y)$
106		fveq1	$⊢ Z = \{⟨1, X⟩, ⟨2, Y⟩\} \to Z (1) = \{⟨1, X⟩, ⟨2, Y⟩\} (1)$
107	106	eqeq1d	$⊢ Z = \{⟨1, X⟩, ⟨2, Y⟩\} \to (Z (1) = X \leftrightarrow \{⟨1, X⟩, ⟨2, Y⟩\} (1) = X)$
108		fveq1	$⊢ Z = \{⟨1, X⟩, ⟨2, Y⟩\} \to Z (2) = \{⟨1, X⟩, ⟨2, Y⟩\} (2)$
109	108	eqeq1d	$⊢ Z = \{⟨1, X⟩, ⟨2, Y⟩\} \to (Z (2) = Y \leftrightarrow \{⟨1, X⟩, ⟨2, Y⟩\} (2) = Y)$
110	107 109	anbi12d	$⊢ Z = \{⟨1, X⟩, ⟨2, Y⟩\} \to ((Z (1) = X \land Z (2) = Y) \leftrightarrow (\{⟨1, X⟩, ⟨2, Y⟩\} (1) = X \land \{⟨1, X⟩, ⟨2, Y⟩\} (2) = Y))$
111	110	adantl	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, X⟩, ⟨2, Y⟩\}) \to ((Z (1) = X \land Z (2) = Y) \leftrightarrow (\{⟨1, X⟩, ⟨2, Y⟩\} (1) = X \land \{⟨1, X⟩, ⟨2, Y⟩\} (2) = Y))$
112	105 111	mpbird	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, X⟩, ⟨2, Y⟩\}) \to (Z (1) = X \land Z (2) = Y)$
113	112	olcd	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, X⟩, ⟨2, Y⟩\}) \to ((Z (1) = A \land Z (2) = B) \lor (Z (1) = X \land Z (2) = Y))$
114	96 113	jca	$⊢ (((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \land Z = \{⟨1, X⟩, ⟨2, Y⟩\}) \to (Z \in P \land ((Z (1) = A \land Z (2) = B) \lor (Z (1) = X \land Z (2) = Y)))$
115	114	ex	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (Z = \{⟨1, X⟩, ⟨2, Y⟩\} \to (Z \in P \land ((Z (1) = A \land Z (2) = B) \lor (Z (1) = X \land Z (2) = Y))))$
116	91 115	jaod	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to ((Z = \{⟨1, A⟩, ⟨2, B⟩\} \lor Z = \{⟨1, X⟩, ⟨2, Y⟩\}) \to (Z \in P \land ((Z (1) = A \land Z (2) = B) \lor (Z (1) = X \land Z (2) = Y))))$
117	67 116	syl5	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to (Z \in \{\{⟨1, A⟩, ⟨2, B⟩\}, \{⟨1, X⟩, ⟨2, Y⟩\}\} \to (Z \in P \land ((Z (1) = A \land Z (2) = B) \lor (Z (1) = X \land Z (2) = Y))))$
118	66 117	impbid	$⊢ ((A \in ℝ \land B \in ℝ) \land (X \in ℝ \land Y \in ℝ)) \to ((Z \in P \land ((Z (1) = A \land Z (2) = B) \lor (Z (1) = X \land Z (2) = Y))) \leftrightarrow Z \in \{\{⟨1, A⟩, ⟨2, B⟩\}, \{⟨1, X⟩, ⟨2, Y⟩\}\})$

Metamath Proof Explorer

Theorem prelrrx2b

Proof