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

Theorem dfac5lem2 8830
 Description: Lemma for dfac5 8834. (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 4381 . . 3 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))}
32eleq2i 2680 . 2 (⟨𝑤, 𝑔⟩ ∈ 𝐴 ↔ ⟨𝑤, 𝑔⟩ ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))})
4 eluniab 4383 . . 3 (⟨𝑤, 𝑔⟩ ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))))
5 r19.42v 3073 . . . . 5 (∃𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)))
6 anass 679 . . . . 5 (((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))))
75, 6bitr2i 264 . . . 4 ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
87exbii 1764 . . 3 (∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑢𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
9 rexcom4 3198 . . . 4 (∃𝑡𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
10 df-rex 2902 . . . 4 (∃𝑡𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
119, 10bitr3i 265 . . 3 (∃𝑢𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
124, 8, 113bitri 285 . 2 (⟨𝑤, 𝑔⟩ ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
13 ancom 465 . . . . . . . . 9 (((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅)))
14 ne0i 3880 . . . . . . . . . . 11 (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅)
1514pm4.71i 662 . . . . . . . . . 10 (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅))
1615anbi2i 726 . . . . . . . . 9 ((𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅)))
1713, 16bitr4i 266 . . . . . . . 8 (((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
1817exbii 1764 . . . . . . 7 (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
19 snex 4835 . . . . . . . . 9 {𝑡} ∈ V
20 vex 3176 . . . . . . . . 9 𝑡 ∈ V
2119, 20xpex 6860 . . . . . . . 8 ({𝑡} × 𝑡) ∈ V
22 eleq2 2677 . . . . . . . 8 (𝑢 = ({𝑡} × 𝑡) → (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
2321, 22ceqsexv 3215 . . . . . . 7 (∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
2418, 23bitri 263 . . . . . 6 (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
2524anbi2i 726 . . . . 5 ((𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
26 opelxp 5070 . . . . . . 7 (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑤 ∈ {𝑡} ∧ 𝑔𝑡))
27 velsn 4141 . . . . . . . . 9 (𝑤 ∈ {𝑡} ↔ 𝑤 = 𝑡)
28 equcom 1932 . . . . . . . . 9 (𝑤 = 𝑡𝑡 = 𝑤)
2927, 28bitri 263 . . . . . . . 8 (𝑤 ∈ {𝑡} ↔ 𝑡 = 𝑤)
3029anbi1i 727 . . . . . . 7 ((𝑤 ∈ {𝑡} ∧ 𝑔𝑡) ↔ (𝑡 = 𝑤𝑔𝑡))
3126, 30bitri 263 . . . . . 6 (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑡 = 𝑤𝑔𝑡))
3231anbi2i 726 . . . . 5 ((𝑡 ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)) ↔ (𝑡 ∧ (𝑡 = 𝑤𝑔𝑡)))
33 an12 834 . . . . 5 ((𝑡 ∧ (𝑡 = 𝑤𝑔𝑡)) ↔ (𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)))
3425, 32, 333bitri 285 . . . 4 ((𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)))
3534exbii 1764 . . 3 (∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)))
36 vex 3176 . . . 4 𝑤 ∈ V
37 elequ1 1984 . . . . 5 (𝑡 = 𝑤 → (𝑡𝑤))
38 eleq2 2677 . . . . 5 (𝑡 = 𝑤 → (𝑔𝑡𝑔𝑤))
3937, 38anbi12d 743 . . . 4 (𝑡 = 𝑤 → ((𝑡𝑔𝑡) ↔ (𝑤𝑔𝑤)))
4036, 39ceqsexv 3215 . . 3 (∃𝑡(𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)) ↔ (𝑤𝑔𝑤))
4135, 40bitri 263 . 2 (∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑤𝑔𝑤))
423, 12, 413bitri 285 1 (⟨𝑤, 𝑔⟩ ∈ 𝐴 ↔ (𝑤𝑔𝑤))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∃wrex 2897  ∅c0 3874  {csn 4125  ⟨cop 4131  ∪ cuni 4372   × cxp 5036 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-opab 4644  df-xp 5044  df-rel 5045 This theorem is referenced by:  dfac5lem5  8833
 Copyright terms: Public domain W3C validator