Step |
Hyp |
Ref |
Expression |
1 |
|
smfco.s |
|- ( ph -> S e. SAlg ) |
2 |
|
smfco.f |
|- ( ph -> F e. ( SMblFn ` S ) ) |
3 |
|
smfco.j |
|- J = ( topGen ` ran (,) ) |
4 |
|
smfco.b |
|- B = ( SalGen ` J ) |
5 |
|
smfco.h |
|- ( ph -> H e. ( SMblFn ` B ) ) |
6 |
|
nfv |
|- F/ a ph |
7 |
|
cnvimass |
|- ( `' F " dom H ) C_ dom F |
8 |
7
|
a1i |
|- ( ph -> ( `' F " dom H ) C_ dom F ) |
9 |
|
eqid |
|- dom F = dom F |
10 |
1 2 9
|
smfdmss |
|- ( ph -> dom F C_ U. S ) |
11 |
8 10
|
sstrd |
|- ( ph -> ( `' F " dom H ) C_ U. S ) |
12 |
|
retop |
|- ( topGen ` ran (,) ) e. Top |
13 |
3 12
|
eqeltri |
|- J e. Top |
14 |
13
|
a1i |
|- ( ph -> J e. Top ) |
15 |
14 4
|
salgencld |
|- ( ph -> B e. SAlg ) |
16 |
|
eqid |
|- dom H = dom H |
17 |
15 5 16
|
smff |
|- ( ph -> H : dom H --> RR ) |
18 |
17
|
ffund |
|- ( ph -> Fun H ) |
19 |
1 2 9
|
smff |
|- ( ph -> F : dom F --> RR ) |
20 |
19
|
ffund |
|- ( ph -> Fun F ) |
21 |
18 20
|
fco3 |
|- ( ph -> ( H o. F ) : ( `' F " dom H ) --> ran H ) |
22 |
17
|
frnd |
|- ( ph -> ran H C_ RR ) |
23 |
21 22
|
fssd |
|- ( ph -> ( H o. F ) : ( `' F " dom H ) --> RR ) |
24 |
23
|
adantr |
|- ( ( ph /\ a e. RR ) -> ( H o. F ) : ( `' F " dom H ) --> RR ) |
25 |
|
rexr |
|- ( a e. RR -> a e. RR* ) |
26 |
25
|
adantl |
|- ( ( ph /\ a e. RR ) -> a e. RR* ) |
27 |
24 26
|
preimaioomnf |
|- ( ( ph /\ a e. RR ) -> ( `' ( H o. F ) " ( -oo (,) a ) ) = { x e. ( `' F " dom H ) | ( ( H o. F ) ` x ) < a } ) |
28 |
27
|
eqcomd |
|- ( ( ph /\ a e. RR ) -> { x e. ( `' F " dom H ) | ( ( H o. F ) ` x ) < a } = ( `' ( H o. F ) " ( -oo (,) a ) ) ) |
29 |
|
cnvco |
|- `' ( H o. F ) = ( `' F o. `' H ) |
30 |
29
|
imaeq1i |
|- ( `' ( H o. F ) " ( -oo (,) a ) ) = ( ( `' F o. `' H ) " ( -oo (,) a ) ) |
31 |
30
|
a1i |
|- ( ( ph /\ a e. RR ) -> ( `' ( H o. F ) " ( -oo (,) a ) ) = ( ( `' F o. `' H ) " ( -oo (,) a ) ) ) |
32 |
|
imaco |
|- ( ( `' F o. `' H ) " ( -oo (,) a ) ) = ( `' F " ( `' H " ( -oo (,) a ) ) ) |
33 |
32
|
a1i |
|- ( ( ph /\ a e. RR ) -> ( ( `' F o. `' H ) " ( -oo (,) a ) ) = ( `' F " ( `' H " ( -oo (,) a ) ) ) ) |
34 |
28 31 33
|
3eqtrd |
|- ( ( ph /\ a e. RR ) -> { x e. ( `' F " dom H ) | ( ( H o. F ) ` x ) < a } = ( `' F " ( `' H " ( -oo (,) a ) ) ) ) |
35 |
17
|
adantr |
|- ( ( ph /\ a e. RR ) -> H : dom H --> RR ) |
36 |
35 26
|
preimaioomnf |
|- ( ( ph /\ a e. RR ) -> ( `' H " ( -oo (,) a ) ) = { x e. dom H | ( H ` x ) < a } ) |
37 |
36
|
eqcomd |
|- ( ( ph /\ a e. RR ) -> { x e. dom H | ( H ` x ) < a } = ( `' H " ( -oo (,) a ) ) ) |
38 |
37
|
eqcomd |
|- ( ( ph /\ a e. RR ) -> ( `' H " ( -oo (,) a ) ) = { x e. dom H | ( H ` x ) < a } ) |
39 |
15
|
adantr |
|- ( ( ph /\ a e. RR ) -> B e. SAlg ) |
40 |
5
|
adantr |
|- ( ( ph /\ a e. RR ) -> H e. ( SMblFn ` B ) ) |
41 |
|
simpr |
|- ( ( ph /\ a e. RR ) -> a e. RR ) |
42 |
39 40 16 41
|
smfpreimalt |
|- ( ( ph /\ a e. RR ) -> { x e. dom H | ( H ` x ) < a } e. ( B |`t dom H ) ) |
43 |
38 42
|
eqeltrd |
|- ( ( ph /\ a e. RR ) -> ( `' H " ( -oo (,) a ) ) e. ( B |`t dom H ) ) |
44 |
15
|
elexd |
|- ( ph -> B e. _V ) |
45 |
5
|
dmexd |
|- ( ph -> dom H e. _V ) |
46 |
|
elrest |
|- ( ( B e. _V /\ dom H e. _V ) -> ( ( `' H " ( -oo (,) a ) ) e. ( B |`t dom H ) <-> E. e e. B ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) ) |
47 |
44 45 46
|
syl2anc |
|- ( ph -> ( ( `' H " ( -oo (,) a ) ) e. ( B |`t dom H ) <-> E. e e. B ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) ) |
48 |
47
|
adantr |
|- ( ( ph /\ a e. RR ) -> ( ( `' H " ( -oo (,) a ) ) e. ( B |`t dom H ) <-> E. e e. B ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) ) |
49 |
43 48
|
mpbid |
|- ( ( ph /\ a e. RR ) -> E. e e. B ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) |
50 |
|
imaeq2 |
|- ( ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) = ( `' F " ( e i^i dom H ) ) ) |
51 |
50
|
3ad2ant3 |
|- ( ( ph /\ e e. B /\ ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) = ( `' F " ( e i^i dom H ) ) ) |
52 |
|
ovexd |
|- ( ( ph /\ e e. B ) -> ( S |`t dom F ) e. _V ) |
53 |
2
|
elexd |
|- ( ph -> F e. _V ) |
54 |
|
cnvexg |
|- ( F e. _V -> `' F e. _V ) |
55 |
53 54
|
syl |
|- ( ph -> `' F e. _V ) |
56 |
|
imaexg |
|- ( `' F e. _V -> ( `' F " dom H ) e. _V ) |
57 |
55 56
|
syl |
|- ( ph -> ( `' F " dom H ) e. _V ) |
58 |
57
|
adantr |
|- ( ( ph /\ e e. B ) -> ( `' F " dom H ) e. _V ) |
59 |
1
|
adantr |
|- ( ( ph /\ e e. B ) -> S e. SAlg ) |
60 |
2
|
adantr |
|- ( ( ph /\ e e. B ) -> F e. ( SMblFn ` S ) ) |
61 |
|
simpr |
|- ( ( ph /\ e e. B ) -> e e. B ) |
62 |
|
eqid |
|- ( `' F " e ) = ( `' F " e ) |
63 |
59 60 9 3 4 61 62
|
smfpimbor1 |
|- ( ( ph /\ e e. B ) -> ( `' F " e ) e. ( S |`t dom F ) ) |
64 |
|
eqid |
|- ( ( `' F " e ) i^i ( `' F " dom H ) ) = ( ( `' F " e ) i^i ( `' F " dom H ) ) |
65 |
52 58 63 64
|
elrestd |
|- ( ( ph /\ e e. B ) -> ( ( `' F " e ) i^i ( `' F " dom H ) ) e. ( ( S |`t dom F ) |`t ( `' F " dom H ) ) ) |
66 |
|
inpreima |
|- ( Fun F -> ( `' F " ( e i^i dom H ) ) = ( ( `' F " e ) i^i ( `' F " dom H ) ) ) |
67 |
20 66
|
syl |
|- ( ph -> ( `' F " ( e i^i dom H ) ) = ( ( `' F " e ) i^i ( `' F " dom H ) ) ) |
68 |
67
|
adantr |
|- ( ( ph /\ e e. B ) -> ( `' F " ( e i^i dom H ) ) = ( ( `' F " e ) i^i ( `' F " dom H ) ) ) |
69 |
2
|
dmexd |
|- ( ph -> dom F e. _V ) |
70 |
|
restabs |
|- ( ( S e. SAlg /\ ( `' F " dom H ) C_ dom F /\ dom F e. _V ) -> ( ( S |`t dom F ) |`t ( `' F " dom H ) ) = ( S |`t ( `' F " dom H ) ) ) |
71 |
1 8 69 70
|
syl3anc |
|- ( ph -> ( ( S |`t dom F ) |`t ( `' F " dom H ) ) = ( S |`t ( `' F " dom H ) ) ) |
72 |
71
|
eqcomd |
|- ( ph -> ( S |`t ( `' F " dom H ) ) = ( ( S |`t dom F ) |`t ( `' F " dom H ) ) ) |
73 |
72
|
adantr |
|- ( ( ph /\ e e. B ) -> ( S |`t ( `' F " dom H ) ) = ( ( S |`t dom F ) |`t ( `' F " dom H ) ) ) |
74 |
68 73
|
eleq12d |
|- ( ( ph /\ e e. B ) -> ( ( `' F " ( e i^i dom H ) ) e. ( S |`t ( `' F " dom H ) ) <-> ( ( `' F " e ) i^i ( `' F " dom H ) ) e. ( ( S |`t dom F ) |`t ( `' F " dom H ) ) ) ) |
75 |
65 74
|
mpbird |
|- ( ( ph /\ e e. B ) -> ( `' F " ( e i^i dom H ) ) e. ( S |`t ( `' F " dom H ) ) ) |
76 |
75
|
3adant3 |
|- ( ( ph /\ e e. B /\ ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) -> ( `' F " ( e i^i dom H ) ) e. ( S |`t ( `' F " dom H ) ) ) |
77 |
51 76
|
eqeltrd |
|- ( ( ph /\ e e. B /\ ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) e. ( S |`t ( `' F " dom H ) ) ) |
78 |
77
|
3exp |
|- ( ph -> ( e e. B -> ( ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) e. ( S |`t ( `' F " dom H ) ) ) ) ) |
79 |
78
|
adantr |
|- ( ( ph /\ a e. RR ) -> ( e e. B -> ( ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) e. ( S |`t ( `' F " dom H ) ) ) ) ) |
80 |
79
|
rexlimdv |
|- ( ( ph /\ a e. RR ) -> ( E. e e. B ( `' H " ( -oo (,) a ) ) = ( e i^i dom H ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) e. ( S |`t ( `' F " dom H ) ) ) ) |
81 |
49 80
|
mpd |
|- ( ( ph /\ a e. RR ) -> ( `' F " ( `' H " ( -oo (,) a ) ) ) e. ( S |`t ( `' F " dom H ) ) ) |
82 |
34 81
|
eqeltrd |
|- ( ( ph /\ a e. RR ) -> { x e. ( `' F " dom H ) | ( ( H o. F ) ` x ) < a } e. ( S |`t ( `' F " dom H ) ) ) |
83 |
6 1 11 23 82
|
issmfd |
|- ( ph -> ( H o. F ) e. ( SMblFn ` S ) ) |