Description: Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | cntop1 | |- ( F e. ( J Cn K ) -> J e. Top ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |- U. J = U. J |
|
2 | eqid | |- U. K = U. K |
|
3 | 1 2 | iscn2 | |- ( F e. ( J Cn K ) <-> ( ( J e. Top /\ K e. Top ) /\ ( F : U. J --> U. K /\ A. x e. K ( `' F " x ) e. J ) ) ) |
4 | 3 | simplbi | |- ( F e. ( J Cn K ) -> ( J e. Top /\ K e. Top ) ) |
5 | 4 | simpld | |- ( F e. ( J Cn K ) -> J e. Top ) |