Metamath Proof Explorer

Theorem 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 ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝜑 ↔ 𝜒 ) )
Assertion opreu2reuALT ( ( ∃! 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝜒 ∧ ∃! 𝑏 ∈ 𝐵 ∃ 𝑎 ∈ 𝐴 𝜒 ) → ∃! 𝑝 ∈ ( 𝐴 × 𝐵 ) 𝜑 )

Proof

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