Theorem fnejoin1

Description: Join of equivalence classes under the fineness relation-part one. (Contributed by Jeff Hankins, 8-Oct-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

	Ref	Expression
Assertion	fnejoin1	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to A\mathrm{Fne}if\left(S=\varnothing ,\left\{X\right\},\bigcup S\right)$$

Proof

Step	Hyp	Ref	Expression
1		elssuni	$$⊢A\in S\to A\subseteq \bigcup S$$
2	1	3ad2ant3	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to A\subseteq \bigcup S$$
3	2	unissd	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to \bigcup A\subseteq \bigcup \bigcup S$$
4		eqimss2	$$⊢X=\bigcup y\to \bigcup y\subseteq X$$
5		sspwuni	$$⊢y\subseteq 𝒫X\leftrightarrow \bigcup y\subseteq X$$
6	4 5	sylibr	$$⊢X=\bigcup y\to y\subseteq 𝒫X$$
7	6	ralimi	$$⊢\forall y\in SX=\bigcup y\to \forall y\in Sy\subseteq 𝒫X$$
8	7	3ad2ant2	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to \forall y\in Sy\subseteq 𝒫X$$
9		unissb	$$⊢\bigcup S\subseteq 𝒫X\leftrightarrow \forall y\in Sy\subseteq 𝒫X$$
10	8 9	sylibr	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to \bigcup S\subseteq 𝒫X$$
11		sspwuni	$$⊢\bigcup S\subseteq 𝒫X\leftrightarrow \bigcup \bigcup S\subseteq X$$
12	10 11	sylib	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to \bigcup \bigcup S\subseteq X$$
13		unieq	$$⊢y=A\to \bigcup y=\bigcup A$$
14	13	eqeq2d	$$⊢y=A\to \left(X=\bigcup y\leftrightarrow X=\bigcup A\right)$$
15	14	rspccva	$$⊢\left(\forall y\in SX=\bigcup y\wedge A\in S\right)\to X=\bigcup A$$
16	15	3adant1	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to X=\bigcup A$$
17	12 16	sseqtrd	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to \bigcup \bigcup S\subseteq \bigcup A$$
18	3 17	eqssd	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to \bigcup A=\bigcup \bigcup S$$
19		pwexg	$$⊢X\in V\to 𝒫X\in \mathrm{V}$$
20	19	3ad2ant1	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to 𝒫X\in \mathrm{V}$$
21	20 10	ssexd	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to \bigcup S\in \mathrm{V}$$
22		bastg	$$⊢\bigcup S\in \mathrm{V}\to \bigcup S\subseteq \mathrm{topGen}\left(\bigcup S\right)$$
23	21 22	syl	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to \bigcup S\subseteq \mathrm{topGen}\left(\bigcup S\right)$$
24	2 23	sstrd	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to A\subseteq \mathrm{topGen}\left(\bigcup S\right)$$
25		eqid	$$⊢\bigcup A=\bigcup A$$
26		eqid	$$⊢\bigcup \bigcup S=\bigcup \bigcup S$$
27	25 26	isfne4	$$⊢A\mathrm{Fne}\bigcup S\leftrightarrow \left(\bigcup A=\bigcup \bigcup S\wedge A\subseteq \mathrm{topGen}\left(\bigcup S\right)\right)$$
28	18 24 27	sylanbrc	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to A\mathrm{Fne}\bigcup S$$
29		ne0i	$$⊢A\in S\to S\ne \varnothing$$
30	29	3ad2ant3	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to S\ne \varnothing$$
31		ifnefalse	$$⊢S\ne \varnothing \to if\left(S=\varnothing ,\left\{X\right\},\bigcup S\right)=\bigcup S$$
32	30 31	syl	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to if\left(S=\varnothing ,\left\{X\right\},\bigcup S\right)=\bigcup S$$
33	28 32	breqtrrd	$$⊢\left(X\in V\wedge \forall y\in SX=\bigcup y\wedge A\in S\right)\to A\mathrm{Fne}if\left(S=\varnothing ,\left\{X\right\},\bigcup S\right)$$