Theorem dfac5lem2 9880

Description: Lemma for dfac5 9884. (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 4852	. . 3 ⊢ ∪ 𝐴 = ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}
3	2	eleq2i 2830	. 2 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ 𝐴 ↔ ⟨𝑤, 𝑔⟩ ∈ ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))})
4		eluniab 4854	. . 3 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))))
5		r19.42v 3279	. . . . 5 ⊢ (∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)))
6		anass 469	. . . . 5 ⊢ (((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))))
7	5, 6	bitr2i 275	. . . 4 ⊢ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
8	7	exbii 1850	. . 3 ⊢ (∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑢∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
9		rexcom4 3233	. . . 4 ⊢ (∃𝑡 ∈ ℎ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
10		df-rex 3070	. . . 4 ⊢ (∃𝑡 ∈ ℎ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
11	9, 10	bitr3i 276	. . 3 ⊢ (∃𝑢∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
12	4, 8, 11	3bitri 297	. 2 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
13		ancom 461	. . . . . . . . 9 ⊢ (((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅)))
14		ne0i 4268	. . . . . . . . . . 11 ⊢ (⟨𝑤, 𝑔⟩ ∈ 𝑢 → 𝑢 ≠ ∅)
15	14	pm4.71i 560	. . . . . . . . . 10 ⊢ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅))
16	15	anbi2i 623	. . . . . . . . 9 ⊢ ((𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅)))
17	13, 16	bitr4i 277	. . . . . . . 8 ⊢ (((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
18	17	exbii 1850	. . . . . . 7 ⊢ (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
19		snex 5354	. . . . . . . . 9 ⊢ {𝑡} ∈ V
20		vex 3436	. . . . . . . . 9 ⊢ 𝑡 ∈ V
21	19, 20	xpex 7603	. . . . . . . 8 ⊢ ({𝑡} × 𝑡) ∈ V
22		eleq2 2827	. . . . . . . 8 ⊢ (𝑢 = ({𝑡} × 𝑡) → (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
23	21, 22	ceqsexv 3479	. . . . . . 7 ⊢ (∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
24	18, 23	bitri 274	. . . . . 6 ⊢ (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
25	24	anbi2i 623	. . . . 5 ⊢ ((𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 ∈ ℎ ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
26		opelxp 5625	. . . . . . 7 ⊢ (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑤 ∈ {𝑡} ∧ 𝑔 ∈ 𝑡))
27		velsn 4577	. . . . . . . . 9 ⊢ (𝑤 ∈ {𝑡} ↔ 𝑤 = 𝑡)
28		equcom 2021	. . . . . . . . 9 ⊢ (𝑤 = 𝑡 ↔ 𝑡 = 𝑤)
29	27, 28	bitri 274	. . . . . . . 8 ⊢ (𝑤 ∈ {𝑡} ↔ 𝑡 = 𝑤)
30	29	anbi1i 624	. . . . . . 7 ⊢ ((𝑤 ∈ {𝑡} ∧ 𝑔 ∈ 𝑡) ↔ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡))
31	26, 30	bitri 274	. . . . . 6 ⊢ (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡))
32	31	anbi2i 623	. . . . 5 ⊢ ((𝑡 ∈ ℎ ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)) ↔ (𝑡 ∈ ℎ ∧ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡)))
33		an12 642	. . . . 5 ⊢ ((𝑡 ∈ ℎ ∧ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡)) ↔ (𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)))
34	25, 32, 33	3bitri 297	. . . 4 ⊢ ((𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)))
35	34	exbii 1850	. . 3 ⊢ (∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)))
36		vex 3436	. . . 4 ⊢ 𝑤 ∈ V
37		elequ1 2113	. . . . 5 ⊢ (𝑡 = 𝑤 → (𝑡 ∈ ℎ ↔ 𝑤 ∈ ℎ))
38		eleq2 2827	. . . . 5 ⊢ (𝑡 = 𝑤 → (𝑔 ∈ 𝑡 ↔ 𝑔 ∈ 𝑤))
39	37, 38	anbi12d 631	. . . 4 ⊢ (𝑡 = 𝑤 → ((𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤)))
40	36, 39	ceqsexv 3479	. . 3 ⊢ (∃𝑡(𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))
41	35, 40	bitri 274	. 2 ⊢ (∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))
42	3, 12, 41	3bitri 297	1 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ 𝐴 ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106  {cab 2715   ≠ wne 2943  ∃wrex 3065  ∅c0 4256  {csn 4561  ⟨cop 4567  ∪ cuni 4839   × cxp 5587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-opab 5137  df-xp 5595  df-rel 5596

This theorem is referenced by:  dfac5lem5  9883