Step |
Hyp |
Ref |
Expression |
1 |
|
cnprest.1 |
|- X = U. J |
2 |
|
cnprest.2 |
|- Y = U. K |
3 |
|
cnptop2 |
|- ( F e. ( ( J CnP K ) ` P ) -> K e. Top ) |
4 |
3
|
a1i |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) ) -> ( F e. ( ( J CnP K ) ` P ) -> K e. Top ) ) |
5 |
|
cnptop2 |
|- ( ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) -> K e. Top ) |
6 |
5
|
a1i |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) ) -> ( ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) -> K e. Top ) ) |
7 |
1
|
ntrss2 |
|- ( ( J e. Top /\ A C_ X ) -> ( ( int ` J ) ` A ) C_ A ) |
8 |
7
|
3ad2ant1 |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( int ` J ) ` A ) C_ A ) |
9 |
|
simp2l |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> P e. ( ( int ` J ) ` A ) ) |
10 |
8 9
|
sseldd |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> P e. A ) |
11 |
10
|
fvresd |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( F |` A ) ` P ) = ( F ` P ) ) |
12 |
11
|
eqcomd |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( F ` P ) = ( ( F |` A ) ` P ) ) |
13 |
12
|
eleq1d |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( F ` P ) e. y <-> ( ( F |` A ) ` P ) e. y ) ) |
14 |
|
inss1 |
|- ( x i^i A ) C_ x |
15 |
|
imass2 |
|- ( ( x i^i A ) C_ x -> ( F " ( x i^i A ) ) C_ ( F " x ) ) |
16 |
|
sstr2 |
|- ( ( F " ( x i^i A ) ) C_ ( F " x ) -> ( ( F " x ) C_ y -> ( F " ( x i^i A ) ) C_ y ) ) |
17 |
14 15 16
|
mp2b |
|- ( ( F " x ) C_ y -> ( F " ( x i^i A ) ) C_ y ) |
18 |
17
|
anim2i |
|- ( ( P e. x /\ ( F " x ) C_ y ) -> ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) ) |
19 |
18
|
reximi |
|- ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) -> E. x e. J ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) ) |
20 |
|
simp1l |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> J e. Top ) |
21 |
1
|
ntropn |
|- ( ( J e. Top /\ A C_ X ) -> ( ( int ` J ) ` A ) e. J ) |
22 |
21
|
3ad2ant1 |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( int ` J ) ` A ) e. J ) |
23 |
|
inopn |
|- ( ( J e. Top /\ x e. J /\ ( ( int ` J ) ` A ) e. J ) -> ( x i^i ( ( int ` J ) ` A ) ) e. J ) |
24 |
23
|
3com23 |
|- ( ( J e. Top /\ ( ( int ` J ) ` A ) e. J /\ x e. J ) -> ( x i^i ( ( int ` J ) ` A ) ) e. J ) |
25 |
24
|
3expia |
|- ( ( J e. Top /\ ( ( int ` J ) ` A ) e. J ) -> ( x e. J -> ( x i^i ( ( int ` J ) ` A ) ) e. J ) ) |
26 |
20 22 25
|
syl2anc |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( x e. J -> ( x i^i ( ( int ` J ) ` A ) ) e. J ) ) |
27 |
|
elin |
|- ( P e. ( x i^i ( ( int ` J ) ` A ) ) <-> ( P e. x /\ P e. ( ( int ` J ) ` A ) ) ) |
28 |
27
|
simplbi2com |
|- ( P e. ( ( int ` J ) ` A ) -> ( P e. x -> P e. ( x i^i ( ( int ` J ) ` A ) ) ) ) |
29 |
9 28
|
syl |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( P e. x -> P e. ( x i^i ( ( int ` J ) ` A ) ) ) ) |
30 |
|
sslin |
|- ( ( ( int ` J ) ` A ) C_ A -> ( x i^i ( ( int ` J ) ` A ) ) C_ ( x i^i A ) ) |
31 |
8 30
|
syl |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( x i^i ( ( int ` J ) ` A ) ) C_ ( x i^i A ) ) |
32 |
|
imass2 |
|- ( ( x i^i ( ( int ` J ) ` A ) ) C_ ( x i^i A ) -> ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ ( F " ( x i^i A ) ) ) |
33 |
31 32
|
syl |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ ( F " ( x i^i A ) ) ) |
34 |
|
sstr2 |
|- ( ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ ( F " ( x i^i A ) ) -> ( ( F " ( x i^i A ) ) C_ y -> ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ y ) ) |
35 |
33 34
|
syl |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( F " ( x i^i A ) ) C_ y -> ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ y ) ) |
36 |
29 35
|
anim12d |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) -> ( P e. ( x i^i ( ( int ` J ) ` A ) ) /\ ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ y ) ) ) |
37 |
26 36
|
anim12d |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( x e. J /\ ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) ) -> ( ( x i^i ( ( int ` J ) ` A ) ) e. J /\ ( P e. ( x i^i ( ( int ` J ) ` A ) ) /\ ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ y ) ) ) ) |
38 |
|
eleq2 |
|- ( z = ( x i^i ( ( int ` J ) ` A ) ) -> ( P e. z <-> P e. ( x i^i ( ( int ` J ) ` A ) ) ) ) |
39 |
|
imaeq2 |
|- ( z = ( x i^i ( ( int ` J ) ` A ) ) -> ( F " z ) = ( F " ( x i^i ( ( int ` J ) ` A ) ) ) ) |
40 |
39
|
sseq1d |
|- ( z = ( x i^i ( ( int ` J ) ` A ) ) -> ( ( F " z ) C_ y <-> ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ y ) ) |
41 |
38 40
|
anbi12d |
|- ( z = ( x i^i ( ( int ` J ) ` A ) ) -> ( ( P e. z /\ ( F " z ) C_ y ) <-> ( P e. ( x i^i ( ( int ` J ) ` A ) ) /\ ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ y ) ) ) |
42 |
41
|
rspcev |
|- ( ( ( x i^i ( ( int ` J ) ` A ) ) e. J /\ ( P e. ( x i^i ( ( int ` J ) ` A ) ) /\ ( F " ( x i^i ( ( int ` J ) ` A ) ) ) C_ y ) ) -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) ) |
43 |
37 42
|
syl6 |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( x e. J /\ ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) ) -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) ) ) |
44 |
43
|
expdimp |
|- ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ x e. J ) -> ( ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) ) ) |
45 |
44
|
rexlimdva |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( E. x e. J ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) -> E. z e. J ( P e. z /\ ( F " z ) C_ y ) ) ) |
46 |
|
eleq2 |
|- ( z = x -> ( P e. z <-> P e. x ) ) |
47 |
|
imaeq2 |
|- ( z = x -> ( F " z ) = ( F " x ) ) |
48 |
47
|
sseq1d |
|- ( z = x -> ( ( F " z ) C_ y <-> ( F " x ) C_ y ) ) |
49 |
46 48
|
anbi12d |
|- ( z = x -> ( ( P e. z /\ ( F " z ) C_ y ) <-> ( P e. x /\ ( F " x ) C_ y ) ) ) |
50 |
49
|
cbvrexvw |
|- ( E. z e. J ( P e. z /\ ( F " z ) C_ y ) <-> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) |
51 |
45 50
|
syl6ib |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( E. x e. J ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) |
52 |
19 51
|
impbid2 |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( E. x e. J ( P e. x /\ ( F " x ) C_ y ) <-> E. x e. J ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) ) ) |
53 |
|
vex |
|- x e. _V |
54 |
53
|
inex1 |
|- ( x i^i A ) e. _V |
55 |
54
|
a1i |
|- ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ x e. J ) -> ( x i^i A ) e. _V ) |
56 |
20
|
uniexd |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> U. J e. _V ) |
57 |
|
simp1r |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> A C_ X ) |
58 |
57 1
|
sseqtrdi |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> A C_ U. J ) |
59 |
56 58
|
ssexd |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> A e. _V ) |
60 |
|
elrest |
|- ( ( J e. Top /\ A e. _V ) -> ( z e. ( J |`t A ) <-> E. x e. J z = ( x i^i A ) ) ) |
61 |
20 59 60
|
syl2anc |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( z e. ( J |`t A ) <-> E. x e. J z = ( x i^i A ) ) ) |
62 |
|
eleq2 |
|- ( z = ( x i^i A ) -> ( P e. z <-> P e. ( x i^i A ) ) ) |
63 |
|
elin |
|- ( P e. ( x i^i A ) <-> ( P e. x /\ P e. A ) ) |
64 |
63
|
rbaib |
|- ( P e. A -> ( P e. ( x i^i A ) <-> P e. x ) ) |
65 |
10 64
|
syl |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( P e. ( x i^i A ) <-> P e. x ) ) |
66 |
62 65
|
sylan9bbr |
|- ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ z = ( x i^i A ) ) -> ( P e. z <-> P e. x ) ) |
67 |
|
simpr |
|- ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ z = ( x i^i A ) ) -> z = ( x i^i A ) ) |
68 |
67
|
imaeq2d |
|- ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ z = ( x i^i A ) ) -> ( ( F |` A ) " z ) = ( ( F |` A ) " ( x i^i A ) ) ) |
69 |
|
inss2 |
|- ( x i^i A ) C_ A |
70 |
|
resima2 |
|- ( ( x i^i A ) C_ A -> ( ( F |` A ) " ( x i^i A ) ) = ( F " ( x i^i A ) ) ) |
71 |
69 70
|
ax-mp |
|- ( ( F |` A ) " ( x i^i A ) ) = ( F " ( x i^i A ) ) |
72 |
68 71
|
eqtrdi |
|- ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ z = ( x i^i A ) ) -> ( ( F |` A ) " z ) = ( F " ( x i^i A ) ) ) |
73 |
72
|
sseq1d |
|- ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ z = ( x i^i A ) ) -> ( ( ( F |` A ) " z ) C_ y <-> ( F " ( x i^i A ) ) C_ y ) ) |
74 |
66 73
|
anbi12d |
|- ( ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) /\ z = ( x i^i A ) ) -> ( ( P e. z /\ ( ( F |` A ) " z ) C_ y ) <-> ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) ) ) |
75 |
55 61 74
|
rexxfr2d |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) <-> E. x e. J ( P e. x /\ ( F " ( x i^i A ) ) C_ y ) ) ) |
76 |
52 75
|
bitr4d |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( 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 ) ) ) |
77 |
13 76
|
imbi12d |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) <-> ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) ) |
78 |
77
|
ralbidv |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) <-> A. y e. K ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) ) |
79 |
|
simp2r |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> F : X --> Y ) |
80 |
|
simp3 |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> K e. Top ) |
81 |
57 10
|
sseldd |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> P e. X ) |
82 |
1 2
|
iscnp2 |
|- ( F e. ( ( J CnP K ) ` P ) <-> ( ( J e. Top /\ K e. Top /\ P e. X ) /\ ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) ) |
83 |
82
|
baib |
|- ( ( J e. Top /\ K e. Top /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) ) |
84 |
20 80 81 83
|
syl3anc |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) ) |
85 |
79 84
|
mpbirand |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( F e. ( ( J CnP K ) ` P ) <-> A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) |
86 |
79 57
|
fssresd |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( F |` A ) : A --> Y ) |
87 |
1
|
toptopon |
|- ( J e. Top <-> J e. ( TopOn ` X ) ) |
88 |
20 87
|
sylib |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> J e. ( TopOn ` X ) ) |
89 |
|
resttopon |
|- ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) e. ( TopOn ` A ) ) |
90 |
88 57 89
|
syl2anc |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( J |`t A ) e. ( TopOn ` A ) ) |
91 |
2
|
toptopon |
|- ( K e. Top <-> K e. ( TopOn ` Y ) ) |
92 |
80 91
|
sylib |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> K e. ( TopOn ` Y ) ) |
93 |
|
iscnp |
|- ( ( ( J |`t A ) e. ( TopOn ` A ) /\ K e. ( TopOn ` Y ) /\ P e. A ) -> ( ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) <-> ( ( F |` A ) : A --> Y /\ A. y e. K ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) ) ) |
94 |
90 92 10 93
|
syl3anc |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) <-> ( ( F |` A ) : A --> Y /\ A. y e. K ( ( ( F |` A ) ` P ) e. y -> E. z e. ( J |`t A ) ( P e. z /\ ( ( F |` A ) " z ) C_ y ) ) ) ) ) |
95 |
86 94
|
mpbirand |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( ( F |` A ) e. ( ( ( J |`t A ) 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 ) ) ) ) |
96 |
78 85 95
|
3bitr4d |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) /\ K e. Top ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) ) ) |
97 |
96
|
3expia |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) ) -> ( K e. Top -> ( F e. ( ( J CnP K ) ` P ) <-> ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) ) ) ) |
98 |
4 6 97
|
pm5.21ndd |
|- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F |` A ) e. ( ( ( J |`t A ) CnP K ) ` P ) ) ) |