Theorem dfac5lem2 9811

Description: Lemma for dfac5 9815. (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

Step	Hyp	Ref	Expression
1		dfac5lem.1	. . . 4 ⊢ 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}
2	1	unieqi 4849	. . 3 ⊢ ∪ 𝐴 = ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}
3	2	eleq2i 2830	. 2 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ 𝐴 ↔ ⟨𝑤, 𝑔⟩ ∈ ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))})
4		eluniab 4851	. . 3 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))))
5		r19.42v 3276	. . . . 5 ⊢ (∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)))
6		anass 468	. . . . 5 ⊢ (((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))))
7	5, 6	bitr2i 275	. . . 4 ⊢ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
8	7	exbii 1851	. . 3 ⊢ (∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑢∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
9		rexcom4 3179	. . . 4 ⊢ (∃𝑡 ∈ ℎ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
10		df-rex 3069	. . . 4 ⊢ (∃𝑡 ∈ ℎ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
11	9, 10	bitr3i 276	. . 3 ⊢ (∃𝑢∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
12	4, 8, 11	3bitri 296	. 2 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
13		ancom 460	. . . . . . . . 9 ⊢ (((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅)))
14		ne0i 4265	. . . . . . . . . . 11 ⊢ (⟨𝑤, 𝑔⟩ ∈ 𝑢 → 𝑢 ≠ ∅)
15	14	pm4.71i 559	. . . . . . . . . 10 ⊢ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅))
16	15	anbi2i 622	. . . . . . . . 9 ⊢ ((𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅)))
17	13, 16	bitr4i 277	. . . . . . . 8 ⊢ (((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
18	17	exbii 1851	. . . . . . 7 ⊢ (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
19		snex 5349	. . . . . . . . 9 ⊢ {𝑡} ∈ V
20		vex 3426	. . . . . . . . 9 ⊢ 𝑡 ∈ V
21	19, 20	xpex 7581	. . . . . . . 8 ⊢ ({𝑡} × 𝑡) ∈ V
22		eleq2 2827	. . . . . . . 8 ⊢ (𝑢 = ({𝑡} × 𝑡) → (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
23	21, 22	ceqsexv 3469	. . . . . . 7 ⊢ (∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
24	18, 23	bitri 274	. . . . . 6 ⊢ (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
25	24	anbi2i 622	. . . . 5 ⊢ ((𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 ∈ ℎ ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
26		opelxp 5616	. . . . . . 7 ⊢ (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑤 ∈ {𝑡} ∧ 𝑔 ∈ 𝑡))
27		velsn 4574	. . . . . . . . 9 ⊢ (𝑤 ∈ {𝑡} ↔ 𝑤 = 𝑡)
28		equcom 2022	. . . . . . . . 9 ⊢ (𝑤 = 𝑡 ↔ 𝑡 = 𝑤)
29	27, 28	bitri 274	. . . . . . . 8 ⊢ (𝑤 ∈ {𝑡} ↔ 𝑡 = 𝑤)
30	29	anbi1i 623	. . . . . . 7 ⊢ ((𝑤 ∈ {𝑡} ∧ 𝑔 ∈ 𝑡) ↔ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡))
31	26, 30	bitri 274	. . . . . 6 ⊢ (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡))
32	31	anbi2i 622	. . . . 5 ⊢ ((𝑡 ∈ ℎ ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)) ↔ (𝑡 ∈ ℎ ∧ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡)))
33		an12 641	. . . . 5 ⊢ ((𝑡 ∈ ℎ ∧ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡)) ↔ (𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)))
34	25, 32, 33	3bitri 296	. . . 4 ⊢ ((𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)))
35	34	exbii 1851	. . 3 ⊢ (∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)))
36		vex 3426	. . . 4 ⊢ 𝑤 ∈ V
37		elequ1 2115	. . . . 5 ⊢ (𝑡 = 𝑤 → (𝑡 ∈ ℎ ↔ 𝑤 ∈ ℎ))
38		eleq2 2827	. . . . 5 ⊢ (𝑡 = 𝑤 → (𝑔 ∈ 𝑡 ↔ 𝑔 ∈ 𝑤))
39	37, 38	anbi12d 630	. . . 4 ⊢ (𝑡 = 𝑤 → ((𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤)))
40	36, 39	ceqsexv 3469	. . 3 ⊢ (∃𝑡(𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))
41	35, 40	bitri 274	. 2 ⊢ (∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))
42	3, 12, 41	3bitri 296	1 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ 𝐴 ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  {cab 2715   ≠ wne 2942  ∃wrex 3064  ∅c0 4253  {csn 4558  ⟨cop 4564  ∪ cuni 4836   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-opab 5133  df-xp 5586  df-rel 5587

This theorem is referenced by:  dfac5lem5  9814