Theorem dfac5lem2 10037

Description: Lemma for dfac5 10042. (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 4850	. . 3 ⊢ ∪ 𝐴 = ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}
3	2	eleq2i 2831	. 2 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ 𝐴 ↔ ⟨𝑤, 𝑔⟩ ∈ ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))})
4		eluniab 4852	. . 3 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))))
5		r19.42v 3171	. . . . 5 ⊢ (∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)))
6		anass 469	. . . . 5 ⊢ (((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))))
7	5, 6	bitr2i 277	. . . 4 ⊢ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
8	7	exbii 1855	. . 3 ⊢ (∃𝑢(⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑢∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
9		rexcom4 3266	. . . 4 ⊢ (∃𝑡 ∈ ℎ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))
10		df-rex 3064	. . . 4 ⊢ (∃𝑡 ∈ ℎ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
11	9, 10	bitr3i 278	. . 3 ⊢ (∃𝑢∃𝑡 ∈ ℎ ((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
12	4, 8, 11	3bitri 298	. 2 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))))
13		ancom 461	. . . . . . . . 9 ⊢ (((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅)))
14		ne0i 4269	. . . . . . . . . . 11 ⊢ (⟨𝑤, 𝑔⟩ ∈ 𝑢 → 𝑢 ≠ ∅)
15	14	pm4.71i 564	. . . . . . . . . 10 ⊢ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅))
16	15	anbi2i 629	. . . . . . . . 9 ⊢ ((𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅)))
17	13, 16	bitr4i 279	. . . . . . . 8 ⊢ (((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
18	17	exbii 1855	. . . . . . 7 ⊢ (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢))
19		vsnex 5364	. . . . . . . . 9 ⊢ {𝑡} ∈ V
20		vex 3435	. . . . . . . . 9 ⊢ 𝑡 ∈ V
21	19, 20	xpex 7696	. . . . . . . 8 ⊢ ({𝑡} × 𝑡) ∈ V
22		eleq2 2828	. . . . . . . 8 ⊢ (𝑢 = ({𝑡} × 𝑡) → (⟨𝑤, 𝑔⟩ ∈ 𝑢 ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
23	21, 22	ceqsexv 3479	. . . . . . 7 ⊢ (∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ ⟨𝑤, 𝑔⟩ ∈ 𝑢) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
24	18, 23	bitri 276	. . . . . 6 ⊢ (∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡))
25	24	anbi2i 629	. . . . 5 ⊢ ((𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 ∈ ℎ ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)))
26		opelxp 5654	. . . . . . 7 ⊢ (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑤 ∈ {𝑡} ∧ 𝑔 ∈ 𝑡))
27		velsn 4571	. . . . . . . . 9 ⊢ (𝑤 ∈ {𝑡} ↔ 𝑤 = 𝑡)
28		equcom 2025	. . . . . . . . 9 ⊢ (𝑤 = 𝑡 ↔ 𝑡 = 𝑤)
29	27, 28	bitri 276	. . . . . . . 8 ⊢ (𝑤 ∈ {𝑡} ↔ 𝑡 = 𝑤)
30	29	anbi1i 630	. . . . . . 7 ⊢ ((𝑤 ∈ {𝑡} ∧ 𝑔 ∈ 𝑡) ↔ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡))
31	26, 30	bitri 276	. . . . . 6 ⊢ (⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡) ↔ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡))
32	31	anbi2i 629	. . . . 5 ⊢ ((𝑡 ∈ ℎ ∧ ⟨𝑤, 𝑔⟩ ∈ ({𝑡} × 𝑡)) ↔ (𝑡 ∈ ℎ ∧ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡)))
33		an12 651	. . . . 5 ⊢ ((𝑡 ∈ ℎ ∧ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡)) ↔ (𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)))
34	25, 32, 33	3bitri 298	. . . 4 ⊢ ((𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)))
35	34	exbii 1855	. . 3 ⊢ (∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)))
36		vex 3435	. . . 4 ⊢ 𝑤 ∈ V
37		elequ1 2126	. . . . 5 ⊢ (𝑡 = 𝑤 → (𝑡 ∈ ℎ ↔ 𝑤 ∈ ℎ))
38		eleq2 2828	. . . . 5 ⊢ (𝑡 = 𝑤 → (𝑔 ∈ 𝑡 ↔ 𝑔 ∈ 𝑤))
39	37, 38	anbi12d 638	. . . 4 ⊢ (𝑡 = 𝑤 → ((𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤)))
40	36, 39	ceqsexv 3479	. . 3 ⊢ (∃𝑡(𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))
41	35, 40	bitri 276	. 2 ⊢ (∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((⟨𝑤, 𝑔⟩ ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))
42	3, 12, 41	3bitri 298	1 ⊢ (⟨𝑤, 𝑔⟩ ∈ ∪ 𝐴 ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  {cab 2717   ≠ wne 2934  ∃wrex 3063  ∅c0 4261  {csn 4555  ⟨cop 4561  ∪ cuni 4838   × cxp 5616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-opab 5135  df-xp 5624  df-rel 5625

This theorem is referenced by:  dfac5lem5  10040