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

Theorem dfac5lem2 8985
Description: Lemma for dfac5 8989. (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 4477 . . 3 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))}
32eleq2i 2722 . 2 (⟨𝑤, 𝑔⟩ ∈ 𝐴 ↔ ⟨𝑤, 𝑔⟩ ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))})
4 eluniab 4479 . . 3 (⟨𝑤, 𝑔⟩ ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))))
5 r19.42v 3121 . . . . 5 (∃𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)))
6 anass 682 . . . . 5 (((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡)) ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))))
75, 6bitr2i 265 . . . 4 ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
87exbii 1814 . . 3 (∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑢𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
9 rexcom4 3256 . . . 4 (∃𝑡𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
10 df-rex 2947 . . . 4 (∃𝑡𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
119, 10bitr3i 266 . . 3 (∃𝑢𝑡 ((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
124, 8, 113bitri 286 . 2 (⟨𝑤, 𝑔⟩ ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
13 ancom 465 . . . . . . . . 9 (((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅)))
14 ne0i 3954 . . . . . . . . . . 11 (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅)
1514pm4.71i 665 . . . . . . . . . 10 (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅))
1615anbi2i 730 . . . . . . . . 9 ((𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅)))
1713, 16bitr4i 267 . . . . . . . 8 (((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
1817exbii 1814 . . . . . . 7 (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
19 snex 4938 . . . . . . . . 9 {𝑡} ∈ V
20 vex 3234 . . . . . . . . 9 𝑡 ∈ V
2119, 20xpex 7004 . . . . . . . 8 ({𝑡} × 𝑡) ∈ V
22 eleq2 2719 . . . . . . . 8 (𝑢 = ({𝑡} × 𝑡) → (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
2321, 22ceqsexv 3273 . . . . . . 7 (∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
2418, 23bitri 264 . . . . . 6 (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
2524anbi2i 730 . . . . 5 ((𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
26 opelxp 5180 . . . . . . 7 (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑤 ∈ {𝑡} ∧ 𝑔𝑡))
27 velsn 4226 . . . . . . . . 9 (𝑤 ∈ {𝑡} ↔ 𝑤 = 𝑡)
28 equcom 1991 . . . . . . . . 9 (𝑤 = 𝑡𝑡 = 𝑤)
2927, 28bitri 264 . . . . . . . 8 (𝑤 ∈ {𝑡} ↔ 𝑡 = 𝑤)
3029anbi1i 731 . . . . . . 7 ((𝑤 ∈ {𝑡} ∧ 𝑔𝑡) ↔ (𝑡 = 𝑤𝑔𝑡))
3126, 30bitri 264 . . . . . 6 (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑡 = 𝑤𝑔𝑡))
3231anbi2i 730 . . . . 5 ((𝑡 ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)) ↔ (𝑡 ∧ (𝑡 = 𝑤𝑔𝑡)))
33 an12 855 . . . . 5 ((𝑡 ∧ (𝑡 = 𝑤𝑔𝑡)) ↔ (𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)))
3425, 32, 333bitri 286 . . . 4 ((𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)))
3534exbii 1814 . . 3 (∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)))
36 vex 3234 . . . 4 𝑤 ∈ V
37 elequ1 2037 . . . . 5 (𝑡 = 𝑤 → (𝑡𝑤))
38 eleq2 2719 . . . . 5 (𝑡 = 𝑤 → (𝑔𝑡𝑔𝑤))
3937, 38anbi12d 747 . . . 4 (𝑡 = 𝑤 → ((𝑡𝑔𝑡) ↔ (𝑤𝑔𝑤)))
4036, 39ceqsexv 3273 . . 3 (∃𝑡(𝑡 = 𝑤 ∧ (𝑡𝑔𝑡)) ↔ (𝑤𝑔𝑤))
4135, 40bitri 264 . 2 (∃𝑡(𝑡 ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑤𝑔𝑤))
423, 12, 413bitri 286 1 (⟨𝑤, 𝑔⟩ ∈ 𝐴 ↔ (𝑤𝑔𝑤))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1523  wex 1744  wcel 2030  {cab 2637  wne 2823  wrex 2942  c0 3948  {csn 4210  cop 4216   cuni 4468   × cxp 5141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-opab 4746  df-xp 5149  df-rel 5150
This theorem is referenced by:  dfac5lem5  8988
  Copyright terms: Public domain W3C validator