Theorem dfac5lem2 10203

Description: Lemma for dfac5 10207. (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 4879	. . 3 ⊢ ∪ 𝐴 = ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}
3	2	eleq2i 2853	. 2 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ 𝐴 ↔ ⟨𝑤, 𝑔⟩ ∈ ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))})
4		eluniab 4881	. . 3 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))))
5		r19.42v 3195	. . . . 5 ⊢ (∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)))
6		anass 474	. . . . 5 ⊢ (((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))))
7	5, 6	bitr2i 279	. . . 4 ⊢ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
8	7	exbii 1881	. . 3 ⊢ (∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑢∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
9		rexcom4 3290	. . . 4 ⊢ (∃𝑡 ∈ ℎ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
10		df-rex 3088	. . . 4 ⊢ (∃𝑡 ∈ ℎ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
11	9, 10	bitr3i 280	. . 3 ⊢ (∃𝑢∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
12	4, 8, 11	3bitri 300	. 2 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
13		ancom 466	. . . . . . . . 9 ⊢ (((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅)))
14		ne0i 4287	. . . . . . . . . . 11 ⊢ (⟨𝑤, 𝑔⟩ ∈ 𝑢 → 𝑢 ≠ ∅)
15	14	pm4.71i 569	. . . . . . . . . 10 ⊢ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅))
16	15	anbi2i 635	. . . . . . . . 9 ⊢ ((𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅)))
17	13, 16	bitr4i 281	. . . . . . . 8 ⊢ (((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
18	17	exbii 1881	. . . . . . 7 ⊢ (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
19		vsnex 5393	. . . . . . . . 9 ⊢ {𝑡} ∈ V
20		vex 3455	. . . . . . . . 9 ⊢ 𝑡 ∈ V
21	19, 20	xpex 7767	. . . . . . . 8 ⊢ ({𝑡} × 𝑡) ∈ V
22		eleq2 2850	. . . . . . . 8 ⊢ (𝑢 = ({𝑡} × 𝑡) → (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
23	21, 22	ceqsexv 3499	. . . . . . 7 ⊢ (∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
24	18, 23	bitri 278	. . . . . 6 ⊢ (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
25	24	anbi2i 635	. . . . 5 ⊢ ((𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 ∈ ℎ ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
26		opelxp 5687	. . . . . . 7 ⊢ (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑤 ∈ {𝑡} ∧ 𝑔 ∈ 𝑡))
27		velsn 4600	. . . . . . . . 9 ⊢ (𝑤 ∈ {𝑡} ↔ 𝑤 = 𝑡)
28		equcom 2051	. . . . . . . . 9 ⊢ (𝑤 = 𝑡 ↔ 𝑡 = 𝑤)
29	27, 28	bitri 278	. . . . . . . 8 ⊢ (𝑤 ∈ {𝑡} ↔ 𝑡 = 𝑤)
30	29	anbi1i 636	. . . . . . 7 ⊢ ((𝑤 ∈ {𝑡} ∧ 𝑔 ∈ 𝑡) ↔ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡))
31	26, 30	bitri 278	. . . . . 6 ⊢ (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡))
32	31	anbi2i 635	. . . . 5 ⊢ ((𝑡 ∈ ℎ ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)) ↔ (𝑡 ∈ ℎ ∧ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡)))
33		an12 658	. . . . 5 ⊢ ((𝑡 ∈ ℎ ∧ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡)) ↔ (𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)))
34	25, 32, 33	3bitri 300	. . . 4 ⊢ ((𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)))
35	34	exbii 1881	. . 3 ⊢ (∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)))
36		vex 3455	. . . 4 ⊢ 𝑤 ∈ V
37		elequ1 2152	. . . . 5 ⊢ (𝑡 = 𝑤 → (𝑡 ∈ ℎ ↔ 𝑤 ∈ ℎ))
38		eleq2 2850	. . . . 5 ⊢ (𝑡 = 𝑤 → (𝑔 ∈ 𝑡 ↔ 𝑔 ∈ 𝑤))
39	37, 38	anbi12d 644	. . . 4 ⊢ (𝑡 = 𝑤 → ((𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤)))
40	36, 39	ceqsexv 3499	. . 3 ⊢ (∃𝑡(𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))
41	35, 40	bitri 278	. 2 ⊢ (∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))
42	3, 12, 41	3bitri 300	1 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ 𝐴 ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2739   ≠ wne 2956  ∃wrex 3087  ∅c0 4279  {csn 4584  ⟨cop 4590  ∪ cuni 4867   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-opab 5168  df-xp 5657  df-rel 5658

This theorem is used by:  dfac5lem5  10206