Theorem dfac5lem2 9569

Description: Lemma for dfac5 9573. (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 4804	. . 3 ⊢ ∪ 𝐴 = ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}
3	2	eleq2i 2842	. 2 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ 𝐴 ↔ ⟨𝑤, 𝑔⟩ ∈ ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))})
4		eluniab 4806	. . 3 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))))
5		r19.42v 3266	. . . . 5 ⊢ (∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)))
6		anass 473	. . . . 5 ⊢ (((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))))
7	5, 6	bitr2i 279	. . . 4 ⊢ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
8	7	exbii 1850	. . 3 ⊢ (∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑢∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
9		rexcom4 3175	. . . 4 ⊢ (∃𝑡 ∈ ℎ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
10		df-rex 3074	. . . 4 ⊢ (∃𝑡 ∈ ℎ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
11	9, 10	bitr3i 280	. . 3 ⊢ (∃𝑢∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
12	4, 8, 11	3bitri 301	. 2 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
13		ancom 465	. . . . . . . . 9 ⊢ (((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅)))
14		ne0i 4229	. . . . . . . . . . 11 ⊢ (⟨𝑤, 𝑔⟩ ∈ 𝑢 → 𝑢 ≠ ∅)
15	14	pm4.71i 564	. . . . . . . . . 10 ⊢ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅))
16	15	anbi2i 626	. . . . . . . . 9 ⊢ ((𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅)))
17	13, 16	bitr4i 281	. . . . . . . 8 ⊢ (((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
18	17	exbii 1850	. . . . . . 7 ⊢ (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
19		snex 5293	. . . . . . . . 9 ⊢ {𝑡} ∈ V
20		vex 3411	. . . . . . . . 9 ⊢ 𝑡 ∈ V
21	19, 20	xpex 7467	. . . . . . . 8 ⊢ ({𝑡} × 𝑡) ∈ V
22		eleq2 2839	. . . . . . . 8 ⊢ (𝑢 = ({𝑡} × 𝑡) → (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
23	21, 22	ceqsexv 3457	. . . . . . 7 ⊢ (∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
24	18, 23	bitri 278	. . . . . 6 ⊢ (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
25	24	anbi2i 626	. . . . 5 ⊢ ((𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 ∈ ℎ ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
26		opelxp 5553	. . . . . . 7 ⊢ (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑤 ∈ {𝑡} ∧ 𝑔 ∈ 𝑡))
27		velsn 4531	. . . . . . . . 9 ⊢ (𝑤 ∈ {𝑡} ↔ 𝑤 = 𝑡)
28		equcom 2026	. . . . . . . . 9 ⊢ (𝑤 = 𝑡 ↔ 𝑡 = 𝑤)
29	27, 28	bitri 278	. . . . . . . 8 ⊢ (𝑤 ∈ {𝑡} ↔ 𝑡 = 𝑤)
30	29	anbi1i 627	. . . . . . 7 ⊢ ((𝑤 ∈ {𝑡} ∧ 𝑔 ∈ 𝑡) ↔ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡))
31	26, 30	bitri 278	. . . . . 6 ⊢ (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡))
32	31	anbi2i 626	. . . . 5 ⊢ ((𝑡 ∈ ℎ ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)) ↔ (𝑡 ∈ ℎ ∧ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡)))
33		an12 645	. . . . 5 ⊢ ((𝑡 ∈ ℎ ∧ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡)) ↔ (𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)))
34	25, 32, 33	3bitri 301	. . . 4 ⊢ ((𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)))
35	34	exbii 1850	. . 3 ⊢ (∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)))
36		vex 3411	. . . 4 ⊢ 𝑤 ∈ V
37		elequ1 2119	. . . . 5 ⊢ (𝑡 = 𝑤 → (𝑡 ∈ ℎ ↔ 𝑤 ∈ ℎ))
38		eleq2 2839	. . . . 5 ⊢ (𝑡 = 𝑤 → (𝑔 ∈ 𝑡 ↔ 𝑔 ∈ 𝑤))
39	37, 38	anbi12d 634	. . . 4 ⊢ (𝑡 = 𝑤 → ((𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤)))
40	36, 39	ceqsexv 3457	. . 3 ⊢ (∃𝑡(𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))
41	35, 40	bitri 278	. 2 ⊢ (∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))
42	3, 12, 41	3bitri 301	1 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ 𝐴 ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1539  ∃wex 1782   ∈ wcel 2112  {cab 2736   ≠ wne 2949  ∃wrex 3069  ∅c0 4221  {csn 4515  ⟨cop 4521  ∪ cuni 4791   × cxp 5515

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-ne 2950  df-ral 3073  df-rex 3074  df-rab 3077  df-v 3409  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-op 4522  df-uni 4792  df-opab 5088  df-xp 5523  df-rel 5524

This theorem is referenced by:  dfac5lem5  9572