Step |
Hyp |
Ref |
Expression |
1 |
|
cnmptid.j |
|- ( ph -> J e. ( TopOn ` X ) ) |
2 |
|
cnmpt11.a |
|- ( ph -> ( x e. X |-> A ) e. ( J Cn K ) ) |
3 |
|
cnmpt11.k |
|- ( ph -> K e. ( TopOn ` Y ) ) |
4 |
|
cnmpt11.b |
|- ( ph -> ( y e. Y |-> B ) e. ( K Cn L ) ) |
5 |
|
cnmpt11.c |
|- ( y = A -> B = C ) |
6 |
|
simpr |
|- ( ( ph /\ x e. X ) -> x e. X ) |
7 |
|
cnf2 |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ ( x e. X |-> A ) e. ( J Cn K ) ) -> ( x e. X |-> A ) : X --> Y ) |
8 |
1 3 2 7
|
syl3anc |
|- ( ph -> ( x e. X |-> A ) : X --> Y ) |
9 |
8
|
fvmptelrn |
|- ( ( ph /\ x e. X ) -> A e. Y ) |
10 |
|
eqid |
|- ( x e. X |-> A ) = ( x e. X |-> A ) |
11 |
10
|
fvmpt2 |
|- ( ( x e. X /\ A e. Y ) -> ( ( x e. X |-> A ) ` x ) = A ) |
12 |
6 9 11
|
syl2anc |
|- ( ( ph /\ x e. X ) -> ( ( x e. X |-> A ) ` x ) = A ) |
13 |
12
|
fveq2d |
|- ( ( ph /\ x e. X ) -> ( ( y e. Y |-> B ) ` ( ( x e. X |-> A ) ` x ) ) = ( ( y e. Y |-> B ) ` A ) ) |
14 |
|
eqid |
|- ( y e. Y |-> B ) = ( y e. Y |-> B ) |
15 |
5
|
eleq1d |
|- ( y = A -> ( B e. U. L <-> C e. U. L ) ) |
16 |
|
cntop2 |
|- ( ( y e. Y |-> B ) e. ( K Cn L ) -> L e. Top ) |
17 |
4 16
|
syl |
|- ( ph -> L e. Top ) |
18 |
|
toptopon2 |
|- ( L e. Top <-> L e. ( TopOn ` U. L ) ) |
19 |
17 18
|
sylib |
|- ( ph -> L e. ( TopOn ` U. L ) ) |
20 |
|
cnf2 |
|- ( ( K e. ( TopOn ` Y ) /\ L e. ( TopOn ` U. L ) /\ ( y e. Y |-> B ) e. ( K Cn L ) ) -> ( y e. Y |-> B ) : Y --> U. L ) |
21 |
3 19 4 20
|
syl3anc |
|- ( ph -> ( y e. Y |-> B ) : Y --> U. L ) |
22 |
14
|
fmpt |
|- ( A. y e. Y B e. U. L <-> ( y e. Y |-> B ) : Y --> U. L ) |
23 |
21 22
|
sylibr |
|- ( ph -> A. y e. Y B e. U. L ) |
24 |
23
|
adantr |
|- ( ( ph /\ x e. X ) -> A. y e. Y B e. U. L ) |
25 |
15 24 9
|
rspcdva |
|- ( ( ph /\ x e. X ) -> C e. U. L ) |
26 |
14 5 9 25
|
fvmptd3 |
|- ( ( ph /\ x e. X ) -> ( ( y e. Y |-> B ) ` A ) = C ) |
27 |
13 26
|
eqtrd |
|- ( ( ph /\ x e. X ) -> ( ( y e. Y |-> B ) ` ( ( x e. X |-> A ) ` x ) ) = C ) |
28 |
|
fvco3 |
|- ( ( ( x e. X |-> A ) : X --> Y /\ x e. X ) -> ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( y e. Y |-> B ) ` ( ( x e. X |-> A ) ` x ) ) ) |
29 |
8 28
|
sylan |
|- ( ( ph /\ x e. X ) -> ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( y e. Y |-> B ) ` ( ( x e. X |-> A ) ` x ) ) ) |
30 |
|
eqid |
|- ( x e. X |-> C ) = ( x e. X |-> C ) |
31 |
30
|
fvmpt2 |
|- ( ( x e. X /\ C e. U. L ) -> ( ( x e. X |-> C ) ` x ) = C ) |
32 |
6 25 31
|
syl2anc |
|- ( ( ph /\ x e. X ) -> ( ( x e. X |-> C ) ` x ) = C ) |
33 |
27 29 32
|
3eqtr4d |
|- ( ( ph /\ x e. X ) -> ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( x e. X |-> C ) ` x ) ) |
34 |
33
|
ralrimiva |
|- ( ph -> A. x e. X ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( x e. X |-> C ) ` x ) ) |
35 |
|
nfv |
|- F/ z ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( x e. X |-> C ) ` x ) |
36 |
|
nfcv |
|- F/_ x ( y e. Y |-> B ) |
37 |
|
nfmpt1 |
|- F/_ x ( x e. X |-> A ) |
38 |
36 37
|
nfco |
|- F/_ x ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) |
39 |
|
nfcv |
|- F/_ x z |
40 |
38 39
|
nffv |
|- F/_ x ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z ) |
41 |
|
nfmpt1 |
|- F/_ x ( x e. X |-> C ) |
42 |
41 39
|
nffv |
|- F/_ x ( ( x e. X |-> C ) ` z ) |
43 |
40 42
|
nfeq |
|- F/ x ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z ) = ( ( x e. X |-> C ) ` z ) |
44 |
|
fveq2 |
|- ( x = z -> ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z ) ) |
45 |
|
fveq2 |
|- ( x = z -> ( ( x e. X |-> C ) ` x ) = ( ( x e. X |-> C ) ` z ) ) |
46 |
44 45
|
eqeq12d |
|- ( x = z -> ( ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( x e. X |-> C ) ` x ) <-> ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z ) = ( ( x e. X |-> C ) ` z ) ) ) |
47 |
35 43 46
|
cbvralw |
|- ( A. x e. X ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` x ) = ( ( x e. X |-> C ) ` x ) <-> A. z e. X ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z ) = ( ( x e. X |-> C ) ` z ) ) |
48 |
34 47
|
sylib |
|- ( ph -> A. z e. X ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z ) = ( ( x e. X |-> C ) ` z ) ) |
49 |
|
fco |
|- ( ( ( y e. Y |-> B ) : Y --> U. L /\ ( x e. X |-> A ) : X --> Y ) -> ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) : X --> U. L ) |
50 |
21 8 49
|
syl2anc |
|- ( ph -> ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) : X --> U. L ) |
51 |
50
|
ffnd |
|- ( ph -> ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) Fn X ) |
52 |
25
|
fmpttd |
|- ( ph -> ( x e. X |-> C ) : X --> U. L ) |
53 |
52
|
ffnd |
|- ( ph -> ( x e. X |-> C ) Fn X ) |
54 |
|
eqfnfv |
|- ( ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) Fn X /\ ( x e. X |-> C ) Fn X ) -> ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) = ( x e. X |-> C ) <-> A. z e. X ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z ) = ( ( x e. X |-> C ) ` z ) ) ) |
55 |
51 53 54
|
syl2anc |
|- ( ph -> ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) = ( x e. X |-> C ) <-> A. z e. X ( ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) ` z ) = ( ( x e. X |-> C ) ` z ) ) ) |
56 |
48 55
|
mpbird |
|- ( ph -> ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) = ( x e. X |-> C ) ) |
57 |
|
cnco |
|- ( ( ( x e. X |-> A ) e. ( J Cn K ) /\ ( y e. Y |-> B ) e. ( K Cn L ) ) -> ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) e. ( J Cn L ) ) |
58 |
2 4 57
|
syl2anc |
|- ( ph -> ( ( y e. Y |-> B ) o. ( x e. X |-> A ) ) e. ( J Cn L ) ) |
59 |
56 58
|
eqeltrrd |
|- ( ph -> ( x e. X |-> C ) e. ( J Cn L ) ) |