Metamath Proof Explorer

Theorem isfne2

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

Ref Expression
Hypotheses isfne.1 
|- X = U. A
isfne.2 
|- Y = U. B
Assertion isfne2 
|- ( B e. C -> ( A Fne B <-> ( X = Y /\ A. x e. A A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) ) )

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