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

Theorem dfac5lem1 9146
Description: Lemma for dfac5 9151. (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 3947 . . . 4 (𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ (𝑣 ∈ ({𝑤} × 𝑤) ∧ 𝑣𝑦))
2 elxp 5271 . . . . . 6 (𝑣 ∈ ({𝑤} × 𝑤) ↔ ∃𝑡𝑔(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
3 excom 2198 . . . . . 6 (∃𝑡𝑔(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ↔ ∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
42, 3bitri 264 . . . . 5 (𝑣 ∈ ({𝑤} × 𝑤) ↔ ∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
54anbi1i 610 . . . 4 ((𝑣 ∈ ({𝑤} × 𝑤) ∧ 𝑣𝑦) ↔ (∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦))
6 19.41vv 2030 . . . . 5 (∃𝑔𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ (∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦))
7 an32 625 . . . . . . . . 9 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑣𝑦) ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
8 eleq1 2838 . . . . . . . . . . 11 (𝑣 = ⟨𝑡, 𝑔⟩ → (𝑣𝑦 ↔ ⟨𝑡, 𝑔⟩ ∈ 𝑦))
98pm5.32i 564 . . . . . . . . . 10 ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑣𝑦) ↔ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))
10 velsn 4332 . . . . . . . . . . 11 (𝑡 ∈ {𝑤} ↔ 𝑡 = 𝑤)
1110anbi1i 610 . . . . . . . . . 10 ((𝑡 ∈ {𝑤} ∧ 𝑔𝑤) ↔ (𝑡 = 𝑤𝑔𝑤))
129, 11anbi12i 612 . . . . . . . . 9 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑣𝑦) ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ↔ ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ∧ (𝑡 = 𝑤𝑔𝑤)))
13 an4 635 . . . . . . . . . 10 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ∧ (𝑡 = 𝑤𝑔𝑤)) ↔ ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑡 = 𝑤) ∧ (⟨𝑡, 𝑔⟩ ∈ 𝑦𝑔𝑤)))
14 ancom 452 . . . . . . . . . . 11 ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑡 = 𝑤) ↔ (𝑡 = 𝑤𝑣 = ⟨𝑡, 𝑔⟩))
15 ancom 452 . . . . . . . . . . 11 ((⟨𝑡, 𝑔⟩ ∈ 𝑦𝑔𝑤) ↔ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))
1614, 15anbi12i 612 . . . . . . . . . 10 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑡 = 𝑤) ∧ (⟨𝑡, 𝑔⟩ ∈ 𝑦𝑔𝑤)) ↔ ((𝑡 = 𝑤𝑣 = ⟨𝑡, 𝑔⟩) ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦)))
17 anass 459 . . . . . . . . . 10 (((𝑡 = 𝑤𝑣 = ⟨𝑡, 𝑔⟩) ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦)) ↔ (𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
1813, 16, 173bitri 286 . . . . . . . . 9 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ∧ (𝑡 = 𝑤𝑔𝑤)) ↔ (𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
197, 12, 183bitri 286 . . . . . . . 8 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ (𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
2019exbii 1924 . . . . . . 7 (∃𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
21 vex 3354 . . . . . . . 8 𝑤 ∈ V
22 opeq1 4539 . . . . . . . . . 10 (𝑡 = 𝑤 → ⟨𝑡, 𝑔⟩ = ⟨𝑤, 𝑔⟩)
2322eqeq2d 2781 . . . . . . . . 9 (𝑡 = 𝑤 → (𝑣 = ⟨𝑡, 𝑔⟩ ↔ 𝑣 = ⟨𝑤, 𝑔⟩))
2422eleq1d 2835 . . . . . . . . . 10 (𝑡 = 𝑤 → (⟨𝑡, 𝑔⟩ ∈ 𝑦 ↔ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
2524anbi2d 614 . . . . . . . . 9 (𝑡 = 𝑤 → ((𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ↔ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
2623, 25anbi12d 616 . . . . . . . 8 (𝑡 = 𝑤 → ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦)) ↔ (𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))))
2721, 26ceqsexv 3394 . . . . . . 7 (∃𝑡(𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))) ↔ (𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
2820, 27bitri 264 . . . . . 6 (∃𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ (𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
2928exbii 1924 . . . . 5 (∃𝑔𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ∃𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
306, 29bitr3i 266 . . . 4 ((∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ∃𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
311, 5, 303bitri 286 . . 3 (𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
3231eubii 2640 . 2 (∃!𝑣 𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃!𝑣𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
3321euop2 5105 . 2 (∃!𝑣𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)) ↔ ∃!𝑔(𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
3432, 33bitri 264 1 (∃!𝑣 𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃!𝑔(𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382   = wceq 1631  wex 1852  wcel 2145  ∃!weu 2618  cin 3722  {csn 4316  cop 4322   × cxp 5247
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-opab 4847  df-xp 5255
This theorem is referenced by:  dfac5lem5  9150
  Copyright terms: Public domain W3C validator