opreu2reuALT

Description: Correspondence between uniqueness of ordered pairs and double restricted existential uniqueness quantification. Alternate proof of one direction only, use opreu2reurex instead. (Contributed by Thierry Arnoux, 4-Jul-2023) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	opsbc2ie.a	$⊢ p = ⟨a, b⟩ \to (φ \leftrightarrow χ)$
	Assertion	opreu2reuALT	$⊢ (\exists! a \in A \exists b \in B χ \land \exists! b \in B \exists a \in A χ) \to \exists! p \in (A \times B) φ$

Proof

Step	Hyp	Ref	Expression
1		opsbc2ie.a	$⊢ p = ⟨a, b⟩ \to (φ \leftrightarrow χ)$
2		2reu4	$⊢ (\exists! a \in A \exists b \in B χ \land \exists! b \in B \exists a \in A χ) \leftrightarrow (\exists a \in A \exists b \in B χ \land \exists x \in A \exists y \in B \forall a \in A \forall b \in B (χ \to (a = x \land b = y)))$
3		simpllr	$⊢ (((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \to x \in A$
4		simplr	$⊢ (((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \to y \in B$
5		opelxpi	$⊢ (x \in A \land y \in B) \to ⟨x, y⟩ \in (A \times B)$
6	3 4 5	syl2anc	$⊢ (((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \to ⟨x, y⟩ \in (A \times B)$
7		nfre1	$⊢ Ⅎ a \exists a \in A \exists b \in B χ$
8		nfv	$⊢ Ⅎ a x \in A$
9	7 8	nfan	$⊢ Ⅎ a (\exists a \in A \exists b \in B χ \land x \in A)$
10		nfv	$⊢ Ⅎ a y \in B$
11	9 10	nfan	$⊢ Ⅎ a ((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B)$
12		nfra1	$⊢ Ⅎ a \forall a \in A \forall b \in B (χ \to (a = x \land b = y))$
13	11 12	nfan	$⊢ Ⅎ a (((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y)))$
14		nfcv	$⊢ \underline{Ⅎ} a y$
15		nfsbc1v	$⊢ Ⅎ a \underset{˙}{[} x / a \underset{˙}{]} χ$
16	14 15	nfsbc	$⊢ Ⅎ a \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} χ$
17		nfcv	$⊢ \underline{Ⅎ} b A$
18		nfre1	$⊢ Ⅎ b \exists b \in B χ$
19	17 18	nfrex	$⊢ Ⅎ b \exists a \in A \exists b \in B χ$
20		nfv	$⊢ Ⅎ b x \in A$
21	19 20	nfan	$⊢ Ⅎ b (\exists a \in A \exists b \in B χ \land x \in A)$
22		nfv	$⊢ Ⅎ b y \in B$
23	21 22	nfan	$⊢ Ⅎ b ((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B)$
24		nfra1	$⊢ Ⅎ b \forall b \in B (χ \to (a = x \land b = y))$
25	17 24	nfral	$⊢ Ⅎ b \forall a \in A \forall b \in B (χ \to (a = x \land b = y))$
26	23 25	nfan	$⊢ Ⅎ b (((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y)))$
27		nfv	$⊢ Ⅎ b a \in A$
28	26 27	nfan	$⊢ Ⅎ b ((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land a \in A)$
29	28 18	nfan	$⊢ Ⅎ b (((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land a \in A) \land \exists b \in B χ)$
30		nfsbc1v	$⊢ Ⅎ b \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} χ$
31		rspa	$⊢ (\forall a \in A \forall b \in B (χ \to (a = x \land b = y)) \land a \in A) \to \forall b \in B (χ \to (a = x \land b = y))$
32	31	ad5ant23	$⊢ ((((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land a \in A) \land b \in B) \land χ) \to \forall b \in B (χ \to (a = x \land b = y))$
33		simplr	$⊢ ((((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land a \in A) \land b \in B) \land χ) \to b \in B$
34		simpr	$⊢ ((((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land a \in A) \land b \in B) \land χ) \to χ$
35		rspa	$⊢ (\forall b \in B (χ \to (a = x \land b = y)) \land b \in B) \to (χ \to (a = x \land b = y))$
36	35	imp	$⊢ ((\forall b \in B (χ \to (a = x \land b = y)) \land b \in B) \land χ) \to (a = x \land b = y)$
37	32 33 34 36	syl21anc	$⊢ ((((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land a \in A) \land b \in B) \land χ) \to (a = x \land b = y)$
38	37	simprd	$⊢ ((((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land a \in A) \land b \in B) \land χ) \to b = y$
39	37	simpld	$⊢ ((((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land a \in A) \land b \in B) \land χ) \to a = x$
40		sbceq1a	$⊢ a = x \to (χ \leftrightarrow \underset{˙}{[} x / a \underset{˙}{]} χ)$
41	40	biimpa	$⊢ (a = x \land χ) \to \underset{˙}{[} x / a \underset{˙}{]} χ$
42	39 34 41	syl2anc	$⊢ ((((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land a \in A) \land b \in B) \land χ) \to \underset{˙}{[} x / a \underset{˙}{]} χ$
43		sbceq1a	$⊢ b = y \to (\underset{˙}{[} x / a \underset{˙}{]} χ \leftrightarrow \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} χ)$
44	43	biimpa	$⊢ (b = y \land \underset{˙}{[} x / a \underset{˙}{]} χ) \to \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} χ$
45	38 42 44	syl2anc	$⊢ ((((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land a \in A) \land b \in B) \land χ) \to \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} χ$
46	45	adantllr	$⊢ (((((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land a \in A) \land \exists b \in B χ) \land b \in B) \land χ) \to \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} χ$
47		simpr	$⊢ (((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land a \in A) \land \exists b \in B χ) \to \exists b \in B χ$
48	29 30 46 47	r19.29af2	$⊢ (((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land a \in A) \land \exists b \in B χ) \to \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} χ$
49		simplll	$⊢ (((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \to \exists a \in A \exists b \in B χ$
50	13 16 48 49	r19.29af2	$⊢ (((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \to \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} χ$
51		1st2nd2	$⊢ p \in (A \times B) \to p = ⟨1^{st} (p), 2^{nd} (p)⟩$
52	51	ad2antlr	$⊢ (((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ) \to p = ⟨1^{st} (p), 2^{nd} (p)⟩$
53		nfv	$⊢ Ⅎ a p \in (A \times B)$
54	13 53	nfan	$⊢ Ⅎ a ((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B))$
55		nfv	$⊢ Ⅎ a φ$
56	54 55	nfan	$⊢ Ⅎ a (((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ)$
57		nfv	$⊢ Ⅎ b p \in (A \times B)$
58	26 57	nfan	$⊢ Ⅎ b ((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B))$
59		nfv	$⊢ Ⅎ b φ$
60	58 59	nfan	$⊢ Ⅎ b (((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ)$
61		nfv	$⊢ Ⅎ a (φ \to (1^{st} (p) = x \land 2^{nd} (p) = y))$
62		nfv	$⊢ Ⅎ b (φ \to (1^{st} (p) = x \land 2^{nd} (p) = y))$
63		xp1st	$⊢ p \in (A \times B) \to 1^{st} (p) \in A$
64	63	ad2antlr	$⊢ (((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ) \to 1^{st} (p) \in A$
65		xp2nd	$⊢ p \in (A \times B) \to 2^{nd} (p) \in B$
66	65	ad2antlr	$⊢ (((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ) \to 2^{nd} (p) \in B$
67		eqcom	$⊢ 1^{st} (p) = a \leftrightarrow a = 1^{st} (p)$
68		eqcom	$⊢ 2^{nd} (p) = b \leftrightarrow b = 2^{nd} (p)$
69		eqopi	$⊢ (p \in (A \times B) \land (1^{st} (p) = a \land 2^{nd} (p) = b)) \to p = ⟨a, b⟩$
70	69 1	syl	$⊢ (p \in (A \times B) \land (1^{st} (p) = a \land 2^{nd} (p) = b)) \to (φ \leftrightarrow χ)$
71	70	bicomd	$⊢ (p \in (A \times B) \land (1^{st} (p) = a \land 2^{nd} (p) = b)) \to (χ \leftrightarrow φ)$
72	71	ancoms	$⊢ ((1^{st} (p) = a \land 2^{nd} (p) = b) \land p \in (A \times B)) \to (χ \leftrightarrow φ)$
73	72	ex	$⊢ (1^{st} (p) = a \land 2^{nd} (p) = b) \to (p \in (A \times B) \to (χ \leftrightarrow φ))$
74	67 68 73	syl2anbr	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to (p \in (A \times B) \to (χ \leftrightarrow φ))$
75	74	impcom	$⊢ (p \in (A \times B) \land (a = 1^{st} (p) \land b = 2^{nd} (p))) \to (χ \leftrightarrow φ)$
76	75	ad4ant24	$⊢ ((((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ) \land (a = 1^{st} (p) \land b = 2^{nd} (p))) \to (χ \leftrightarrow φ)$
77		simpl	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to a = 1^{st} (p)$
78	77	eqeq1d	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to (a = x \leftrightarrow 1^{st} (p) = x)$
79		simpr	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to b = 2^{nd} (p)$
80	79	eqeq1d	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to (b = y \leftrightarrow 2^{nd} (p) = y)$
81	78 80	anbi12d	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to ((a = x \land b = y) \leftrightarrow (1^{st} (p) = x \land 2^{nd} (p) = y))$
82	81	adantl	$⊢ ((((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ) \land (a = 1^{st} (p) \land b = 2^{nd} (p))) \to ((a = x \land b = y) \leftrightarrow (1^{st} (p) = x \land 2^{nd} (p) = y))$
83	76 82	imbi12d	$⊢ ((((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ) \land (a = 1^{st} (p) \land b = 2^{nd} (p))) \to ((χ \to (a = x \land b = y)) \leftrightarrow (φ \to (1^{st} (p) = x \land 2^{nd} (p) = y)))$
84		simpllr	$⊢ (((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ) \to \forall a \in A \forall b \in B (χ \to (a = x \land b = y))$
85	56 60 61 62 64 66 83 84	rspc2daf	$⊢ (((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ) \to (φ \to (1^{st} (p) = x \land 2^{nd} (p) = y))$
86	85	com12	$⊢ φ \to ((((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ) \to (1^{st} (p) = x \land 2^{nd} (p) = y))$
87	86	anabsi7	$⊢ (((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ) \to (1^{st} (p) = x \land 2^{nd} (p) = y)$
88	87	simpld	$⊢ (((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ) \to 1^{st} (p) = x$
89	87	simprd	$⊢ (((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ) \to 2^{nd} (p) = y$
90	88 89	opeq12d	$⊢ (((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ) \to ⟨1^{st} (p), 2^{nd} (p)⟩ = ⟨x, y⟩$
91	52 90	eqtrd	$⊢ (((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \land φ) \to p = ⟨x, y⟩$
92	91	ex	$⊢ ((((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \land p \in (A \times B)) \to (φ \to p = ⟨x, y⟩)$
93	92	ralrimiva	$⊢ (((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \to \forall p \in (A \times B) (φ \to p = ⟨x, y⟩)$
94	6 50 93	3jca	$⊢ (((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \to (⟨x, y⟩ \in (A \times B) \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} χ \land \forall p \in (A \times B) (φ \to p = ⟨x, y⟩))$
95	1	opsbc2ie	$⊢ p = ⟨x, y⟩ \to (φ \leftrightarrow \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} χ)$
96	95	eqreu	$⊢ (⟨x, y⟩ \in (A \times B) \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} χ \land \forall p \in (A \times B) (φ \to p = ⟨x, y⟩)) \to \exists! p \in (A \times B) φ$
97	94 96	syl	$⊢ (((\exists a \in A \exists b \in B χ \land x \in A) \land y \in B) \land \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \to \exists! p \in (A \times B) φ$
98	97	r19.29ffa	$⊢ (\exists a \in A \exists b \in B χ \land \exists x \in A \exists y \in B \forall a \in A \forall b \in B (χ \to (a = x \land b = y))) \to \exists! p \in (A \times B) φ$
99	2 98	sylbi	$⊢ (\exists! a \in A \exists b \in B χ \land \exists! b \in B \exists a \in A χ) \to \exists! p \in (A \times B) φ$

Metamath Proof Explorer

Theorem opreu2reuALT

Proof