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

Theorem dfac5lem2 9147
Description: Lemma for dfac5 9151. (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 4583 . . 3 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))}
32eleq2i 2842 . 2 (⟨𝑤, 𝑔⟩ ∈ 𝐴 ↔ ⟨𝑤, 𝑔⟩ ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))})
4 eluniab 4585 . . 3 (⟨𝑤, 𝑔⟩ ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))))
5 r19.42v 3240 . . . . 5 (∃𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)))
6 anass 459 . . . . 5 (((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))))
75, 6bitr2i 265 . . . 4 ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
87exbii 1924 . . 3 (∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑢𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
9 rexcom4 3377 . . . 4 (∃𝑡𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
10 df-rex 3067 . . . 4 (∃𝑡𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
119, 10bitr3i 266 . . 3 (∃𝑢𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
124, 8, 113bitri 286 . 2 (⟨𝑤, 𝑔⟩ ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
13 ancom 452 . . . . . . . . 9 (((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅)))
14 ne0i 4069 . . . . . . . . . . 11 (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅)
1514pm4.71i 549 . . . . . . . . . 10 (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅))
1615anbi2i 609 . . . . . . . . 9 ((𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅)))
1713, 16bitr4i 267 . . . . . . . 8 (((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
1817exbii 1924 . . . . . . 7 (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
19 snex 5036 . . . . . . . . 9 {𝑡} ∈ V
20 vex 3354 . . . . . . . . 9 𝑡 ∈ V
2119, 20xpex 7109 . . . . . . . 8 ({𝑡} × 𝑡) ∈ V
22 eleq2 2839 . . . . . . . 8 (𝑢 = ({𝑡} × 𝑡) → (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
2321, 22ceqsexv 3394 . . . . . . 7 (∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
2418, 23bitri 264 . . . . . 6 (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
2524anbi2i 609 . . . . 5 ((𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
26 opelxp 5286 . . . . . . 7 (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑤 ∈ {𝑡} ∧ 𝑔𝑡))
27 velsn 4332 . . . . . . . . 9 (𝑤 ∈ {𝑡} ↔ 𝑤 = 𝑡)
28 equcom 2103 . . . . . . . . 9 (𝑤 = 𝑡𝑡 = 𝑤)
2927, 28bitri 264 . . . . . . . 8 (𝑤 ∈ {𝑡} ↔ 𝑡 = 𝑤)
3029anbi1i 610 . . . . . . 7 ((𝑤 ∈ {𝑡} ∧ 𝑔𝑡) ↔ (𝑡 = 𝑤𝑔𝑡))
3126, 30bitri 264 . . . . . 6 (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑡 = 𝑤𝑔𝑡))
3231anbi2i 609 . . . . 5 ((𝑡 ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)) ↔ (𝑡 ∧ (𝑡 = 𝑤𝑔𝑡)))
33 an12 624 . . . . 5 ((𝑡 ∧ (𝑡 = 𝑤𝑔𝑡)) ↔ (𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)))
3425, 32, 333bitri 286 . . . 4 ((𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)))
3534exbii 1924 . . 3 (∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)))
36 vex 3354 . . . 4 𝑤 ∈ V
37 elequ1 2152 . . . . 5 (𝑡 = 𝑤 → (𝑡𝑤))
38 eleq2 2839 . . . . 5 (𝑡 = 𝑤 → (𝑔𝑡𝑔𝑤))
3937, 38anbi12d 616 . . . 4 (𝑡 = 𝑤 → ((𝑡𝑔𝑡) ↔ (𝑤𝑔𝑤)))
4036, 39ceqsexv 3394 . . 3 (∃𝑡(𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)) ↔ (𝑤𝑔𝑤))
4135, 40bitri 264 . 2 (∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑤𝑔𝑤))
423, 12, 413bitri 286 1 (⟨𝑤, 𝑔⟩ ∈ 𝐴 ↔ (𝑤𝑔𝑤))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382   = wceq 1631  wex 1852  wcel 2145  {cab 2757  wne 2943  wrex 3062  c0 4063  {csn 4316  cop 4322   cuni 4574   × 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-8 2147  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-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-opab 4847  df-xp 5255  df-rel 5256
This theorem is referenced by:  dfac5lem5  9150
  Copyright terms: Public domain W3C validator