Theorem dfac5lem3

Description: Lemma for dfac5 . (Contributed by NM, 12-Apr-2004)

	Ref	Expression
Hypothesis	dfac5lem.1	$$⊢A=\left\{u|\left(u\ne \varnothing \wedge \exists t\in hu=\left\{t\right\}\times t\right)\right\}$$
Assertion	dfac5lem3	$$⊢\left\{w\right\}\times w\in A\leftrightarrow \left(w\ne \varnothing \wedge w\in h\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfac5lem.1	$$⊢A=\left\{u|\left(u\ne \varnothing \wedge \exists t\in hu=\left\{t\right\}\times t\right)\right\}$$
2		snex	$$⊢\left\{w\right\}\in \mathrm{V}$$
3		vex	$$⊢w\in \mathrm{V}$$
4	2 3	xpex	$$⊢\left\{w\right\}\times w\in \mathrm{V}$$
5		neeq1	$$⊢u=\left\{w\right\}\times w\to \left(u\ne \varnothing \leftrightarrow \left\{w\right\}\times w\ne \varnothing \right)$$
6		eqeq1	$$⊢u=\left\{w\right\}\times w\to \left(u=\left\{t\right\}\times t\leftrightarrow \left\{w\right\}\times w=\left\{t\right\}\times t\right)$$
7	6	rexbidv	$$⊢u=\left\{w\right\}\times w\to \left(\exists t\in hu=\left\{t\right\}\times t\leftrightarrow \exists t\in h\left\{w\right\}\times w=\left\{t\right\}\times t\right)$$
8	5 7	anbi12d	$$⊢u=\left\{w\right\}\times w\to \left(\left(u\ne \varnothing \wedge \exists t\in hu=\left\{t\right\}\times t\right)\leftrightarrow \left(\left\{w\right\}\times w\ne \varnothing \wedge \exists t\in h\left\{w\right\}\times w=\left\{t\right\}\times t\right)\right)$$
9	4 8	elab	$$⊢\left\{w\right\}\times w\in \left\{u|\left(u\ne \varnothing \wedge \exists t\in hu=\left\{t\right\}\times t\right)\right\}\leftrightarrow \left(\left\{w\right\}\times w\ne \varnothing \wedge \exists t\in h\left\{w\right\}\times w=\left\{t\right\}\times t\right)$$
10	1	eleq2i	$$⊢\left\{w\right\}\times w\in A\leftrightarrow \left\{w\right\}\times w\in \left\{u|\left(u\ne \varnothing \wedge \exists t\in hu=\left\{t\right\}\times t\right)\right\}$$
11		xpeq2	$$⊢w=\varnothing \to \left\{w\right\}\times w=\left\{w\right\}\times \varnothing$$
12		xp0	$$⊢\left\{w\right\}\times \varnothing =\varnothing$$
13	11 12	eqtrdi	$$⊢w=\varnothing \to \left\{w\right\}\times w=\varnothing$$
14		rneq	$$⊢\left\{w\right\}\times w=\varnothing \to \mathrm{ran}\left(\left\{w\right\}\times w\right)=\mathrm{ran}\varnothing$$
15	3	snnz	$$⊢\left\{w\right\}\ne \varnothing$$
16		rnxp	$$⊢\left\{w\right\}\ne \varnothing \to \mathrm{ran}\left(\left\{w\right\}\times w\right)=w$$
17	15 16	ax-mp	$$⊢\mathrm{ran}\left(\left\{w\right\}\times w\right)=w$$
18		rn0	$$⊢\mathrm{ran}\varnothing =\varnothing$$
19	14 17 18	3eqtr3g	$$⊢\left\{w\right\}\times w=\varnothing \to w=\varnothing$$
20	13 19	impbii	$$⊢w=\varnothing \leftrightarrow \left\{w\right\}\times w=\varnothing$$
21	20	necon3bii	$$⊢w\ne \varnothing \leftrightarrow \left\{w\right\}\times w\ne \varnothing$$
22		df-rex	$$⊢\exists t\in h\left\{w\right\}\times w=\left\{t\right\}\times t\leftrightarrow \exists t\left(t\in h\wedge \left\{w\right\}\times w=\left\{t\right\}\times t\right)$$
23		rneq	$$⊢\left\{w\right\}\times w=\left\{t\right\}\times t\to \mathrm{ran}\left(\left\{w\right\}\times w\right)=\mathrm{ran}\left(\left\{t\right\}\times t\right)$$
24		vex	$$⊢t\in \mathrm{V}$$
25	24	snnz	$$⊢\left\{t\right\}\ne \varnothing$$
26		rnxp	$$⊢\left\{t\right\}\ne \varnothing \to \mathrm{ran}\left(\left\{t\right\}\times t\right)=t$$
27	25 26	ax-mp	$$⊢\mathrm{ran}\left(\left\{t\right\}\times t\right)=t$$
28	23 17 27	3eqtr3g	$$⊢\left\{w\right\}\times w=\left\{t\right\}\times t\to w=t$$
29		sneq	$$⊢w=t\to \left\{w\right\}=\left\{t\right\}$$
30	29	xpeq1d	$$⊢w=t\to \left\{w\right\}\times w=\left\{t\right\}\times w$$
31		xpeq2	$$⊢w=t\to \left\{t\right\}\times w=\left\{t\right\}\times t$$
32	30 31	eqtrd	$$⊢w=t\to \left\{w\right\}\times w=\left\{t\right\}\times t$$
33	28 32	impbii	$$⊢\left\{w\right\}\times w=\left\{t\right\}\times t\leftrightarrow w=t$$
34		equcom	$$⊢w=t\leftrightarrow t=w$$
35	33 34	bitri	$$⊢\left\{w\right\}\times w=\left\{t\right\}\times t\leftrightarrow t=w$$
36	35	anbi1ci	$$⊢\left(t\in h\wedge \left\{w\right\}\times w=\left\{t\right\}\times t\right)\leftrightarrow \left(t=w\wedge t\in h\right)$$
37	36	exbii	$$⊢\exists t\left(t\in h\wedge \left\{w\right\}\times w=\left\{t\right\}\times t\right)\leftrightarrow \exists t\left(t=w\wedge t\in h\right)$$
38		elequ1	$$⊢t=w\to \left(t\in h\leftrightarrow w\in h\right)$$
39	38	equsexvw	$$⊢\exists t\left(t=w\wedge t\in h\right)\leftrightarrow w\in h$$
40	22 37 39	3bitrri	$$⊢w\in h\leftrightarrow \exists t\in h\left\{w\right\}\times w=\left\{t\right\}\times t$$
41	21 40	anbi12i	$$⊢\left(w\ne \varnothing \wedge w\in h\right)\leftrightarrow \left(\left\{w\right\}\times w\ne \varnothing \wedge \exists t\in h\left\{w\right\}\times w=\left\{t\right\}\times t\right)$$
42	9 10 41	3bitr4i	$$⊢\left\{w\right\}\times w\in A\leftrightarrow \left(w\ne \varnothing \wedge w\in h\right)$$