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

Theorem dfac5lem1 9136
 Description: Lemma for dfac5 9141. (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 3939 . . . 4 (𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ (𝑣 ∈ ({𝑤} × 𝑤) ∧ 𝑣𝑦))
2 elxp 5288 . . . . . 6 (𝑣 ∈ ({𝑤} × 𝑤) ↔ ∃𝑡𝑔(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
3 excom 2191 . . . . . 6 (∃𝑡𝑔(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ↔ ∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
42, 3bitri 264 . . . . 5 (𝑣 ∈ ({𝑤} × 𝑤) ↔ ∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
54anbi1i 733 . . . 4 ((𝑣 ∈ ({𝑤} × 𝑤) ∧ 𝑣𝑦) ↔ (∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦))
6 19.41vv 2027 . . . . 5 (∃𝑔𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ (∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦))
7 an32 874 . . . . . . . . 9 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑣𝑦) ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)))
8 eleq1 2827 . . . . . . . . . . 11 (𝑣 = ⟨𝑡, 𝑔⟩ → (𝑣𝑦 ↔ ⟨𝑡, 𝑔⟩ ∈ 𝑦))
98pm5.32i 672 . . . . . . . . . 10 ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑣𝑦) ↔ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))
10 velsn 4337 . . . . . . . . . . 11 (𝑡 ∈ {𝑤} ↔ 𝑡 = 𝑤)
1110anbi1i 733 . . . . . . . . . 10 ((𝑡 ∈ {𝑤} ∧ 𝑔𝑤) ↔ (𝑡 = 𝑤𝑔𝑤))
129, 11anbi12i 735 . . . . . . . . 9 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑣𝑦) ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ↔ ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ∧ (𝑡 = 𝑤𝑔𝑤)))
13 an4 900 . . . . . . . . . 10 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ∧ (𝑡 = 𝑤𝑔𝑤)) ↔ ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑡 = 𝑤) ∧ (⟨𝑡, 𝑔⟩ ∈ 𝑦𝑔𝑤)))
14 ancom 465 . . . . . . . . . . 11 ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑡 = 𝑤) ↔ (𝑡 = 𝑤𝑣 = ⟨𝑡, 𝑔⟩))
15 ancom 465 . . . . . . . . . . 11 ((⟨𝑡, 𝑔⟩ ∈ 𝑦𝑔𝑤) ↔ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))
1614, 15anbi12i 735 . . . . . . . . . 10 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ 𝑡 = 𝑤) ∧ (⟨𝑡, 𝑔⟩ ∈ 𝑦𝑔𝑤)) ↔ ((𝑡 = 𝑤𝑣 = ⟨𝑡, 𝑔⟩) ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦)))
17 anass 684 . . . . . . . . . 10 (((𝑡 = 𝑤𝑣 = ⟨𝑡, 𝑔⟩) ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦)) ↔ (𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
1813, 16, 173bitri 286 . . . . . . . . 9 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ∧ (𝑡 = 𝑤𝑔𝑤)) ↔ (𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
197, 12, 183bitri 286 . . . . . . . 8 (((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ (𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
2019exbii 1923 . . . . . . 7 (∃𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))))
21 vex 3343 . . . . . . . 8 𝑤 ∈ V
22 opeq1 4553 . . . . . . . . . 10 (𝑡 = 𝑤 → ⟨𝑡, 𝑔⟩ = ⟨𝑤, 𝑔⟩)
2322eqeq2d 2770 . . . . . . . . 9 (𝑡 = 𝑤 → (𝑣 = ⟨𝑡, 𝑔⟩ ↔ 𝑣 = ⟨𝑤, 𝑔⟩))
2422eleq1d 2824 . . . . . . . . . 10 (𝑡 = 𝑤 → (⟨𝑡, 𝑔⟩ ∈ 𝑦 ↔ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
2524anbi2d 742 . . . . . . . . 9 (𝑡 = 𝑤 → ((𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦) ↔ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
2623, 25anbi12d 749 . . . . . . . 8 (𝑡 = 𝑤 → ((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦)) ↔ (𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))))
2721, 26ceqsexv 3382 . . . . . . 7 (∃𝑡(𝑡 = 𝑤 ∧ (𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑡, 𝑔⟩ ∈ 𝑦))) ↔ (𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
2820, 27bitri 264 . . . . . 6 (∃𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ (𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
2928exbii 1923 . . . . 5 (∃𝑔𝑡((𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ∃𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
306, 29bitr3i 266 . . . 4 ((∃𝑔𝑡(𝑣 = ⟨𝑡, 𝑔⟩ ∧ (𝑡 ∈ {𝑤} ∧ 𝑔𝑤)) ∧ 𝑣𝑦) ↔ ∃𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
311, 5, 303bitri 286 . . 3 (𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
3231eubii 2629 . 2 (∃!𝑣 𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃!𝑣𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)))
3321euop2 5122 . 2 (∃!𝑣𝑔(𝑣 = ⟨𝑤, 𝑔⟩ ∧ (𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦)) ↔ ∃!𝑔(𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
3432, 33bitri 264 1 (∃!𝑣 𝑣 ∈ (({𝑤} × 𝑤) ∩ 𝑦) ↔ ∃!𝑔(𝑔𝑤 ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑦))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 383   = wceq 1632  ∃wex 1853   ∈ wcel 2139  ∃!weu 2607   ∩ cin 3714  {csn 4321  ⟨cop 4327   × cxp 5264 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-opab 4865  df-xp 5272 This theorem is referenced by:  dfac5lem5  9140
 Copyright terms: Public domain W3C validator