Step |
Hyp |
Ref |
Expression |
1 |
|
cnmptk1.j |
|- ( ph -> J e. ( TopOn ` X ) ) |
2 |
|
cnmptk1.k |
|- ( ph -> K e. ( TopOn ` Y ) ) |
3 |
|
cnmptk1.l |
|- ( ph -> L e. ( TopOn ` Z ) ) |
4 |
|
cnmptk1.a |
|- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) ) |
5 |
|
cnmptk1.b |
|- ( ph -> ( z e. Z |-> B ) e. ( L Cn M ) ) |
6 |
|
cnmptk1.c |
|- ( z = A -> B = C ) |
7 |
2
|
adantr |
|- ( ( ph /\ x e. X ) -> K e. ( TopOn ` Y ) ) |
8 |
3
|
adantr |
|- ( ( ph /\ x e. X ) -> L e. ( TopOn ` Z ) ) |
9 |
|
topontop |
|- ( K e. ( TopOn ` Y ) -> K e. Top ) |
10 |
2 9
|
syl |
|- ( ph -> K e. Top ) |
11 |
|
topontop |
|- ( L e. ( TopOn ` Z ) -> L e. Top ) |
12 |
3 11
|
syl |
|- ( ph -> L e. Top ) |
13 |
|
eqid |
|- ( L ^ko K ) = ( L ^ko K ) |
14 |
13
|
xkotopon |
|- ( ( K e. Top /\ L e. Top ) -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) ) |
15 |
10 12 14
|
syl2anc |
|- ( ph -> ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) ) |
16 |
|
cnf2 |
|- ( ( J e. ( TopOn ` X ) /\ ( L ^ko K ) e. ( TopOn ` ( K Cn L ) ) /\ ( x e. X |-> ( y e. Y |-> A ) ) e. ( J Cn ( L ^ko K ) ) ) -> ( x e. X |-> ( y e. Y |-> A ) ) : X --> ( K Cn L ) ) |
17 |
1 15 4 16
|
syl3anc |
|- ( ph -> ( x e. X |-> ( y e. Y |-> A ) ) : X --> ( K Cn L ) ) |
18 |
17
|
fvmptelrn |
|- ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) e. ( K Cn L ) ) |
19 |
|
cnf2 |
|- ( ( K e. ( TopOn ` Y ) /\ L e. ( TopOn ` Z ) /\ ( y e. Y |-> A ) e. ( K Cn L ) ) -> ( y e. Y |-> A ) : Y --> Z ) |
20 |
7 8 18 19
|
syl3anc |
|- ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) : Y --> Z ) |
21 |
|
eqid |
|- ( y e. Y |-> A ) = ( y e. Y |-> A ) |
22 |
21
|
fmpt |
|- ( A. y e. Y A e. Z <-> ( y e. Y |-> A ) : Y --> Z ) |
23 |
20 22
|
sylibr |
|- ( ( ph /\ x e. X ) -> A. y e. Y A e. Z ) |
24 |
|
eqidd |
|- ( ( ph /\ x e. X ) -> ( y e. Y |-> A ) = ( y e. Y |-> A ) ) |
25 |
|
eqidd |
|- ( ( ph /\ x e. X ) -> ( z e. Z |-> B ) = ( z e. Z |-> B ) ) |
26 |
23 24 25 6
|
fmptcof |
|- ( ( ph /\ x e. X ) -> ( ( z e. Z |-> B ) o. ( y e. Y |-> A ) ) = ( y e. Y |-> C ) ) |
27 |
26
|
mpteq2dva |
|- ( ph -> ( x e. X |-> ( ( z e. Z |-> B ) o. ( y e. Y |-> A ) ) ) = ( x e. X |-> ( y e. Y |-> C ) ) ) |
28 |
10 5
|
xkoco2cn |
|- ( ph -> ( w e. ( K Cn L ) |-> ( ( z e. Z |-> B ) o. w ) ) e. ( ( L ^ko K ) Cn ( M ^ko K ) ) ) |
29 |
|
coeq2 |
|- ( w = ( y e. Y |-> A ) -> ( ( z e. Z |-> B ) o. w ) = ( ( z e. Z |-> B ) o. ( y e. Y |-> A ) ) ) |
30 |
1 4 15 28 29
|
cnmpt11 |
|- ( ph -> ( x e. X |-> ( ( z e. Z |-> B ) o. ( y e. Y |-> A ) ) ) e. ( J Cn ( M ^ko K ) ) ) |
31 |
27 30
|
eqeltrrd |
|- ( ph -> ( x e. X |-> ( y e. Y |-> C ) ) e. ( J Cn ( M ^ko K ) ) ) |