Step |
Hyp |
Ref |
Expression |
1 |
|
cnprest.1 |
|- X = U. J |
2 |
|
eqid |
|- U. K = U. K |
3 |
1 2
|
cnpf |
|- ( F e. ( ( J CnP K ) ` P ) -> F : X --> U. K ) |
4 |
3
|
3ad2ant3 |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> U. K ) |
5 |
|
simp1 |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> A C_ X ) |
6 |
4 5
|
fssresd |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( F |` A ) : A --> U. K ) |
7 |
|
simpl2 |
|- ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. K ) -> P e. A ) |
8 |
7
|
fvresd |
|- ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. K ) -> ( ( F |` A ) ` P ) = ( F ` P ) ) |
9 |
8
|
eleq1d |
|- ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. K ) -> ( ( ( F |` A ) ` P ) e. y <-> ( F ` P ) e. y ) ) |
10 |
|
cnpimaex |
|- ( ( F e. ( ( J CnP K ) ` P ) /\ y e. K /\ ( F ` P ) e. y ) -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) |
11 |
10
|
3expia |
|- ( ( F e. ( ( J CnP K ) ` P ) /\ y e. K ) -> ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) |
12 |
11
|
3ad2antl3 |
|- ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. K ) -> ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) |
13 |
|
idd |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( P e. x -> P e. x ) ) |
14 |
|
simp2 |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> P e. A ) |
15 |
13 14
|
jctird |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( P e. x -> ( P e. x /\ P e. A ) ) ) |
16 |
|
elin |
|- ( P e. ( x i^i A ) <-> ( P e. x /\ P e. A ) ) |
17 |
15 16
|
syl6ibr |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( P e. x -> P e. ( x i^i A ) ) ) |
18 |
|
inss1 |
|- ( x i^i A ) C_ x |
19 |
|
imass2 |
|- ( ( x i^i A ) C_ x -> ( F " ( x i^i A ) ) C_ ( F " x ) ) |
20 |
18 19
|
ax-mp |
|- ( F " ( x i^i A ) ) C_ ( F " x ) |
21 |
|
id |
|- ( ( F " x ) C_ y -> ( F " x ) C_ y ) |
22 |
20 21
|
sstrid |
|- ( ( F " x ) C_ y -> ( F " ( x i^i A ) ) C_ y ) |
23 |
17 22
|
anim12d1 |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( ( P e. x /\ ( F " x ) C_ y ) -> ( P e. ( x i^i A ) /\ ( F " ( x i^i A ) ) C_ y ) ) ) |
24 |
23
|
reximdv |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) -> E. x e. J ( P e. ( x i^i A ) /\ ( F " ( x i^i A ) ) C_ y ) ) ) |
25 |
|
vex |
|- x e. _V |
26 |
25
|
inex1 |
|- ( x i^i A ) e. _V |
27 |
26
|
a1i |
|- ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ x e. J ) -> ( x i^i A ) e. _V ) |
28 |
|
cnptop1 |
|- ( F e. ( ( J CnP K ) ` P ) -> J e. Top ) |
29 |
28
|
3ad2ant3 |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> J e. Top ) |
30 |
29
|
uniexd |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> U. J e. _V ) |
31 |
5 1
|
sseqtrdi |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> A C_ U. J ) |
32 |
30 31
|
ssexd |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> A e. _V ) |
33 |
|
elrest |
|- ( ( J e. Top /\ A e. _V ) -> ( z e. ( J |`t A ) <-> E. x e. J z = ( x i^i A ) ) ) |
34 |
29 32 33
|
syl2anc |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( z e. ( J |`t A ) <-> E. x e. J z = ( x i^i A ) ) ) |
35 |
|
simpr |
|- ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ z = ( x i^i A ) ) -> z = ( x i^i A ) ) |
36 |
35
|
eleq2d |
|- ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ z = ( x i^i A ) ) -> ( P e. z <-> P e. ( x i^i A ) ) ) |
37 |
35
|
imaeq2d |
|- ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ z = ( x i^i A ) ) -> ( ( F |` A ) " z ) = ( ( F |` A ) " ( x i^i A ) ) ) |
38 |
|
inss2 |
|- ( x i^i A ) C_ A |
39 |
|
resima2 |
|- ( ( x i^i A ) C_ A -> ( ( F |` A ) " ( x i^i A ) ) = ( F " ( x i^i A ) ) ) |
40 |
38 39
|
ax-mp |
|- ( ( F |` A ) " ( x i^i A ) ) = ( F " ( x i^i A ) ) |
41 |
37 40
|
eqtrdi |
|- ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ z = ( x i^i A ) ) -> ( ( F |` A ) " z ) = ( F " ( x i^i A ) ) ) |
42 |
41
|
sseq1d |
|- ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ z = ( x i^i A ) ) -> ( ( ( F |` A ) " z ) C_ y <-> ( F " ( x i^i A ) ) C_ y ) ) |
43 |
36 42
|
anbi12d |
|- ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ z = ( x i^i A ) ) -> ( ( P e. z /\ ( ( F |` A ) " z ) C_ y ) <-> ( P e. ( x i^i A ) /\ ( F " ( x i^i A ) ) C_ y ) ) ) |
44 |
27 34 43
|
rexxfr2d |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) <-> E. x e. J ( P e. ( x i^i A ) /\ ( F " ( x i^i A ) ) C_ y ) ) ) |
45 |
24 44
|
sylibrd |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) |
46 |
45
|
adantr |
|- ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. K ) -> ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) |
47 |
12 46
|
syld |
|- ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. K ) -> ( ( F ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) |
48 |
9 47
|
sylbid |
|- ( ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) /\ y e. K ) -> ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) |
49 |
48
|
ralrimiva |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> A. y e. K ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) |
50 |
1
|
toptopon |
|- ( J e. Top <-> J e. ( TopOn ` X ) ) |
51 |
29 50
|
sylib |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> J e. ( TopOn ` X ) ) |
52 |
|
resttopon |
|- ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) e. ( TopOn ` A ) ) |
53 |
51 5 52
|
syl2anc |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( J |`t A ) e. ( TopOn ` A ) ) |
54 |
|
cnptop2 |
|- ( F e. ( ( J CnP K ) ` P ) -> K e. Top ) |
55 |
54
|
3ad2ant3 |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> K e. Top ) |
56 |
2
|
toptopon |
|- ( K e. Top <-> K e. ( TopOn ` U. K ) ) |
57 |
55 56
|
sylib |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> K e. ( TopOn ` U. K ) ) |
58 |
|
iscnp |
|- ( ( ( J |`t A ) e. ( TopOn ` A ) /\ K e. ( TopOn ` U. K ) /\ P e. A ) -> ( ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) <-> ( ( F |` A ) : A --> U. K /\ A. y e. K ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) ) ) |
59 |
53 57 14 58
|
syl3anc |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) <-> ( ( F |` A ) : A --> U. K /\ A. y e. K ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) ) ) |
60 |
6 49 59
|
mpbir2and |
|- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) ) |