Step |
Hyp |
Ref |
Expression |
1 |
|
cnss1.1 |
|- X = U. J |
2 |
|
eqid |
|- U. L = U. L |
3 |
1 2
|
cnf |
|- ( f e. ( J Cn L ) -> f : X --> U. L ) |
4 |
3
|
adantl |
|- ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) -> f : X --> U. L ) |
5 |
|
simpllr |
|- ( ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) /\ x e. L ) -> J C_ K ) |
6 |
|
cnima |
|- ( ( f e. ( J Cn L ) /\ x e. L ) -> ( `' f " x ) e. J ) |
7 |
6
|
adantll |
|- ( ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) /\ x e. L ) -> ( `' f " x ) e. J ) |
8 |
5 7
|
sseldd |
|- ( ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) /\ x e. L ) -> ( `' f " x ) e. K ) |
9 |
8
|
ralrimiva |
|- ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) -> A. x e. L ( `' f " x ) e. K ) |
10 |
|
simpll |
|- ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) -> K e. ( TopOn ` X ) ) |
11 |
|
cntop2 |
|- ( f e. ( J Cn L ) -> L e. Top ) |
12 |
11
|
adantl |
|- ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) -> L e. Top ) |
13 |
|
toptopon2 |
|- ( L e. Top <-> L e. ( TopOn ` U. L ) ) |
14 |
12 13
|
sylib |
|- ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) -> L e. ( TopOn ` U. L ) ) |
15 |
|
iscn |
|- ( ( K e. ( TopOn ` X ) /\ L e. ( TopOn ` U. L ) ) -> ( f e. ( K Cn L ) <-> ( f : X --> U. L /\ A. x e. L ( `' f " x ) e. K ) ) ) |
16 |
10 14 15
|
syl2anc |
|- ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) -> ( f e. ( K Cn L ) <-> ( f : X --> U. L /\ A. x e. L ( `' f " x ) e. K ) ) ) |
17 |
4 9 16
|
mpbir2and |
|- ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) -> f e. ( K Cn L ) ) |
18 |
17
|
ex |
|- ( ( K e. ( TopOn ` X ) /\ J C_ K ) -> ( f e. ( J Cn L ) -> f e. ( K Cn L ) ) ) |
19 |
18
|
ssrdv |
|- ( ( K e. ( TopOn ` X ) /\ J C_ K ) -> ( J Cn L ) C_ ( K Cn L ) ) |