Step |
Hyp |
Ref |
Expression |
1 |
|
cncfmpt2ss.1 |
|- J = ( TopOpen ` CCfld ) |
2 |
|
cncfmpt2ss.2 |
|- F e. ( ( J tX J ) Cn J ) |
3 |
|
cncfmpt2ss.3 |
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> S ) ) |
4 |
|
cncfmpt2ss.4 |
|- ( ph -> ( x e. X |-> B ) e. ( X -cn-> S ) ) |
5 |
|
cncfmpt2ss.5 |
|- S C_ CC |
6 |
|
cncfmpt2ss.6 |
|- ( ( A e. S /\ B e. S ) -> ( A F B ) e. S ) |
7 |
|
cncff |
|- ( ( x e. X |-> A ) e. ( X -cn-> S ) -> ( x e. X |-> A ) : X --> S ) |
8 |
3 7
|
syl |
|- ( ph -> ( x e. X |-> A ) : X --> S ) |
9 |
8
|
fvmptelrn |
|- ( ( ph /\ x e. X ) -> A e. S ) |
10 |
|
cncff |
|- ( ( x e. X |-> B ) e. ( X -cn-> S ) -> ( x e. X |-> B ) : X --> S ) |
11 |
4 10
|
syl |
|- ( ph -> ( x e. X |-> B ) : X --> S ) |
12 |
11
|
fvmptelrn |
|- ( ( ph /\ x e. X ) -> B e. S ) |
13 |
9 12 6
|
syl2anc |
|- ( ( ph /\ x e. X ) -> ( A F B ) e. S ) |
14 |
13
|
fmpttd |
|- ( ph -> ( x e. X |-> ( A F B ) ) : X --> S ) |
15 |
2
|
a1i |
|- ( ph -> F e. ( ( J tX J ) Cn J ) ) |
16 |
|
ssid |
|- CC C_ CC |
17 |
|
cncfss |
|- ( ( S C_ CC /\ CC C_ CC ) -> ( X -cn-> S ) C_ ( X -cn-> CC ) ) |
18 |
5 16 17
|
mp2an |
|- ( X -cn-> S ) C_ ( X -cn-> CC ) |
19 |
18 3
|
sselid |
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) ) |
20 |
18 4
|
sselid |
|- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) ) |
21 |
1 15 19 20
|
cncfmpt2f |
|- ( ph -> ( x e. X |-> ( A F B ) ) e. ( X -cn-> CC ) ) |
22 |
|
cncffvrn |
|- ( ( S C_ CC /\ ( x e. X |-> ( A F B ) ) e. ( X -cn-> CC ) ) -> ( ( x e. X |-> ( A F B ) ) e. ( X -cn-> S ) <-> ( x e. X |-> ( A F B ) ) : X --> S ) ) |
23 |
5 21 22
|
sylancr |
|- ( ph -> ( ( x e. X |-> ( A F B ) ) e. ( X -cn-> S ) <-> ( x e. X |-> ( A F B ) ) : X --> S ) ) |
24 |
14 23
|
mpbird |
|- ( ph -> ( x e. X |-> ( A F B ) ) e. ( X -cn-> S ) ) |