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

Theorem dfac5lem2 10119
Description: Lemma for dfac5 10123. (Contributed by NM, 12-Apr-2004.)
Hypothesis
Ref Expression
dfac5lem.1 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))}
Assertion
Ref Expression
dfac5lem2 (⟨𝑤, 𝑔⟩ ∈ 𝐴 ↔ (𝑤𝑔𝑤))
Distinct variable groups:   𝑤,𝑢,𝑡,,𝑔   𝑤,𝐴,𝑔
Allowed substitution hints:   𝐴(𝑢,𝑡,)

Proof of Theorem dfac5lem2
StepHypRef Expression
1 dfac5lem.1 . . . 4 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))}
21unieqi 4922 . . 3 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))}
32eleq2i 2826 . 2 (⟨𝑤, 𝑔⟩ ∈ 𝐴 ↔ ⟨𝑤, 𝑔⟩ ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))})
4 eluniab 4924 . . 3 (⟨𝑤, 𝑔⟩ ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))))
5 r19.42v 3191 . . . . 5 (∃𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)))
6 anass 470 . . . . 5 (((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))))
75, 6bitr2i 276 . . . 4 ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
87exbii 1851 . . 3 (∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑢𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
9 rexcom4 3286 . . . 4 (∃𝑡𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
10 df-rex 3072 . . . 4 (∃𝑡𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
119, 10bitr3i 277 . . 3 (∃𝑢𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
124, 8, 113bitri 297 . 2 (⟨𝑤, 𝑔⟩ ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
13 ancom 462 . . . . . . . . 9 (((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅)))
14 ne0i 4335 . . . . . . . . . . 11 (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅)
1514pm4.71i 561 . . . . . . . . . 10 (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅))
1615anbi2i 624 . . . . . . . . 9 ((𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅)))
1713, 16bitr4i 278 . . . . . . . 8 (((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
1817exbii 1851 . . . . . . 7 (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
19 vsnex 5430 . . . . . . . . 9 {𝑡} ∈ V
20 vex 3479 . . . . . . . . 9 𝑡 ∈ V
2119, 20xpex 7740 . . . . . . . 8 ({𝑡} × 𝑡) ∈ V
22 eleq2 2823 . . . . . . . 8 (𝑢 = ({𝑡} × 𝑡) → (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
2321, 22ceqsexv 3526 . . . . . . 7 (∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
2418, 23bitri 275 . . . . . 6 (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
2524anbi2i 624 . . . . 5 ((𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
26 opelxp 5713 . . . . . . 7 (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑤 ∈ {𝑡} ∧ 𝑔𝑡))
27 velsn 4645 . . . . . . . . 9 (𝑤 ∈ {𝑡} ↔ 𝑤 = 𝑡)
28 equcom 2022 . . . . . . . . 9 (𝑤 = 𝑡𝑡 = 𝑤)
2927, 28bitri 275 . . . . . . . 8 (𝑤 ∈ {𝑡} ↔ 𝑡 = 𝑤)
3029anbi1i 625 . . . . . . 7 ((𝑤 ∈ {𝑡} ∧ 𝑔𝑡) ↔ (𝑡 = 𝑤𝑔𝑡))
3126, 30bitri 275 . . . . . 6 (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑡 = 𝑤𝑔𝑡))
3231anbi2i 624 . . . . 5 ((𝑡 ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)) ↔ (𝑡 ∧ (𝑡 = 𝑤𝑔𝑡)))
33 an12 644 . . . . 5 ((𝑡 ∧ (𝑡 = 𝑤𝑔𝑡)) ↔ (𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)))
3425, 32, 333bitri 297 . . . 4 ((𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)))
3534exbii 1851 . . 3 (∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)))
36 vex 3479 . . . 4 𝑤 ∈ V
37 elequ1 2114 . . . . 5 (𝑡 = 𝑤 → (𝑡𝑤))
38 eleq2 2823 . . . . 5 (𝑡 = 𝑤 → (𝑔𝑡𝑔𝑤))
3937, 38anbi12d 632 . . . 4 (𝑡 = 𝑤 → ((𝑡𝑔𝑡) ↔ (𝑤𝑔𝑤)))
4036, 39ceqsexv 3526 . . 3 (∃𝑡(𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)) ↔ (𝑤𝑔𝑤))
4135, 40bitri 275 . 2 (∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑤𝑔𝑤))
423, 12, 413bitri 297 1 (⟨𝑤, 𝑔⟩ ∈ 𝐴 ↔ (𝑤𝑔𝑤))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397   = wceq 1542  wex 1782  wcel 2107  {cab 2710  wne 2941  wrex 3071  c0 4323  {csn 4629  cop 4635   cuni 4909   × cxp 5675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-opab 5212  df-xp 5683  df-rel 5684
This theorem is referenced by:  dfac5lem5  10122
  Copyright terms: Public domain W3C validator