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 = U. A
	isfne.2	|- Y = U. B
Assertion	isfne3	|- ( B e. C -> ( A Fne B <-> ( X = Y /\ A. x e. A E. y ( y C_ B /\ x = U. y ) ) ) )

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		dfss3	|- ( A C_ ( topGen ` B ) <-> A. x e. A x e. ( topGen ` B ) )
5		eltg3	|- ( B e. C -> ( x e. ( topGen ` B ) <-> E. y ( y C_ B /\ x = U. y ) ) )
6	5	ralbidv	|- ( B e. C -> ( A. x e. A x e. ( topGen ` B ) <-> A. x e. A E. y ( y C_ B /\ x = U. y ) ) )
7	4 6	syl5bb	|- ( B e. C -> ( A C_ ( topGen ` B ) <-> A. x e. A E. y ( y C_ B /\ x = U. y ) ) )
8	7	anbi2d	|- ( B e. C -> ( ( X = Y /\ A C_ ( topGen ` B ) ) <-> ( X = Y /\ A. x e. A E. y ( y C_ B /\ x = U. y ) ) ) )
9	3 8	syl5bb	|- ( B e. C -> ( A Fne B <-> ( X = Y /\ A. x e. A E. y ( y C_ B /\ x = U. y ) ) ) )