Step |
Hyp |
Ref |
Expression |
1 |
|
fmfnfm.b |
|- ( ph -> B e. ( fBas ` Y ) ) |
2 |
|
fmfnfm.l |
|- ( ph -> L e. ( Fil ` X ) ) |
3 |
|
fmfnfm.f |
|- ( ph -> F : Y --> X ) |
4 |
|
fmfnfm.fm |
|- ( ph -> ( ( X FilMap F ) ` B ) C_ L ) |
5 |
2
|
ad2antrr |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> L e. ( Fil ` X ) ) |
6 |
|
simplr |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> x e. L ) |
7 |
|
ffn |
|- ( F : Y --> X -> F Fn Y ) |
8 |
|
dffn4 |
|- ( F Fn Y <-> F : Y -onto-> ran F ) |
9 |
7 8
|
sylib |
|- ( F : Y --> X -> F : Y -onto-> ran F ) |
10 |
|
foima |
|- ( F : Y -onto-> ran F -> ( F " Y ) = ran F ) |
11 |
3 9 10
|
3syl |
|- ( ph -> ( F " Y ) = ran F ) |
12 |
|
filtop |
|- ( L e. ( Fil ` X ) -> X e. L ) |
13 |
2 12
|
syl |
|- ( ph -> X e. L ) |
14 |
|
fgcl |
|- ( B e. ( fBas ` Y ) -> ( Y filGen B ) e. ( Fil ` Y ) ) |
15 |
|
filtop |
|- ( ( Y filGen B ) e. ( Fil ` Y ) -> Y e. ( Y filGen B ) ) |
16 |
1 14 15
|
3syl |
|- ( ph -> Y e. ( Y filGen B ) ) |
17 |
|
eqid |
|- ( Y filGen B ) = ( Y filGen B ) |
18 |
17
|
imaelfm |
|- ( ( ( X e. L /\ B e. ( fBas ` Y ) /\ F : Y --> X ) /\ Y e. ( Y filGen B ) ) -> ( F " Y ) e. ( ( X FilMap F ) ` B ) ) |
19 |
13 1 3 16 18
|
syl31anc |
|- ( ph -> ( F " Y ) e. ( ( X FilMap F ) ` B ) ) |
20 |
11 19
|
eqeltrrd |
|- ( ph -> ran F e. ( ( X FilMap F ) ` B ) ) |
21 |
4 20
|
sseldd |
|- ( ph -> ran F e. L ) |
22 |
21
|
ad2antrr |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ran F e. L ) |
23 |
|
filin |
|- ( ( L e. ( Fil ` X ) /\ x e. L /\ ran F e. L ) -> ( x i^i ran F ) e. L ) |
24 |
5 6 22 23
|
syl3anc |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( x i^i ran F ) e. L ) |
25 |
|
simprr |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> t C_ X ) |
26 |
|
elin |
|- ( y e. ( x i^i ran F ) <-> ( y e. x /\ y e. ran F ) ) |
27 |
|
fvelrnb |
|- ( F Fn Y -> ( y e. ran F <-> E. z e. Y ( F ` z ) = y ) ) |
28 |
3 7 27
|
3syl |
|- ( ph -> ( y e. ran F <-> E. z e. Y ( F ` z ) = y ) ) |
29 |
28
|
ad2antrr |
|- ( ( ( ph /\ x e. L ) /\ ( F " ( `' F " x ) ) C_ t ) -> ( y e. ran F <-> E. z e. Y ( F ` z ) = y ) ) |
30 |
3
|
ffund |
|- ( ph -> Fun F ) |
31 |
30
|
ad2antrr |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> Fun F ) |
32 |
|
simprr |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> z e. Y ) |
33 |
3
|
fdmd |
|- ( ph -> dom F = Y ) |
34 |
33
|
ad2antrr |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> dom F = Y ) |
35 |
32 34
|
eleqtrrd |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> z e. dom F ) |
36 |
|
fvimacnv |
|- ( ( Fun F /\ z e. dom F ) -> ( ( F ` z ) e. x <-> z e. ( `' F " x ) ) ) |
37 |
31 35 36
|
syl2anc |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> ( ( F ` z ) e. x <-> z e. ( `' F " x ) ) ) |
38 |
|
cnvimass |
|- ( `' F " x ) C_ dom F |
39 |
|
funfvima2 |
|- ( ( Fun F /\ ( `' F " x ) C_ dom F ) -> ( z e. ( `' F " x ) -> ( F ` z ) e. ( F " ( `' F " x ) ) ) ) |
40 |
31 38 39
|
sylancl |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> ( z e. ( `' F " x ) -> ( F ` z ) e. ( F " ( `' F " x ) ) ) ) |
41 |
|
ssel |
|- ( ( F " ( `' F " x ) ) C_ t -> ( ( F ` z ) e. ( F " ( `' F " x ) ) -> ( F ` z ) e. t ) ) |
42 |
41
|
ad2antrl |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> ( ( F ` z ) e. ( F " ( `' F " x ) ) -> ( F ` z ) e. t ) ) |
43 |
40 42
|
syld |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> ( z e. ( `' F " x ) -> ( F ` z ) e. t ) ) |
44 |
37 43
|
sylbid |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> ( ( F ` z ) e. x -> ( F ` z ) e. t ) ) |
45 |
|
eleq1 |
|- ( ( F ` z ) = y -> ( ( F ` z ) e. x <-> y e. x ) ) |
46 |
|
eleq1 |
|- ( ( F ` z ) = y -> ( ( F ` z ) e. t <-> y e. t ) ) |
47 |
45 46
|
imbi12d |
|- ( ( F ` z ) = y -> ( ( ( F ` z ) e. x -> ( F ` z ) e. t ) <-> ( y e. x -> y e. t ) ) ) |
48 |
44 47
|
syl5ibcom |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ z e. Y ) ) -> ( ( F ` z ) = y -> ( y e. x -> y e. t ) ) ) |
49 |
48
|
expr |
|- ( ( ( ph /\ x e. L ) /\ ( F " ( `' F " x ) ) C_ t ) -> ( z e. Y -> ( ( F ` z ) = y -> ( y e. x -> y e. t ) ) ) ) |
50 |
49
|
rexlimdv |
|- ( ( ( ph /\ x e. L ) /\ ( F " ( `' F " x ) ) C_ t ) -> ( E. z e. Y ( F ` z ) = y -> ( y e. x -> y e. t ) ) ) |
51 |
29 50
|
sylbid |
|- ( ( ( ph /\ x e. L ) /\ ( F " ( `' F " x ) ) C_ t ) -> ( y e. ran F -> ( y e. x -> y e. t ) ) ) |
52 |
51
|
impcomd |
|- ( ( ( ph /\ x e. L ) /\ ( F " ( `' F " x ) ) C_ t ) -> ( ( y e. x /\ y e. ran F ) -> y e. t ) ) |
53 |
52
|
adantrr |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( ( y e. x /\ y e. ran F ) -> y e. t ) ) |
54 |
26 53
|
syl5bi |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( y e. ( x i^i ran F ) -> y e. t ) ) |
55 |
54
|
ssrdv |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> ( x i^i ran F ) C_ t ) |
56 |
|
filss |
|- ( ( L e. ( Fil ` X ) /\ ( ( x i^i ran F ) e. L /\ t C_ X /\ ( x i^i ran F ) C_ t ) ) -> t e. L ) |
57 |
5 24 25 55 56
|
syl13anc |
|- ( ( ( ph /\ x e. L ) /\ ( ( F " ( `' F " x ) ) C_ t /\ t C_ X ) ) -> t e. L ) |
58 |
57
|
exp32 |
|- ( ( ph /\ x e. L ) -> ( ( F " ( `' F " x ) ) C_ t -> ( t C_ X -> t e. L ) ) ) |
59 |
|
imaeq2 |
|- ( s = ( `' F " x ) -> ( F " s ) = ( F " ( `' F " x ) ) ) |
60 |
59
|
sseq1d |
|- ( s = ( `' F " x ) -> ( ( F " s ) C_ t <-> ( F " ( `' F " x ) ) C_ t ) ) |
61 |
60
|
imbi1d |
|- ( s = ( `' F " x ) -> ( ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) <-> ( ( F " ( `' F " x ) ) C_ t -> ( t C_ X -> t e. L ) ) ) ) |
62 |
58 61
|
syl5ibrcom |
|- ( ( ph /\ x e. L ) -> ( s = ( `' F " x ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) ) |
63 |
62
|
rexlimdva |
|- ( ph -> ( E. x e. L s = ( `' F " x ) -> ( ( F " s ) C_ t -> ( t C_ X -> t e. L ) ) ) ) |