Step |
Hyp |
Ref |
Expression |
1 |
|
cncfcompt2.xph |
|- F/ x ph |
2 |
|
cncfcompt2.ab |
|- ( ph -> ( x e. A |-> R ) e. ( A -cn-> B ) ) |
3 |
|
cncfcompt2.cd |
|- ( ph -> ( y e. C |-> S ) e. ( C -cn-> E ) ) |
4 |
|
cncfcompt2.bc |
|- ( ph -> B C_ C ) |
5 |
|
cncfcompt2.st |
|- ( y = R -> S = T ) |
6 |
4
|
adantr |
|- ( ( ph /\ x e. A ) -> B C_ C ) |
7 |
|
cncff |
|- ( ( x e. A |-> R ) e. ( A -cn-> B ) -> ( x e. A |-> R ) : A --> B ) |
8 |
2 7
|
syl |
|- ( ph -> ( x e. A |-> R ) : A --> B ) |
9 |
8
|
fvmptelrn |
|- ( ( ph /\ x e. A ) -> R e. B ) |
10 |
6 9
|
sseldd |
|- ( ( ph /\ x e. A ) -> R e. C ) |
11 |
10
|
ex |
|- ( ph -> ( x e. A -> R e. C ) ) |
12 |
1 11
|
ralrimi |
|- ( ph -> A. x e. A R e. C ) |
13 |
|
eqidd |
|- ( ph -> ( x e. A |-> R ) = ( x e. A |-> R ) ) |
14 |
|
eqidd |
|- ( ph -> ( y e. C |-> S ) = ( y e. C |-> S ) ) |
15 |
12 13 14 5
|
fmptcof |
|- ( ph -> ( ( y e. C |-> S ) o. ( x e. A |-> R ) ) = ( x e. A |-> T ) ) |
16 |
15
|
eqcomd |
|- ( ph -> ( x e. A |-> T ) = ( ( y e. C |-> S ) o. ( x e. A |-> R ) ) ) |
17 |
|
cncfrss |
|- ( ( y e. C |-> S ) e. ( C -cn-> E ) -> C C_ CC ) |
18 |
3 17
|
syl |
|- ( ph -> C C_ CC ) |
19 |
|
cncfss |
|- ( ( B C_ C /\ C C_ CC ) -> ( A -cn-> B ) C_ ( A -cn-> C ) ) |
20 |
4 18 19
|
syl2anc |
|- ( ph -> ( A -cn-> B ) C_ ( A -cn-> C ) ) |
21 |
20 2
|
sseldd |
|- ( ph -> ( x e. A |-> R ) e. ( A -cn-> C ) ) |
22 |
21 3
|
cncfco |
|- ( ph -> ( ( y e. C |-> S ) o. ( x e. A |-> R ) ) e. ( A -cn-> E ) ) |
23 |
16 22
|
eqeltrd |
|- ( ph -> ( x e. A |-> T ) e. ( A -cn-> E ) ) |