Theorem isfne4b

Description: A condition for a topology to be finer than another. (Contributed by Jeff Hankins, 28-Sep-2009) (Revised by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	isfne.1	|- X = U. A
	isfne.2	|- Y = U. B
Assertion	isfne4b	|- ( B e. V -> ( A Fne B <-> ( X = Y /\ ( topGen ` A ) C_ ( topGen ` B ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isfne.1	|- X = U. A
2		isfne.2	|- Y = U. B
3	1 2	isfne4	|- ( A Fne B <-> ( X = Y /\ A C_ ( topGen ` B ) ) )
4		simpr	|- ( ( B e. V /\ X = Y ) -> X = Y )
5	4 1 2	3eqtr3g	|- ( ( B e. V /\ X = Y ) -> U. A = U. B )
6		uniexg	|- ( B e. V -> U. B e. _V )
7	6	adantr	|- ( ( B e. V /\ X = Y ) -> U. B e. _V )
8	5 7	eqeltrd	|- ( ( B e. V /\ X = Y ) -> U. A e. _V )
9		uniexb	|- ( A e. _V <-> U. A e. _V )
10	8 9	sylibr	|- ( ( B e. V /\ X = Y ) -> A e. _V )
11		simpl	|- ( ( B e. V /\ X = Y ) -> B e. V )
12		tgss3	|- ( ( A e. _V /\ B e. V ) -> ( ( topGen ` A ) C_ ( topGen ` B ) <-> A C_ ( topGen ` B ) ) )
13	10 11 12	syl2anc	|- ( ( B e. V /\ X = Y ) -> ( ( topGen ` A ) C_ ( topGen ` B ) <-> A C_ ( topGen ` B ) ) )
14	13	pm5.32da	|- ( B e. V -> ( ( X = Y /\ ( topGen ` A ) C_ ( topGen ` B ) ) <-> ( X = Y /\ A C_ ( topGen ` B ) ) ) )
15	3 14	bitr4id	|- ( B e. V -> ( A Fne B <-> ( X = Y /\ ( topGen ` A ) C_ ( topGen ` B ) ) ) )