Step |
Hyp |
Ref |
Expression |
1 |
|
smf2id.j |
|- J = ( topGen ` ran (,) ) |
2 |
|
smf2id.b |
|- B = ( SalGen ` J ) |
3 |
|
smf2id.a |
|- ( ph -> A C_ RR ) |
4 |
|
nfv |
|- F/ x ph |
5 |
|
retop |
|- ( topGen ` ran (,) ) e. Top |
6 |
1 5
|
eqeltri |
|- J e. Top |
7 |
6
|
a1i |
|- ( ph -> J e. Top ) |
8 |
7 2
|
salgencld |
|- ( ph -> B e. SAlg ) |
9 |
|
reex |
|- RR e. _V |
10 |
9
|
a1i |
|- ( ph -> RR e. _V ) |
11 |
10 3
|
ssexd |
|- ( ph -> A e. _V ) |
12 |
3
|
adantr |
|- ( ( ph /\ x e. A ) -> A C_ RR ) |
13 |
|
simpr |
|- ( ( ph /\ x e. A ) -> x e. A ) |
14 |
12 13
|
sseldd |
|- ( ( ph /\ x e. A ) -> x e. RR ) |
15 |
|
2re |
|- 2 e. RR |
16 |
15
|
a1i |
|- ( ph -> 2 e. RR ) |
17 |
1 2 3
|
smfid |
|- ( ph -> ( x e. A |-> x ) e. ( SMblFn ` B ) ) |
18 |
4 8 11 14 16 17
|
smfmulc1 |
|- ( ph -> ( x e. A |-> ( 2 x. x ) ) e. ( SMblFn ` B ) ) |