Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( B e. TopBases /\ B ~<_ _om ) -> B e. TopBases ) |
2 |
|
simpr |
|- ( ( B e. TopBases /\ B ~<_ _om ) -> B ~<_ _om ) |
3 |
|
eqidd |
|- ( ( B e. TopBases /\ B ~<_ _om ) -> ( topGen ` B ) = ( topGen ` B ) ) |
4 |
|
breq1 |
|- ( x = B -> ( x ~<_ _om <-> B ~<_ _om ) ) |
5 |
|
fveqeq2 |
|- ( x = B -> ( ( topGen ` x ) = ( topGen ` B ) <-> ( topGen ` B ) = ( topGen ` B ) ) ) |
6 |
4 5
|
anbi12d |
|- ( x = B -> ( ( x ~<_ _om /\ ( topGen ` x ) = ( topGen ` B ) ) <-> ( B ~<_ _om /\ ( topGen ` B ) = ( topGen ` B ) ) ) ) |
7 |
6
|
rspcev |
|- ( ( B e. TopBases /\ ( B ~<_ _om /\ ( topGen ` B ) = ( topGen ` B ) ) ) -> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = ( topGen ` B ) ) ) |
8 |
1 2 3 7
|
syl12anc |
|- ( ( B e. TopBases /\ B ~<_ _om ) -> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = ( topGen ` B ) ) ) |
9 |
|
is2ndc |
|- ( ( topGen ` B ) e. 2ndc <-> E. x e. TopBases ( x ~<_ _om /\ ( topGen ` x ) = ( topGen ` B ) ) ) |
10 |
8 9
|
sylibr |
|- ( ( B e. TopBases /\ B ~<_ _om ) -> ( topGen ` B ) e. 2ndc ) |