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

Theorem dfac5lem1 10148
Description: Lemma for dfac5 10153. (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 3960 . . . 4 (𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ (𝑣 ∈ ({𝑤} × 𝑤) ∧ 𝑣𝑦))
2 elxp 5701 . . . . . 6 (𝑣 ∈ ({𝑤} × 𝑤) ↔ ∃𝑡𝑔(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
3 excom 2151 . . . . . 6 (∃𝑡𝑔(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ↔ ∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
42, 3bitri 274 . . . . 5 (𝑣 ∈ ({𝑤} × 𝑤) ↔ ∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
54anbi1i 622 . . . 4 ((𝑣 ∈ ({𝑤} × 𝑤) ∧ 𝑣𝑦) ↔ (∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦))
6 19.41vv 1946 . . . . 5 (∃𝑔𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ (∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦))
7 an32 644 . . . . . . . . 9 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑣𝑦) ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
8 eleq1 2813 . . . . . . . . . . 11 (𝑣 = ⟨𝑡, 𝑔⟩ → (𝑣𝑦 ↔ ⟨𝑡, 𝑔⟩ ∈ 𝑦))
98pm5.32i 573 . . . . . . . . . 10 ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑣𝑦) ↔ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))
10 velsn 4646 . . . . . . . . . . 11 (𝑡 ∈ {𝑤} ↔ 𝑡 = 𝑤)
1110anbi1i 622 . . . . . . . . . 10 ((𝑡 ∈ {𝑤} ∧ 𝑔𝑤) ↔ (𝑡 = 𝑤𝑔𝑤))
129, 11anbi12i 626 . . . . . . . . 9 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑣𝑦) ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ↔ ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ∧ (𝑡 = 𝑤𝑔𝑤)))
13 an4 654 . . . . . . . . . 10 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ∧ (𝑡 = 𝑤𝑔𝑤)) ↔ ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑡 = 𝑤) ∧ (⟨𝑡, 𝑔⟩ ∈ 𝑦𝑔𝑤)))
14 ancom 459 . . . . . . . . . . 11 ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑡 = 𝑤) ↔ (𝑡 = 𝑤𝑣 = ⟨𝑡, 𝑔⟩))
15 ancom 459 . . . . . . . . . . 11 ((⟨𝑡, 𝑔⟩ ∈ 𝑦𝑔𝑤) ↔ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))
1614, 15anbi12i 626 . . . . . . . . . 10 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑡 = 𝑤) ∧ (⟨𝑡, 𝑔⟩ ∈ 𝑦𝑔𝑤)) ↔ ((𝑡 = 𝑤𝑣 = ⟨𝑡, 𝑔⟩) ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦)))
17 anass 467 . . . . . . . . . 10 (((𝑡 = 𝑤𝑣 = ⟨𝑡, 𝑔⟩) ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦)) ↔ (𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
1813, 16, 173bitri 296 . . . . . . . . 9 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ∧ (𝑡 = 𝑤𝑔𝑤)) ↔ (𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
197, 12, 183bitri 296 . . . . . . . 8 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ (𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
2019exbii 1842 . . . . . . 7 (∃𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
21 opeq1 4875 . . . . . . . . . 10 (𝑡 = 𝑤 → ⟨𝑡, 𝑔⟩ = ⟨𝑤, 𝑔⟩)
2221eqeq2d 2736 . . . . . . . . 9 (𝑡 = 𝑤 → (𝑣 = ⟨𝑡, 𝑔⟩ ↔ 𝑣 = ⟨𝑤, 𝑔⟩))
2321eleq1d 2810 . . . . . . . . . 10 (𝑡 = 𝑤 → (⟨𝑡, 𝑔⟩ ∈ 𝑦 ↔ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
2423anbi2d 628 . . . . . . . . 9 (𝑡 = 𝑤 → ((𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ↔ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
2522, 24anbi12d 630 . . . . . . . 8 (𝑡 = 𝑤 → ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦)) ↔ (𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))))
2625equsexvw 2000 . . . . . . 7 (∃𝑡(𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))) ↔ (𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
2720, 26bitri 274 . . . . . 6 (∃𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ (𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
2827exbii 1842 . . . . 5 (∃𝑔𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ∃𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
296, 28bitr3i 276 . . . 4 ((∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ∃𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
301, 5, 293bitri 296 . . 3 (𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
3130eubii 2573 . 2 (∃!𝑣 𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃!𝑣𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
32 vex 3465 . . 3 𝑤 ∈ V
3332euop2 5514 . 2 (∃!𝑣𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)) ↔ ∃!𝑔(𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
3431, 33bitri 274 1 (∃!𝑣 𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃!𝑔(𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394   = wceq 1533  wex 1773  wcel 2098  ∃!weu 2556  cin 3943  {csn 4630  cop 4636   × cxp 5676
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-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-opab 5212  df-xp 5684
This theorem is referenced by:  dfac5lem5  10152
  Copyright terms: Public domain W3C validator