Theorem isfne3

Description: The predicate " B is finer than A ". (Contributed by Jeff Hankins, 11-Oct-2009) (Proof shortened by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	isfne.1	$$⊢X=\bigcup A$$
	isfne.2	$$⊢Y=\bigcup B$$
Assertion	isfne3	$$⊢B\in C\to \left(A\mathrm{Fne}B\leftrightarrow \left(X=Y\wedge \forall x\in A\exists y\left(y\subseteq B\wedge x=\bigcup y\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isfne.1	$$⊢X=\bigcup A$$
2		isfne.2	$$⊢Y=\bigcup B$$
3	1 2	isfne4	$$⊢A\mathrm{Fne}B\leftrightarrow \left(X=Y\wedge A\subseteq \mathrm{topGen}\left(B\right)\right)$$
4		dfss3	$$⊢A\subseteq \mathrm{topGen}\left(B\right)\leftrightarrow \forall x\in Ax\in \mathrm{topGen}\left(B\right)$$
5		eltg3	$$⊢B\in C\to \left(x\in \mathrm{topGen}\left(B\right)\leftrightarrow \exists y\left(y\subseteq B\wedge x=\bigcup y\right)\right)$$
6	5	ralbidv	$$⊢B\in C\to \left(\forall x\in Ax\in \mathrm{topGen}\left(B\right)\leftrightarrow \forall x\in A\exists y\left(y\subseteq B\wedge x=\bigcup y\right)\right)$$
7	4 6	bitrid	$$⊢B\in C\to \left(A\subseteq \mathrm{topGen}\left(B\right)\leftrightarrow \forall x\in A\exists y\left(y\subseteq B\wedge x=\bigcup y\right)\right)$$
8	7	anbi2d	$$⊢B\in C\to \left(\left(X=Y\wedge A\subseteq \mathrm{topGen}\left(B\right)\right)\leftrightarrow \left(X=Y\wedge \forall x\in A\exists y\left(y\subseteq B\wedge x=\bigcup y\right)\right)\right)$$
9	3 8	bitrid	$$⊢B\in C\to \left(A\mathrm{Fne}B\leftrightarrow \left(X=Y\wedge \forall x\in A\exists y\left(y\subseteq B\wedge x=\bigcup y\right)\right)\right)$$