Step |
Hyp |
Ref |
Expression |
1 |
|
toptopon2 |
|- ( x e. Top <-> x e. ( TopOn ` U. x ) ) |
2 |
|
fvex |
|- ( TopOn ` U. x ) e. _V |
3 |
|
eleq2 |
|- ( y = ( TopOn ` U. x ) -> ( x e. y <-> x e. ( TopOn ` U. x ) ) ) |
4 |
|
eleq1 |
|- ( y = ( TopOn ` U. x ) -> ( y e. ran TopOn <-> ( TopOn ` U. x ) e. ran TopOn ) ) |
5 |
3 4
|
anbi12d |
|- ( y = ( TopOn ` U. x ) -> ( ( x e. y /\ y e. ran TopOn ) <-> ( x e. ( TopOn ` U. x ) /\ ( TopOn ` U. x ) e. ran TopOn ) ) ) |
6 |
|
simpl |
|- ( ( x e. ( TopOn ` U. x ) /\ ( TopOn ` U. x ) e. ran TopOn ) -> x e. ( TopOn ` U. x ) ) |
7 |
|
fntopon |
|- TopOn Fn _V |
8 |
|
vuniex |
|- U. x e. _V |
9 |
|
fnfvelrn |
|- ( ( TopOn Fn _V /\ U. x e. _V ) -> ( TopOn ` U. x ) e. ran TopOn ) |
10 |
7 8 9
|
mp2an |
|- ( TopOn ` U. x ) e. ran TopOn |
11 |
10
|
jctr |
|- ( x e. ( TopOn ` U. x ) -> ( x e. ( TopOn ` U. x ) /\ ( TopOn ` U. x ) e. ran TopOn ) ) |
12 |
6 11
|
impbii |
|- ( ( x e. ( TopOn ` U. x ) /\ ( TopOn ` U. x ) e. ran TopOn ) <-> x e. ( TopOn ` U. x ) ) |
13 |
5 12
|
bitrdi |
|- ( y = ( TopOn ` U. x ) -> ( ( x e. y /\ y e. ran TopOn ) <-> x e. ( TopOn ` U. x ) ) ) |
14 |
2 13
|
spcev |
|- ( x e. ( TopOn ` U. x ) -> E. y ( x e. y /\ y e. ran TopOn ) ) |
15 |
1 14
|
sylbi |
|- ( x e. Top -> E. y ( x e. y /\ y e. ran TopOn ) ) |
16 |
|
funtopon |
|- Fun TopOn |
17 |
|
elrnrexdm |
|- ( Fun TopOn -> ( y e. ran TopOn -> E. z e. dom TopOn y = ( TopOn ` z ) ) ) |
18 |
16 17
|
ax-mp |
|- ( y e. ran TopOn -> E. z e. dom TopOn y = ( TopOn ` z ) ) |
19 |
|
rexex |
|- ( E. z e. dom TopOn y = ( TopOn ` z ) -> E. z y = ( TopOn ` z ) ) |
20 |
18 19
|
syl |
|- ( y e. ran TopOn -> E. z y = ( TopOn ` z ) ) |
21 |
|
19.42v |
|- ( E. z ( x e. y /\ y = ( TopOn ` z ) ) <-> ( x e. y /\ E. z y = ( TopOn ` z ) ) ) |
22 |
|
eqimss |
|- ( y = ( TopOn ` z ) -> y C_ ( TopOn ` z ) ) |
23 |
22
|
sseld |
|- ( y = ( TopOn ` z ) -> ( x e. y -> x e. ( TopOn ` z ) ) ) |
24 |
23
|
impcom |
|- ( ( x e. y /\ y = ( TopOn ` z ) ) -> x e. ( TopOn ` z ) ) |
25 |
24
|
eximi |
|- ( E. z ( x e. y /\ y = ( TopOn ` z ) ) -> E. z x e. ( TopOn ` z ) ) |
26 |
21 25
|
sylbir |
|- ( ( x e. y /\ E. z y = ( TopOn ` z ) ) -> E. z x e. ( TopOn ` z ) ) |
27 |
20 26
|
sylan2 |
|- ( ( x e. y /\ y e. ran TopOn ) -> E. z x e. ( TopOn ` z ) ) |
28 |
|
topontop |
|- ( x e. ( TopOn ` z ) -> x e. Top ) |
29 |
28
|
exlimiv |
|- ( E. z x e. ( TopOn ` z ) -> x e. Top ) |
30 |
27 29
|
syl |
|- ( ( x e. y /\ y e. ran TopOn ) -> x e. Top ) |
31 |
30
|
exlimiv |
|- ( E. y ( x e. y /\ y e. ran TopOn ) -> x e. Top ) |
32 |
15 31
|
impbii |
|- ( x e. Top <-> E. y ( x e. y /\ y e. ran TopOn ) ) |
33 |
|
eluni |
|- ( x e. U. ran TopOn <-> E. y ( x e. y /\ y e. ran TopOn ) ) |
34 |
32 33
|
bitr4i |
|- ( x e. Top <-> x e. U. ran TopOn ) |
35 |
34
|
eqriv |
|- Top = U. ran TopOn |