Step |
Hyp |
Ref |
Expression |
1 |
|
ptcn.2 |
|- K = ( Xt_ ` F ) |
2 |
|
ptcn.3 |
|- ( ph -> J e. ( TopOn ` X ) ) |
3 |
|
ptcn.4 |
|- ( ph -> I e. V ) |
4 |
|
ptcn.5 |
|- ( ph -> F : I --> Top ) |
5 |
|
ptcn.6 |
|- ( ( ph /\ k e. I ) -> ( x e. X |-> A ) e. ( J Cn ( F ` k ) ) ) |
6 |
2
|
adantr |
|- ( ( ph /\ k e. I ) -> J e. ( TopOn ` X ) ) |
7 |
4
|
ffvelrnda |
|- ( ( ph /\ k e. I ) -> ( F ` k ) e. Top ) |
8 |
|
toptopon2 |
|- ( ( F ` k ) e. Top <-> ( F ` k ) e. ( TopOn ` U. ( F ` k ) ) ) |
9 |
7 8
|
sylib |
|- ( ( ph /\ k e. I ) -> ( F ` k ) e. ( TopOn ` U. ( F ` k ) ) ) |
10 |
|
cnf2 |
|- ( ( J e. ( TopOn ` X ) /\ ( F ` k ) e. ( TopOn ` U. ( F ` k ) ) /\ ( x e. X |-> A ) e. ( J Cn ( F ` k ) ) ) -> ( x e. X |-> A ) : X --> U. ( F ` k ) ) |
11 |
6 9 5 10
|
syl3anc |
|- ( ( ph /\ k e. I ) -> ( x e. X |-> A ) : X --> U. ( F ` k ) ) |
12 |
11
|
fvmptelrn |
|- ( ( ( ph /\ k e. I ) /\ x e. X ) -> A e. U. ( F ` k ) ) |
13 |
12
|
an32s |
|- ( ( ( ph /\ x e. X ) /\ k e. I ) -> A e. U. ( F ` k ) ) |
14 |
13
|
ralrimiva |
|- ( ( ph /\ x e. X ) -> A. k e. I A e. U. ( F ` k ) ) |
15 |
3
|
adantr |
|- ( ( ph /\ x e. X ) -> I e. V ) |
16 |
|
mptelixpg |
|- ( I e. V -> ( ( k e. I |-> A ) e. X_ k e. I U. ( F ` k ) <-> A. k e. I A e. U. ( F ` k ) ) ) |
17 |
15 16
|
syl |
|- ( ( ph /\ x e. X ) -> ( ( k e. I |-> A ) e. X_ k e. I U. ( F ` k ) <-> A. k e. I A e. U. ( F ` k ) ) ) |
18 |
14 17
|
mpbird |
|- ( ( ph /\ x e. X ) -> ( k e. I |-> A ) e. X_ k e. I U. ( F ` k ) ) |
19 |
1
|
ptuni |
|- ( ( I e. V /\ F : I --> Top ) -> X_ k e. I U. ( F ` k ) = U. K ) |
20 |
3 4 19
|
syl2anc |
|- ( ph -> X_ k e. I U. ( F ` k ) = U. K ) |
21 |
20
|
adantr |
|- ( ( ph /\ x e. X ) -> X_ k e. I U. ( F ` k ) = U. K ) |
22 |
18 21
|
eleqtrd |
|- ( ( ph /\ x e. X ) -> ( k e. I |-> A ) e. U. K ) |
23 |
22
|
fmpttd |
|- ( ph -> ( x e. X |-> ( k e. I |-> A ) ) : X --> U. K ) |
24 |
2
|
adantr |
|- ( ( ph /\ z e. X ) -> J e. ( TopOn ` X ) ) |
25 |
3
|
adantr |
|- ( ( ph /\ z e. X ) -> I e. V ) |
26 |
4
|
adantr |
|- ( ( ph /\ z e. X ) -> F : I --> Top ) |
27 |
|
simpr |
|- ( ( ph /\ z e. X ) -> z e. X ) |
28 |
5
|
adantlr |
|- ( ( ( ph /\ z e. X ) /\ k e. I ) -> ( x e. X |-> A ) e. ( J Cn ( F ` k ) ) ) |
29 |
|
simplr |
|- ( ( ( ph /\ z e. X ) /\ k e. I ) -> z e. X ) |
30 |
|
toponuni |
|- ( J e. ( TopOn ` X ) -> X = U. J ) |
31 |
2 30
|
syl |
|- ( ph -> X = U. J ) |
32 |
31
|
ad2antrr |
|- ( ( ( ph /\ z e. X ) /\ k e. I ) -> X = U. J ) |
33 |
29 32
|
eleqtrd |
|- ( ( ( ph /\ z e. X ) /\ k e. I ) -> z e. U. J ) |
34 |
|
eqid |
|- U. J = U. J |
35 |
34
|
cncnpi |
|- ( ( ( x e. X |-> A ) e. ( J Cn ( F ` k ) ) /\ z e. U. J ) -> ( x e. X |-> A ) e. ( ( J CnP ( F ` k ) ) ` z ) ) |
36 |
28 33 35
|
syl2anc |
|- ( ( ( ph /\ z e. X ) /\ k e. I ) -> ( x e. X |-> A ) e. ( ( J CnP ( F ` k ) ) ` z ) ) |
37 |
1 24 25 26 27 36
|
ptcnp |
|- ( ( ph /\ z e. X ) -> ( x e. X |-> ( k e. I |-> A ) ) e. ( ( J CnP K ) ` z ) ) |
38 |
37
|
ralrimiva |
|- ( ph -> A. z e. X ( x e. X |-> ( k e. I |-> A ) ) e. ( ( J CnP K ) ` z ) ) |
39 |
|
pttop |
|- ( ( I e. V /\ F : I --> Top ) -> ( Xt_ ` F ) e. Top ) |
40 |
3 4 39
|
syl2anc |
|- ( ph -> ( Xt_ ` F ) e. Top ) |
41 |
1 40
|
eqeltrid |
|- ( ph -> K e. Top ) |
42 |
|
toptopon2 |
|- ( K e. Top <-> K e. ( TopOn ` U. K ) ) |
43 |
41 42
|
sylib |
|- ( ph -> K e. ( TopOn ` U. K ) ) |
44 |
|
cncnp |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` U. K ) ) -> ( ( x e. X |-> ( k e. I |-> A ) ) e. ( J Cn K ) <-> ( ( x e. X |-> ( k e. I |-> A ) ) : X --> U. K /\ A. z e. X ( x e. X |-> ( k e. I |-> A ) ) e. ( ( J CnP K ) ` z ) ) ) ) |
45 |
2 43 44
|
syl2anc |
|- ( ph -> ( ( x e. X |-> ( k e. I |-> A ) ) e. ( J Cn K ) <-> ( ( x e. X |-> ( k e. I |-> A ) ) : X --> U. K /\ A. z e. X ( x e. X |-> ( k e. I |-> A ) ) e. ( ( J CnP K ) ` z ) ) ) ) |
46 |
23 38 45
|
mpbir2and |
|- ( ph -> ( x e. X |-> ( k e. I |-> A ) ) e. ( J Cn K ) ) |