MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  copsexgw Structured version   Visualization version   GIF version

Theorem copsexgw 5481
Description: Version of copsexg 5482 with a disjoint variable condition, which does not require ax-13 2363. (Contributed by Gino Giotto, 26-Jan-2024.)
Assertion
Ref Expression
copsexgw (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
Distinct variable group:   𝑥,𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem copsexgw
Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3470 . . . 4 𝑥 ∈ V
2 vex 3470 . . . 4 𝑦 ∈ V
31, 2eqvinop 5478 . . 3 (𝐴 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑧𝑤(𝐴 = ⟨𝑧, 𝑤⟩ ∧ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
4 19.8a 2166 . . . . . . . . 9 ((⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
5419.8ad 2167 . . . . . . . 8 ((⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))
65ex 412 . . . . . . 7 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 → ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
7 vex 3470 . . . . . . . . 9 𝑧 ∈ V
8 vex 3470 . . . . . . . . 9 𝑤 ∈ V
97, 8opth 5467 . . . . . . . 8 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝑧 = 𝑥𝑤 = 𝑦))
109anbi1i 623 . . . . . . . . . 10 ((⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑))
11102exbii 1843 . . . . . . . . 9 (∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑))
12 nfe1 2139 . . . . . . . . . . 11 𝑥𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))
13 19.8a 2166 . . . . . . . . . . . . . . . 16 ((𝑤 = 𝑦𝜑) → ∃𝑦(𝑤 = 𝑦𝜑))
1413anim2i 616 . . . . . . . . . . . . . . 15 ((𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
1514anassrs 467 . . . . . . . . . . . . . 14 (((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
1615eximi 1829 . . . . . . . . . . . . 13 (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑦(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
17 biidd 262 . . . . . . . . . . . . . 14 (∀𝑦 𝑦 = 𝑥 → ((𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) ↔ (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
1817drex1v 2360 . . . . . . . . . . . . 13 (∀𝑦 𝑦 = 𝑥 → (∃𝑦(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) ↔ ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
1916, 18imbitrid 243 . . . . . . . . . . . 12 (∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
20 anass 468 . . . . . . . . . . . . . . 15 (((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) ↔ (𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)))
2120exbii 1842 . . . . . . . . . . . . . 14 (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) ↔ ∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)))
22 19.40 1881 . . . . . . . . . . . . . . 15 (∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)) → (∃𝑦 𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
23 nfvd 1910 . . . . . . . . . . . . . . . . 17 (¬ ∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦 𝑧 = 𝑥)
242319.9d 2188 . . . . . . . . . . . . . . . 16 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦 𝑧 = 𝑥𝑧 = 𝑥))
2524anim1d 610 . . . . . . . . . . . . . . 15 (¬ ∀𝑦 𝑦 = 𝑥 → ((∃𝑦 𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
2622, 25syl5 34 . . . . . . . . . . . . . 14 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦(𝑧 = 𝑥 ∧ (𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
2721, 26biimtrid 241 . . . . . . . . . . . . 13 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → (𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
28 19.8a 2166 . . . . . . . . . . . . 13 ((𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
2927, 28syl6 35 . . . . . . . . . . . 12 (¬ ∀𝑦 𝑦 = 𝑥 → (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))))
3019, 29pm2.61i 182 . . . . . . . . . . 11 (∃𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
3112, 30exlimi 2202 . . . . . . . . . 10 (∃𝑥𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)))
32 euequ 2583 . . . . . . . . . . . . . 14 ∃!𝑥 𝑥 = 𝑧
33 equcom 2013 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧𝑧 = 𝑥)
3433eubii 2571 . . . . . . . . . . . . . 14 (∃!𝑥 𝑥 = 𝑧 ↔ ∃!𝑥 𝑧 = 𝑥)
3532, 34mpbi 229 . . . . . . . . . . . . 13 ∃!𝑥 𝑧 = 𝑥
36 eupick 2621 . . . . . . . . . . . . 13 ((∃!𝑥 𝑧 = 𝑥 ∧ ∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑))) → (𝑧 = 𝑥 → ∃𝑦(𝑤 = 𝑦𝜑)))
3735, 36mpan 687 . . . . . . . . . . . 12 (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → (𝑧 = 𝑥 → ∃𝑦(𝑤 = 𝑦𝜑)))
3837com12 32 . . . . . . . . . . 11 (𝑧 = 𝑥 → (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → ∃𝑦(𝑤 = 𝑦𝜑)))
39 euequ 2583 . . . . . . . . . . . . . 14 ∃!𝑦 𝑦 = 𝑤
40 equcom 2013 . . . . . . . . . . . . . . 15 (𝑦 = 𝑤𝑤 = 𝑦)
4140eubii 2571 . . . . . . . . . . . . . 14 (∃!𝑦 𝑦 = 𝑤 ↔ ∃!𝑦 𝑤 = 𝑦)
4239, 41mpbi 229 . . . . . . . . . . . . 13 ∃!𝑦 𝑤 = 𝑦
43 eupick 2621 . . . . . . . . . . . . 13 ((∃!𝑦 𝑤 = 𝑦 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → (𝑤 = 𝑦𝜑))
4442, 43mpan 687 . . . . . . . . . . . 12 (∃𝑦(𝑤 = 𝑦𝜑) → (𝑤 = 𝑦𝜑))
4544com12 32 . . . . . . . . . . 11 (𝑤 = 𝑦 → (∃𝑦(𝑤 = 𝑦𝜑) → 𝜑))
4638, 45sylan9 507 . . . . . . . . . 10 ((𝑧 = 𝑥𝑤 = 𝑦) → (∃𝑥(𝑧 = 𝑥 ∧ ∃𝑦(𝑤 = 𝑦𝜑)) → 𝜑))
4731, 46syl5 34 . . . . . . . . 9 ((𝑧 = 𝑥𝑤 = 𝑦) → (∃𝑥𝑦((𝑧 = 𝑥𝑤 = 𝑦) ∧ 𝜑) → 𝜑))
4811, 47biimtrid 241 . . . . . . . 8 ((𝑧 = 𝑥𝑤 = 𝑦) → (∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝜑))
499, 48sylbi 216 . . . . . . 7 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝜑))
506, 49impbid 211 . . . . . 6 (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
51 eqeq1 2728 . . . . . . 7 (𝐴 = ⟨𝑧, 𝑤⟩ → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
5251anbi1d 629 . . . . . . . . 9 (𝐴 = ⟨𝑧, 𝑤⟩ → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
53522exbidv 1919 . . . . . . . 8 (𝐴 = ⟨𝑧, 𝑤⟩ → (∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
5453bibi2d 342 . . . . . . 7 (𝐴 = ⟨𝑧, 𝑤⟩ → ((𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) ↔ (𝜑 ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
5551, 54imbi12d 344 . . . . . 6 (𝐴 = ⟨𝑧, 𝑤⟩ → ((𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))) ↔ (⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))))
5650, 55mpbiri 258 . . . . 5 (𝐴 = ⟨𝑧, 𝑤⟩ → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
5756adantr 480 . . . 4 ((𝐴 = ⟨𝑧, 𝑤⟩ ∧ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
5857exlimivv 1927 . . 3 (∃𝑧𝑤(𝐴 = ⟨𝑧, 𝑤⟩ ∧ ⟨𝑧, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
593, 58sylbi 216 . 2 (𝐴 = ⟨𝑥, 𝑦⟩ → (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))))
6059pm2.43i 52 1 (𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wal 1531   = wceq 1533  wex 1773  ∃!weu 2554  cop 4627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pr 5418
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628
This theorem is referenced by:  copsex2t  5483  copsex2gOLD  5485  mosubopt  5501  opabidw  5515  brabgaf  32309  copsex2d  36511
  Copyright terms: Public domain W3C validator