Step |
Hyp |
Ref |
Expression |
1 |
|
cncfmptssg.2 |
|- F = ( x e. A |-> E ) |
2 |
|
cncfmptssg.3 |
|- ( ph -> F e. ( A -cn-> B ) ) |
3 |
|
cncfmptssg.4 |
|- ( ph -> C C_ A ) |
4 |
|
cncfmptssg.5 |
|- ( ph -> D C_ B ) |
5 |
|
cncfmptssg.6 |
|- ( ( ph /\ x e. C ) -> E e. D ) |
6 |
5
|
fmpttd |
|- ( ph -> ( x e. C |-> E ) : C --> D ) |
7 |
|
cncfrss2 |
|- ( F e. ( A -cn-> B ) -> B C_ CC ) |
8 |
2 7
|
syl |
|- ( ph -> B C_ CC ) |
9 |
4 8
|
sstrd |
|- ( ph -> D C_ CC ) |
10 |
3
|
sselda |
|- ( ( ph /\ x e. C ) -> x e. A ) |
11 |
1
|
fvmpt2 |
|- ( ( x e. A /\ E e. D ) -> ( F ` x ) = E ) |
12 |
10 5 11
|
syl2anc |
|- ( ( ph /\ x e. C ) -> ( F ` x ) = E ) |
13 |
12
|
mpteq2dva |
|- ( ph -> ( x e. C |-> ( F ` x ) ) = ( x e. C |-> E ) ) |
14 |
|
nfmpt1 |
|- F/_ x ( x e. A |-> E ) |
15 |
1 14
|
nfcxfr |
|- F/_ x F |
16 |
15 2 3
|
cncfmptss |
|- ( ph -> ( x e. C |-> ( F ` x ) ) e. ( C -cn-> B ) ) |
17 |
13 16
|
eqeltrrd |
|- ( ph -> ( x e. C |-> E ) e. ( C -cn-> B ) ) |
18 |
|
cncffvrn |
|- ( ( D C_ CC /\ ( x e. C |-> E ) e. ( C -cn-> B ) ) -> ( ( x e. C |-> E ) e. ( C -cn-> D ) <-> ( x e. C |-> E ) : C --> D ) ) |
19 |
9 17 18
|
syl2anc |
|- ( ph -> ( ( x e. C |-> E ) e. ( C -cn-> D ) <-> ( x e. C |-> E ) : C --> D ) ) |
20 |
6 19
|
mpbird |
|- ( ph -> ( x e. C |-> E ) e. ( C -cn-> D ) ) |