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

Theorem dfac5lem1 9538
Description: Lemma for dfac5 9543. (Contributed by NM, 12-Apr-2004.)
Assertion
Ref Expression
dfac5lem1 (∃!𝑣 𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃!𝑔(𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
Distinct variable group:   𝑤,𝑣,𝑦,𝑔

Proof of Theorem dfac5lem1
Dummy variable 𝑡 is distinct from all other variables.
StepHypRef Expression
1 elin 3924 . . . 4 (𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ (𝑣 ∈ ({𝑤} × 𝑤) ∧ 𝑣𝑦))
2 elxp 5555 . . . . . 6 (𝑣 ∈ ({𝑤} × 𝑤) ↔ ∃𝑡𝑔(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
3 excom 2169 . . . . . 6 (∃𝑡𝑔(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ↔ ∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
42, 3bitri 278 . . . . 5 (𝑣 ∈ ({𝑤} × 𝑤) ↔ ∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
54anbi1i 626 . . . 4 ((𝑣 ∈ ({𝑤} × 𝑤) ∧ 𝑣𝑦) ↔ (∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦))
6 19.41vv 1951 . . . . 5 (∃𝑔𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ (∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦))
7 an32 645 . . . . . . . . 9 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑣𝑦) ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
8 eleq1 2901 . . . . . . . . . . 11 (𝑣 = ⟨𝑡, 𝑔⟩ → (𝑣𝑦 ↔ ⟨𝑡, 𝑔⟩ ∈ 𝑦))
98pm5.32i 578 . . . . . . . . . 10 ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑣𝑦) ↔ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))
10 velsn 4555 . . . . . . . . . . 11 (𝑡 ∈ {𝑤} ↔ 𝑡 = 𝑤)
1110anbi1i 626 . . . . . . . . . 10 ((𝑡 ∈ {𝑤} ∧ 𝑔𝑤) ↔ (𝑡 = 𝑤𝑔𝑤))
129, 11anbi12i 629 . . . . . . . . 9 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑣𝑦) ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ↔ ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ∧ (𝑡 = 𝑤𝑔𝑤)))
13 an4 655 . . . . . . . . . 10 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ∧ (𝑡 = 𝑤𝑔𝑤)) ↔ ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑡 = 𝑤) ∧ (⟨𝑡, 𝑔⟩ ∈ 𝑦𝑔𝑤)))
14 ancom 464 . . . . . . . . . . 11 ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑡 = 𝑤) ↔ (𝑡 = 𝑤𝑣 = ⟨𝑡, 𝑔⟩))
15 ancom 464 . . . . . . . . . . 11 ((⟨𝑡, 𝑔⟩ ∈ 𝑦𝑔𝑤) ↔ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))
1614, 15anbi12i 629 . . . . . . . . . 10 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑡 = 𝑤) ∧ (⟨𝑡, 𝑔⟩ ∈ 𝑦𝑔𝑤)) ↔ ((𝑡 = 𝑤𝑣 = ⟨𝑡, 𝑔⟩) ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦)))
17 anass 472 . . . . . . . . . 10 (((𝑡 = 𝑤𝑣 = ⟨𝑡, 𝑔⟩) ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦)) ↔ (𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
1813, 16, 173bitri 300 . . . . . . . . 9 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ∧ (𝑡 = 𝑤𝑔𝑤)) ↔ (𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
197, 12, 183bitri 300 . . . . . . . 8 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ (𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
2019exbii 1849 . . . . . . 7 (∃𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
21 opeq1 4776 . . . . . . . . . 10 (𝑡 = 𝑤 → ⟨𝑡, 𝑔⟩ = ⟨𝑤, 𝑔⟩)
2221eqeq2d 2833 . . . . . . . . 9 (𝑡 = 𝑤 → (𝑣 = ⟨𝑡, 𝑔⟩ ↔ 𝑣 = ⟨𝑤, 𝑔⟩))
2321eleq1d 2898 . . . . . . . . . 10 (𝑡 = 𝑤 → (⟨𝑡, 𝑔⟩ ∈ 𝑦 ↔ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
2423anbi2d 631 . . . . . . . . 9 (𝑡 = 𝑤 → ((𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ↔ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
2522, 24anbi12d 633 . . . . . . . 8 (𝑡 = 𝑤 → ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦)) ↔ (𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))))
2625equsexvw 2011 . . . . . . 7 (∃𝑡(𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))) ↔ (𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
2720, 26bitri 278 . . . . . 6 (∃𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ (𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
2827exbii 1849 . . . . 5 (∃𝑔𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ∃𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
296, 28bitr3i 280 . . . 4 ((∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ∃𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
301, 5, 293bitri 300 . . 3 (𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
3130eubii 2669 . 2 (∃!𝑣 𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃!𝑣𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
32 vex 3472 . . 3 𝑤 ∈ V
3332euop2 5379 . 2 (∃!𝑣𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)) ↔ ∃!𝑔(𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
3431, 33bitri 278 1 (∃!𝑣 𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃!𝑔(𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399   = wceq 1538  wex 1781  wcel 2114  ∃!weu 2652  cin 3907  {csn 4539  cop 4545   × cxp 5530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-opab 5105  df-xp 5538
This theorem is referenced by:  dfac5lem5  9542
  Copyright terms: Public domain W3C validator