Step |
Hyp |
Ref |
Expression |
1 |
|
bastg |
|- ( B e. V -> B C_ ( topGen ` B ) ) |
2 |
1
|
adantr |
|- ( ( B e. V /\ C e. W ) -> B C_ ( topGen ` B ) ) |
3 |
|
sstr2 |
|- ( B C_ ( topGen ` B ) -> ( ( topGen ` B ) C_ ( topGen ` C ) -> B C_ ( topGen ` C ) ) ) |
4 |
2 3
|
syl |
|- ( ( B e. V /\ C e. W ) -> ( ( topGen ` B ) C_ ( topGen ` C ) -> B C_ ( topGen ` C ) ) ) |
5 |
|
fvex |
|- ( topGen ` C ) e. _V |
6 |
|
tgss |
|- ( ( ( topGen ` C ) e. _V /\ B C_ ( topGen ` C ) ) -> ( topGen ` B ) C_ ( topGen ` ( topGen ` C ) ) ) |
7 |
5 6
|
mpan |
|- ( B C_ ( topGen ` C ) -> ( topGen ` B ) C_ ( topGen ` ( topGen ` C ) ) ) |
8 |
|
tgidm |
|- ( C e. W -> ( topGen ` ( topGen ` C ) ) = ( topGen ` C ) ) |
9 |
8
|
adantl |
|- ( ( B e. V /\ C e. W ) -> ( topGen ` ( topGen ` C ) ) = ( topGen ` C ) ) |
10 |
9
|
sseq2d |
|- ( ( B e. V /\ C e. W ) -> ( ( topGen ` B ) C_ ( topGen ` ( topGen ` C ) ) <-> ( topGen ` B ) C_ ( topGen ` C ) ) ) |
11 |
7 10
|
syl5ib |
|- ( ( B e. V /\ C e. W ) -> ( B C_ ( topGen ` C ) -> ( topGen ` B ) C_ ( topGen ` C ) ) ) |
12 |
4 11
|
impbid |
|- ( ( B e. V /\ C e. W ) -> ( ( topGen ` B ) C_ ( topGen ` C ) <-> B C_ ( topGen ` C ) ) ) |