Step |
Hyp |
Ref |
Expression |
1 |
|
dfiun3g |
|- ( A. x e. A C e. B -> U_ x e. A C = U. ran ( x e. A |-> C ) ) |
2 |
1
|
adantl |
|- ( ( B e. V /\ A. x e. A C e. B ) -> U_ x e. A C = U. ran ( x e. A |-> C ) ) |
3 |
|
eqid |
|- ( x e. A |-> C ) = ( x e. A |-> C ) |
4 |
3
|
rnmptss |
|- ( A. x e. A C e. B -> ran ( x e. A |-> C ) C_ B ) |
5 |
|
eltg3i |
|- ( ( B e. V /\ ran ( x e. A |-> C ) C_ B ) -> U. ran ( x e. A |-> C ) e. ( topGen ` B ) ) |
6 |
4 5
|
sylan2 |
|- ( ( B e. V /\ A. x e. A C e. B ) -> U. ran ( x e. A |-> C ) e. ( topGen ` B ) ) |
7 |
2 6
|
eqeltrd |
|- ( ( B e. V /\ A. x e. A C e. B ) -> U_ x e. A C e. ( topGen ` B ) ) |