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

Theorem dfac5lem1 8890
Description: Lemma for dfac5 8895. (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 3774 . . . 4 (𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ (𝑣 ∈ ({𝑤} × 𝑤) ∧ 𝑣𝑦))
2 elxp 5091 . . . . . 6 (𝑣 ∈ ({𝑤} × 𝑤) ↔ ∃𝑡𝑔(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
3 excom 2039 . . . . . 6 (∃𝑡𝑔(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ↔ ∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
42, 3bitri 264 . . . . 5 (𝑣 ∈ ({𝑤} × 𝑤) ↔ ∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
54anbi1i 730 . . . 4 ((𝑣 ∈ ({𝑤} × 𝑤) ∧ 𝑣𝑦) ↔ (∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦))
6 19.41vv 1912 . . . . 5 (∃𝑔𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ (∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦))
7 an32 838 . . . . . . . . 9 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑣𝑦) ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
8 eleq1 2686 . . . . . . . . . . 11 (𝑣 = ⟨𝑡, 𝑔⟩ → (𝑣𝑦 ↔ ⟨𝑡, 𝑔⟩ ∈ 𝑦))
98pm5.32i 668 . . . . . . . . . 10 ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑣𝑦) ↔ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))
10 velsn 4164 . . . . . . . . . . 11 (𝑡 ∈ {𝑤} ↔ 𝑡 = 𝑤)
1110anbi1i 730 . . . . . . . . . 10 ((𝑡 ∈ {𝑤} ∧ 𝑔𝑤) ↔ (𝑡 = 𝑤𝑔𝑤))
129, 11anbi12i 732 . . . . . . . . 9 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑣𝑦) ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ↔ ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ∧ (𝑡 = 𝑤𝑔𝑤)))
13 an4 864 . . . . . . . . . 10 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ∧ (𝑡 = 𝑤𝑔𝑤)) ↔ ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑡 = 𝑤) ∧ (⟨𝑡, 𝑔⟩ ∈ 𝑦𝑔𝑤)))
14 ancom 466 . . . . . . . . . . 11 ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑡 = 𝑤) ↔ (𝑡 = 𝑤𝑣 = ⟨𝑡, 𝑔⟩))
15 ancom 466 . . . . . . . . . . 11 ((⟨𝑡, 𝑔⟩ ∈ 𝑦𝑔𝑤) ↔ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))
1614, 15anbi12i 732 . . . . . . . . . 10 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑡 = 𝑤) ∧ (⟨𝑡, 𝑔⟩ ∈ 𝑦𝑔𝑤)) ↔ ((𝑡 = 𝑤𝑣 = ⟨𝑡, 𝑔⟩) ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦)))
17 anass 680 . . . . . . . . . 10 (((𝑡 = 𝑤𝑣 = ⟨𝑡, 𝑔⟩) ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦)) ↔ (𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
1813, 16, 173bitri 286 . . . . . . . . 9 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ∧ (𝑡 = 𝑤𝑔𝑤)) ↔ (𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
197, 12, 183bitri 286 . . . . . . . 8 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ (𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
2019exbii 1771 . . . . . . 7 (∃𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
21 vex 3189 . . . . . . . 8 𝑤 ∈ V
22 opeq1 4370 . . . . . . . . . 10 (𝑡 = 𝑤 → ⟨𝑡, 𝑔⟩ = ⟨𝑤, 𝑔⟩)
2322eqeq2d 2631 . . . . . . . . 9 (𝑡 = 𝑤 → (𝑣 = ⟨𝑡, 𝑔⟩ ↔ 𝑣 = ⟨𝑤, 𝑔⟩))
2422eleq1d 2683 . . . . . . . . . 10 (𝑡 = 𝑤 → (⟨𝑡, 𝑔⟩ ∈ 𝑦 ↔ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
2524anbi2d 739 . . . . . . . . 9 (𝑡 = 𝑤 → ((𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ↔ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
2623, 25anbi12d 746 . . . . . . . 8 (𝑡 = 𝑤 → ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦)) ↔ (𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))))
2721, 26ceqsexv 3228 . . . . . . 7 (∃𝑡(𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))) ↔ (𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
2820, 27bitri 264 . . . . . 6 (∃𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ (𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
2928exbii 1771 . . . . 5 (∃𝑔𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ∃𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
306, 29bitr3i 266 . . . 4 ((∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ∃𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
311, 5, 303bitri 286 . . 3 (𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
3231eubii 2491 . 2 (∃!𝑣 𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃!𝑣𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
3321euop2 4934 . 2 (∃!𝑣𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)) ↔ ∃!𝑔(𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
3432, 33bitri 264 1 (∃!𝑣 𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃!𝑔(𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1987  ∃!weu 2469  cin 3554  {csn 4148  cop 4154   × cxp 5072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-opab 4674  df-xp 5080
This theorem is referenced by:  dfac5lem5  8894
  Copyright terms: Public domain W3C validator