Metamath Proof Explorer

Theorem fnetg

Description: A finer cover generates a topology finer than the original set. (Contributed by Mario Carneiro, 11-Sep-2015)

Ref Expression
Assertion fnetg 
|- ( A Fne B -> A C_ ( topGen ` B ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. A = U. A
2 eqid 
 |-  U. B = U. B
3 1 2 isfne4 
 |-  ( A Fne B <-> ( U. A = U. B /\ A C_ ( topGen ` B ) ) )
4 3 simprbi 
 |-  ( A Fne B -> A C_ ( topGen ` B ) )