Metamath Proof Explorer


Theorem copsexgw

Description: Version of copsexg with a disjoint variable condition, which does not require ax-13 . (Contributed by Gino Giotto, 26-Jan-2024)

Ref Expression
Assertion copsexgw ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 vex 𝑥 ∈ V
2 vex 𝑦 ∈ V
3 1 2 eqvinop ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑧𝑤 ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
4 19.8a ( ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
5 4 19.8ad ( ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ∃ 𝑥𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
6 5 ex ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 → ∃ 𝑥𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
7 vex 𝑧 ∈ V
8 vex 𝑤 ∈ V
9 7 8 opth ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑧 = 𝑥𝑤 = 𝑦 ) )
10 9 anbi1i ( ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) ∧ 𝜑 ) )
11 10 2exbii ( ∃ 𝑥𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥𝑦 ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) ∧ 𝜑 ) )
12 nfe1 𝑥𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) )
13 19.8a ( ( 𝑤 = 𝑦𝜑 ) → ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) )
14 13 anim2i ( ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦𝜑 ) ) → ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) )
15 14 anassrs ( ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) ∧ 𝜑 ) → ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) )
16 15 eximi ( ∃ 𝑦 ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) ∧ 𝜑 ) → ∃ 𝑦 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) )
17 biidd ( ∀ 𝑦 𝑦 = 𝑥 → ( ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) ↔ ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) ) )
18 17 drex1v ( ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) ↔ ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) ) )
19 16 18 syl5ib ( ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) ∧ 𝜑 ) → ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) ) )
20 anass ( ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦𝜑 ) ) )
21 20 exbii ( ∃ 𝑦 ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦𝜑 ) ) )
22 19.40 ( ∃ 𝑦 ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦𝜑 ) ) → ( ∃ 𝑦 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) )
23 nfvd ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑦 𝑧 = 𝑥 )
24 23 19.9d ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 𝑧 = 𝑥𝑧 = 𝑥 ) )
25 24 anim1d ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ( ∃ 𝑦 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) → ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) ) )
26 22 25 syl5 ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦𝜑 ) ) → ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) ) )
27 21 26 syl5bi ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) ∧ 𝜑 ) → ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) ) )
28 19.8a ( ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) → ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) )
29 27 28 syl6 ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) ∧ 𝜑 ) → ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) ) )
30 19 29 pm2.61i ( ∃ 𝑦 ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) ∧ 𝜑 ) → ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) )
31 12 30 exlimi ( ∃ 𝑥𝑦 ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) ∧ 𝜑 ) → ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) )
32 euequ ∃! 𝑥 𝑥 = 𝑧
33 equcom ( 𝑥 = 𝑧𝑧 = 𝑥 )
34 33 eubii ( ∃! 𝑥 𝑥 = 𝑧 ↔ ∃! 𝑥 𝑧 = 𝑥 )
35 32 34 mpbi ∃! 𝑥 𝑧 = 𝑥
36 eupick ( ( ∃! 𝑥 𝑧 = 𝑥 ∧ ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) ) → ( 𝑧 = 𝑥 → ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) )
37 35 36 mpan ( ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) → ( 𝑧 = 𝑥 → ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) )
38 37 com12 ( 𝑧 = 𝑥 → ( ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) → ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) )
39 euequ ∃! 𝑦 𝑦 = 𝑤
40 equcom ( 𝑦 = 𝑤𝑤 = 𝑦 )
41 40 eubii ( ∃! 𝑦 𝑦 = 𝑤 ↔ ∃! 𝑦 𝑤 = 𝑦 )
42 39 41 mpbi ∃! 𝑦 𝑤 = 𝑦
43 eupick ( ( ∃! 𝑦 𝑤 = 𝑦 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) → ( 𝑤 = 𝑦𝜑 ) )
44 42 43 mpan ( ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) → ( 𝑤 = 𝑦𝜑 ) )
45 44 com12 ( 𝑤 = 𝑦 → ( ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) → 𝜑 ) )
46 38 45 sylan9 ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) → ( ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦𝜑 ) ) → 𝜑 ) )
47 31 46 syl5 ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) → ( ∃ 𝑥𝑦 ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) ∧ 𝜑 ) → 𝜑 ) )
48 11 47 syl5bi ( ( 𝑧 = 𝑥𝑤 = 𝑦 ) → ( ∃ 𝑥𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝜑 ) )
49 9 48 sylbi ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( ∃ 𝑥𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝜑 ) )
50 6 49 impbid ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
51 eqeq1 ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
52 51 anbi1d ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
53 52 2exbidv ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( ∃ 𝑥𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
54 53 bibi2d ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( 𝜑 ↔ ∃ 𝑥𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ( 𝜑 ↔ ∃ 𝑥𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) )
55 51 54 imbi12d ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) ↔ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) ) )
56 50 55 mpbiri ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) )
57 56 adantr ( ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) )
58 57 exlimivv ( ∃ 𝑧𝑤 ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) )
59 3 58 sylbi ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) )
60 59 pm2.43i ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )