This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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