dfac5lem2

		Ref	Expression
	Hypothesis	dfac5lem.1	$⊢ A = \{u \| (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)\}$
	Assertion	dfac5lem2	$⊢ ⟨w, g⟩ \in ⋃ A \leftrightarrow (w \in h \land g \in w)$

Proof

Step	Hyp	Ref	Expression
1		dfac5lem.1	$⊢ A = \{u \| (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)\}$
2	1	unieqi	$⊢ ⋃ A = ⋃ \{u \| (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)\}$
3	2	eleq2i	$⊢ ⟨w, g⟩ \in ⋃ A \leftrightarrow ⟨w, g⟩ \in ⋃ \{u \| (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)\}$
4		eluniab	$⊢ ⟨w, g⟩ \in ⋃ \{u \| (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)\} \leftrightarrow \exists u (⟨w, g⟩ \in u \land (u \neq \emptyset \land \exists t \in h u = \{t\} \times t))$
5		r19.42v	$⊢ \exists t \in h ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t) \leftrightarrow ((⟨w, g⟩ \in u \land u \neq \emptyset) \land \exists t \in h u = \{t\} \times t)$
6		anass	$⊢ ((⟨w, g⟩ \in u \land u \neq \emptyset) \land \exists t \in h u = \{t\} \times t) \leftrightarrow (⟨w, g⟩ \in u \land (u \neq \emptyset \land \exists t \in h u = \{t\} \times t))$
7	5 6	bitr2i	$⊢ (⟨w, g⟩ \in u \land (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)) \leftrightarrow \exists t \in h ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t)$
8	7	exbii	$⊢ \exists u (⟨w, g⟩ \in u \land (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)) \leftrightarrow \exists u \exists t \in h ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t)$
9		rexcom4	$⊢ \exists t \in h \exists u ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t) \leftrightarrow \exists u \exists t \in h ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t)$
10		df-rex	$⊢ \exists t \in h \exists u ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t) \leftrightarrow \exists t (t \in h \land \exists u ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t))$
11	9 10	bitr3i	$⊢ \exists u \exists t \in h ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t) \leftrightarrow \exists t (t \in h \land \exists u ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t))$
12	4 8 11	3bitri	$⊢ ⟨w, g⟩ \in ⋃ \{u \| (u \neq \emptyset \land \exists t \in h u = \{t\} \times t)\} \leftrightarrow \exists t (t \in h \land \exists u ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t))$
13		ancom	$⊢ ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t) \leftrightarrow (u = \{t\} \times t \land (⟨w, g⟩ \in u \land u \neq \emptyset))$
14		ne0i	$⊢ ⟨w, g⟩ \in u \to u \neq \emptyset$
15	14	pm4.71i	$⊢ ⟨w, g⟩ \in u \leftrightarrow (⟨w, g⟩ \in u \land u \neq \emptyset)$
16	15	anbi2i	$⊢ (u = \{t\} \times t \land ⟨w, g⟩ \in u) \leftrightarrow (u = \{t\} \times t \land (⟨w, g⟩ \in u \land u \neq \emptyset))$
17	13 16	bitr4i	$⊢ ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t) \leftrightarrow (u = \{t\} \times t \land ⟨w, g⟩ \in u)$
18	17	exbii	$⊢ \exists u ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t) \leftrightarrow \exists u (u = \{t\} \times t \land ⟨w, g⟩ \in u)$
19		snex	$⊢ \{t\} \in V$
20		vex	$⊢ t \in V$
21	19 20	xpex	$⊢ \{t\} \times t \in V$
22		eleq2	$⊢ u = \{t\} \times t \to (⟨w, g⟩ \in u \leftrightarrow ⟨w, g⟩ \in (\{t\} \times t))$
23	21 22	ceqsexv	$⊢ \exists u (u = \{t\} \times t \land ⟨w, g⟩ \in u) \leftrightarrow ⟨w, g⟩ \in (\{t\} \times t)$
24	18 23	bitri	$⊢ \exists u ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t) \leftrightarrow ⟨w, g⟩ \in (\{t\} \times t)$
25	24	anbi2i	$⊢ (t \in h \land \exists u ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t)) \leftrightarrow (t \in h \land ⟨w, g⟩ \in (\{t\} \times t))$
26		opelxp	$⊢ ⟨w, g⟩ \in (\{t\} \times t) \leftrightarrow (w \in \{t\} \land g \in t)$
27		velsn	$⊢ w \in \{t\} \leftrightarrow w = t$
28		equcom	$⊢ w = t \leftrightarrow t = w$
29	27 28	bitri	$⊢ w \in \{t\} \leftrightarrow t = w$
30	29	anbi1i	$⊢ (w \in \{t\} \land g \in t) \leftrightarrow (t = w \land g \in t)$
31	26 30	bitri	$⊢ ⟨w, g⟩ \in (\{t\} \times t) \leftrightarrow (t = w \land g \in t)$
32	31	anbi2i	$⊢ (t \in h \land ⟨w, g⟩ \in (\{t\} \times t)) \leftrightarrow (t \in h \land (t = w \land g \in t))$
33		an12	$⊢ (t \in h \land (t = w \land g \in t)) \leftrightarrow (t = w \land (t \in h \land g \in t))$
34	25 32 33	3bitri	$⊢ (t \in h \land \exists u ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t)) \leftrightarrow (t = w \land (t \in h \land g \in t))$
35	34	exbii	$⊢ \exists t (t \in h \land \exists u ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t)) \leftrightarrow \exists t (t = w \land (t \in h \land g \in t))$
36		vex	$⊢ w \in V$
37		elequ1	$⊢ t = w \to (t \in h \leftrightarrow w \in h)$
38		eleq2	$⊢ t = w \to (g \in t \leftrightarrow g \in w)$
39	37 38	anbi12d	$⊢ t = w \to ((t \in h \land g \in t) \leftrightarrow (w \in h \land g \in w))$
40	36 39	ceqsexv	$⊢ \exists t (t = w \land (t \in h \land g \in t)) \leftrightarrow (w \in h \land g \in w)$
41	35 40	bitri	$⊢ \exists t (t \in h \land \exists u ((⟨w, g⟩ \in u \land u \neq \emptyset) \land u = \{t\} \times t)) \leftrightarrow (w \in h \land g \in w)$
42	3 12 41	3bitri	$⊢ ⟨w, g⟩ \in ⋃ A \leftrightarrow (w \in h \land g \in w)$

Metamath Proof Explorer

Theorem dfac5lem2

Proof