Metamath Proof Explorer

Theorem isfne4

Description: The predicate " B is finer than A " in terms of the topology generation function. (Contributed by Mario Carneiro, 11-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 isfne.1 
 |-  X = U. A
2 isfne.2 
 |-  Y = U. B
3 fnerel 
 |-  Rel Fne
4 3 brrelex2i 
 |-  ( A Fne B -> B e. _V )
5 simpl 
 |-  ( ( X = Y /\ A C_ ( topGen ` B ) ) -> X = Y )
6 5 1 2 3eqtr3g 
 |-  ( ( X = Y /\ A C_ ( topGen ` B ) ) -> U. A = U. B )
7 fvex 
 |-  ( topGen ` B ) e. _V
8 7 ssex 
 |-  ( A C_ ( topGen ` B ) -> A e. _V )
9 8 adantl 
 |-  ( ( X = Y /\ A C_ ( topGen ` B ) ) -> A e. _V )
10 9 uniexd 
 |-  ( ( X = Y /\ A C_ ( topGen ` B ) ) -> U. A e. _V )
11 6 10 eqeltrrd 
 |-  ( ( X = Y /\ A C_ ( topGen ` B ) ) -> U. B e. _V )
12 uniexb 
 |-  ( B e. _V <-> U. B e. _V )
13 11 12 sylibr 
 |-  ( ( X = Y /\ A C_ ( topGen ` B ) ) -> B e. _V )
14 1 2 isfne 
 |-  ( B e. _V -> ( A Fne B <-> ( X = Y /\ A. x e. A x C_ U. ( B i^i ~P x ) ) ) )
15 dfss3 
 |-  ( A C_ ( topGen ` B ) <-> A. x e. A x e. ( topGen ` B ) )
16 eltg 
 |-  ( B e. _V -> ( x e. ( topGen ` B ) <-> x C_ U. ( B i^i ~P x ) ) )
17 16 ralbidv 
 |-  ( B e. _V -> ( A. x e. A x e. ( topGen ` B ) <-> A. x e. A x C_ U. ( B i^i ~P x ) ) )
18 15 17 syl5bb 
 |-  ( B e. _V -> ( A C_ ( topGen ` B ) <-> A. x e. A x C_ U. ( B i^i ~P x ) ) )
19 18 anbi2d 
 |-  ( B e. _V -> ( ( X = Y /\ A C_ ( topGen ` B ) ) <-> ( X = Y /\ A. x e. A x C_ U. ( B i^i ~P x ) ) ) )
20 14 19 bitr4d 
 |-  ( B e. _V -> ( A Fne B <-> ( X = Y /\ A C_ ( topGen ` B ) ) ) )
21 4 13 20 pm5.21nii 
 |-  ( A Fne B <-> ( X = Y /\ A C_ ( topGen ` B ) ) )