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

Theorem dfac5lem2 8892
Description: Lemma for dfac5 8896. (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 4416 . . 3 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))}
32eleq2i 2696 . 2 (⟨𝑤, 𝑔⟩ ∈ 𝐴 ↔ ⟨𝑤, 𝑔⟩ ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))})
4 eluniab 4418 . . 3 (⟨𝑤, 𝑔⟩ ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))))
5 r19.42v 3089 . . . . 5 (∃𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)))
6 anass 680 . . . . 5 (((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))))
75, 6bitr2i 265 . . . 4 ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
87exbii 1772 . . 3 (∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑢𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
9 rexcom4 3216 . . . 4 (∃𝑡𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
10 df-rex 2918 . . . 4 (∃𝑡𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
119, 10bitr3i 266 . . 3 (∃𝑢𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
124, 8, 113bitri 286 . 2 (⟨𝑤, 𝑔⟩ ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
13 ancom 466 . . . . . . . . 9 (((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅)))
14 ne0i 3902 . . . . . . . . . . 11 (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅)
1514pm4.71i 663 . . . . . . . . . 10 (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅))
1615anbi2i 729 . . . . . . . . 9 ((𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅)))
1713, 16bitr4i 267 . . . . . . . 8 (((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
1817exbii 1772 . . . . . . 7 (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
19 snex 4874 . . . . . . . . 9 {𝑡} ∈ V
20 vex 3194 . . . . . . . . 9 𝑡 ∈ V
2119, 20xpex 6916 . . . . . . . 8 ({𝑡} × 𝑡) ∈ V
22 eleq2 2693 . . . . . . . 8 (𝑢 = ({𝑡} × 𝑡) → (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
2321, 22ceqsexv 3233 . . . . . . 7 (∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
2418, 23bitri 264 . . . . . 6 (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
2524anbi2i 729 . . . . 5 ((𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
26 opelxp 5111 . . . . . . 7 (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑤 ∈ {𝑡} ∧ 𝑔𝑡))
27 velsn 4169 . . . . . . . . 9 (𝑤 ∈ {𝑡} ↔ 𝑤 = 𝑡)
28 equcom 1947 . . . . . . . . 9 (𝑤 = 𝑡𝑡 = 𝑤)
2927, 28bitri 264 . . . . . . . 8 (𝑤 ∈ {𝑡} ↔ 𝑡 = 𝑤)
3029anbi1i 730 . . . . . . 7 ((𝑤 ∈ {𝑡} ∧ 𝑔𝑡) ↔ (𝑡 = 𝑤𝑔𝑡))
3126, 30bitri 264 . . . . . 6 (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑡 = 𝑤𝑔𝑡))
3231anbi2i 729 . . . . 5 ((𝑡 ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)) ↔ (𝑡 ∧ (𝑡 = 𝑤𝑔𝑡)))
33 an12 837 . . . . 5 ((𝑡 ∧ (𝑡 = 𝑤𝑔𝑡)) ↔ (𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)))
3425, 32, 333bitri 286 . . . 4 ((𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)))
3534exbii 1772 . . 3 (∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)))
36 vex 3194 . . . 4 𝑤 ∈ V
37 elequ1 1999 . . . . 5 (𝑡 = 𝑤 → (𝑡𝑤))
38 eleq2 2693 . . . . 5 (𝑡 = 𝑤 → (𝑔𝑡𝑔𝑤))
3937, 38anbi12d 746 . . . 4 (𝑡 = 𝑤 → ((𝑡𝑔𝑡) ↔ (𝑤𝑔𝑤)))
4036, 39ceqsexv 3233 . . 3 (∃𝑡(𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)) ↔ (𝑤𝑔𝑤))
4135, 40bitri 264 . 2 (∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑤𝑔𝑤))
423, 12, 413bitri 286 1 (⟨𝑤, 𝑔⟩ ∈ 𝐴 ↔ (𝑤𝑔𝑤))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1992  {cab 2612  wne 2796  wrex 2913  c0 3896  {csn 4153  cop 4159   cuni 4407   × cxp 5077
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 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903
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 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-opab 4679  df-xp 5085  df-rel 5086
This theorem is referenced by:  dfac5lem5  8895
  Copyright terms: Public domain W3C validator