Metamath Proof Explorer

Theorem fneuni

Description: If B is finer than A , every element of A is a union of elements of B . (Contributed by Jeff Hankins, 11-Oct-2009)

Ref Expression
Assertion fneuni 
|- ( ( A Fne B /\ S e. A ) -> E. x ( x C_ B /\ S = U. x ) )

Proof

Step Hyp Ref Expression
1 fnetg 
 |-  ( A Fne B -> A C_ ( topGen ` B ) )
2 1 sselda 
 |-  ( ( A Fne B /\ S e. A ) -> S e. ( topGen ` B ) )
3 elfvdm 
 |-  ( S e. ( topGen ` B ) -> B e. dom topGen )
4 eltg3 
 |-  ( B e. dom topGen -> ( S e. ( topGen ` B ) <-> E. x ( x C_ B /\ S = U. x ) ) )
5 3 4 syl 
 |-  ( S e. ( topGen ` B ) -> ( S e. ( topGen ` B ) <-> E. x ( x C_ B /\ S = U. x ) ) )
6 5 ibi 
 |-  ( S e. ( topGen ` B ) -> E. x ( x C_ B /\ S = U. x ) )
7 2 6 syl 
 |-  ( ( A Fne B /\ S e. A ) -> E. x ( x C_ B /\ S = U. x ) )