Step |
Hyp |
Ref |
Expression |
1 |
|
subbascn.1 |
|- ( ph -> J e. ( TopOn ` X ) ) |
2 |
|
subbascn.2 |
|- ( ph -> B e. V ) |
3 |
|
subbascn.3 |
|- ( ph -> K = ( topGen ` ( fi ` B ) ) ) |
4 |
|
subbascn.4 |
|- ( ph -> K e. ( TopOn ` Y ) ) |
5 |
1 3 4
|
tgcn |
|- ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. ( fi ` B ) ( `' F " y ) e. J ) ) ) |
6 |
2
|
adantr |
|- ( ( ph /\ F : X --> Y ) -> B e. V ) |
7 |
|
ssfii |
|- ( B e. V -> B C_ ( fi ` B ) ) |
8 |
|
ssralv |
|- ( B C_ ( fi ` B ) -> ( A. y e. ( fi ` B ) ( `' F " y ) e. J -> A. y e. B ( `' F " y ) e. J ) ) |
9 |
6 7 8
|
3syl |
|- ( ( ph /\ F : X --> Y ) -> ( A. y e. ( fi ` B ) ( `' F " y ) e. J -> A. y e. B ( `' F " y ) e. J ) ) |
10 |
|
vex |
|- x e. _V |
11 |
|
elfi |
|- ( ( x e. _V /\ B e. V ) -> ( x e. ( fi ` B ) <-> E. z e. ( ~P B i^i Fin ) x = |^| z ) ) |
12 |
10 6 11
|
sylancr |
|- ( ( ph /\ F : X --> Y ) -> ( x e. ( fi ` B ) <-> E. z e. ( ~P B i^i Fin ) x = |^| z ) ) |
13 |
|
simpr2 |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> x = |^| z ) |
14 |
13
|
imaeq2d |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> ( `' F " x ) = ( `' F " |^| z ) ) |
15 |
|
ffun |
|- ( F : X --> Y -> Fun F ) |
16 |
15
|
ad2antlr |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> Fun F ) |
17 |
13 10
|
eqeltrrdi |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> |^| z e. _V ) |
18 |
|
intex |
|- ( z =/= (/) <-> |^| z e. _V ) |
19 |
17 18
|
sylibr |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> z =/= (/) ) |
20 |
|
intpreima |
|- ( ( Fun F /\ z =/= (/) ) -> ( `' F " |^| z ) = |^|_ y e. z ( `' F " y ) ) |
21 |
16 19 20
|
syl2anc |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> ( `' F " |^| z ) = |^|_ y e. z ( `' F " y ) ) |
22 |
14 21
|
eqtrd |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> ( `' F " x ) = |^|_ y e. z ( `' F " y ) ) |
23 |
|
topontop |
|- ( J e. ( TopOn ` X ) -> J e. Top ) |
24 |
1 23
|
syl |
|- ( ph -> J e. Top ) |
25 |
24
|
ad2antrr |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> J e. Top ) |
26 |
|
simpr1 |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> z e. ( ~P B i^i Fin ) ) |
27 |
26
|
elin2d |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> z e. Fin ) |
28 |
26
|
elin1d |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> z e. ~P B ) |
29 |
28
|
elpwid |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> z C_ B ) |
30 |
|
simpr3 |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> A. y e. B ( `' F " y ) e. J ) |
31 |
|
ssralv |
|- ( z C_ B -> ( A. y e. B ( `' F " y ) e. J -> A. y e. z ( `' F " y ) e. J ) ) |
32 |
29 30 31
|
sylc |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> A. y e. z ( `' F " y ) e. J ) |
33 |
|
iinopn |
|- ( ( J e. Top /\ ( z e. Fin /\ z =/= (/) /\ A. y e. z ( `' F " y ) e. J ) ) -> |^|_ y e. z ( `' F " y ) e. J ) |
34 |
25 27 19 32 33
|
syl13anc |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> |^|_ y e. z ( `' F " y ) e. J ) |
35 |
22 34
|
eqeltrd |
|- ( ( ( ph /\ F : X --> Y ) /\ ( z e. ( ~P B i^i Fin ) /\ x = |^| z /\ A. y e. B ( `' F " y ) e. J ) ) -> ( `' F " x ) e. J ) |
36 |
35
|
3exp2 |
|- ( ( ph /\ F : X --> Y ) -> ( z e. ( ~P B i^i Fin ) -> ( x = |^| z -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) ) ) |
37 |
36
|
rexlimdv |
|- ( ( ph /\ F : X --> Y ) -> ( E. z e. ( ~P B i^i Fin ) x = |^| z -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) ) |
38 |
12 37
|
sylbid |
|- ( ( ph /\ F : X --> Y ) -> ( x e. ( fi ` B ) -> ( A. y e. B ( `' F " y ) e. J -> ( `' F " x ) e. J ) ) ) |
39 |
38
|
com23 |
|- ( ( ph /\ F : X --> Y ) -> ( A. y e. B ( `' F " y ) e. J -> ( x e. ( fi ` B ) -> ( `' F " x ) e. J ) ) ) |
40 |
39
|
ralrimdv |
|- ( ( ph /\ F : X --> Y ) -> ( A. y e. B ( `' F " y ) e. J -> A. x e. ( fi ` B ) ( `' F " x ) e. J ) ) |
41 |
|
imaeq2 |
|- ( y = x -> ( `' F " y ) = ( `' F " x ) ) |
42 |
41
|
eleq1d |
|- ( y = x -> ( ( `' F " y ) e. J <-> ( `' F " x ) e. J ) ) |
43 |
42
|
cbvralvw |
|- ( A. y e. ( fi ` B ) ( `' F " y ) e. J <-> A. x e. ( fi ` B ) ( `' F " x ) e. J ) |
44 |
40 43
|
syl6ibr |
|- ( ( ph /\ F : X --> Y ) -> ( A. y e. B ( `' F " y ) e. J -> A. y e. ( fi ` B ) ( `' F " y ) e. J ) ) |
45 |
9 44
|
impbid |
|- ( ( ph /\ F : X --> Y ) -> ( A. y e. ( fi ` B ) ( `' F " y ) e. J <-> A. y e. B ( `' F " y ) e. J ) ) |
46 |
45
|
pm5.32da |
|- ( ph -> ( ( F : X --> Y /\ A. y e. ( fi ` B ) ( `' F " y ) e. J ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) ) |
47 |
5 46
|
bitrd |
|- ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) ) |