Step | Hyp | Ref
| Expression |
1 | | rge0ssre 13380 |
. . 3
β’
(0[,)+β) β β |
2 | | fss 6690 |
. . 3
β’ ((πΉ:ββΆ(0[,)+β)
β§ (0[,)+β) β β) β πΉ:ββΆβ) |
3 | 1, 2 | mpan2 690 |
. 2
β’ (πΉ:ββΆ(0[,)+β)
β πΉ:ββΆβ) |
4 | | ffvelcdm 7037 |
. . . . 5
β’ ((πΉ:ββΆβ β§
π₯ β β) β
(πΉβπ₯) β β) |
5 | | elrege0 13378 |
. . . . . 6
β’ ((πΉβπ₯) β (0[,)+β) β ((πΉβπ₯) β β β§ 0 β€ (πΉβπ₯))) |
6 | 5 | baib 537 |
. . . . 5
β’ ((πΉβπ₯) β β β ((πΉβπ₯) β (0[,)+β) β 0 β€ (πΉβπ₯))) |
7 | 4, 6 | syl 17 |
. . . 4
β’ ((πΉ:ββΆβ β§
π₯ β β) β
((πΉβπ₯) β (0[,)+β) β 0
β€ (πΉβπ₯))) |
8 | 7 | ralbidva 3173 |
. . 3
β’ (πΉ:ββΆβ β
(βπ₯ β β
(πΉβπ₯) β (0[,)+β) β βπ₯ β β 0 β€ (πΉβπ₯))) |
9 | | ffn 6673 |
. . . 4
β’ (πΉ:ββΆβ β
πΉ Fn
β) |
10 | | ffnfv 7071 |
. . . . 5
β’ (πΉ:ββΆ(0[,)+β)
β (πΉ Fn β β§
βπ₯ β β
(πΉβπ₯) β (0[,)+β))) |
11 | 10 | baib 537 |
. . . 4
β’ (πΉ Fn β β (πΉ:ββΆ(0[,)+β)
β βπ₯ β
β (πΉβπ₯) β
(0[,)+β))) |
12 | 9, 11 | syl 17 |
. . 3
β’ (πΉ:ββΆβ β
(πΉ:ββΆ(0[,)+β) β
βπ₯ β β
(πΉβπ₯) β (0[,)+β))) |
13 | | 0cn 11154 |
. . . . . . 7
β’ 0 β
β |
14 | | fnconstg 6735 |
. . . . . . 7
β’ (0 β
β β (β Γ {0}) Fn β) |
15 | 13, 14 | ax-mp 5 |
. . . . . 6
β’ (β
Γ {0}) Fn β |
16 | | df-0p 25050 |
. . . . . . 7
β’
0π = (β Γ {0}) |
17 | 16 | fneq1i 6604 |
. . . . . 6
β’
(0π Fn β β (β Γ {0}) Fn
β) |
18 | 15, 17 | mpbir 230 |
. . . . 5
β’
0π Fn β |
19 | 18 | a1i 11 |
. . . 4
β’ (πΉ:ββΆβ β
0π Fn β) |
20 | | cnex 11139 |
. . . . 5
β’ β
β V |
21 | 20 | a1i 11 |
. . . 4
β’ (πΉ:ββΆβ β
β β V) |
22 | | reex 11149 |
. . . . 5
β’ β
β V |
23 | 22 | a1i 11 |
. . . 4
β’ (πΉ:ββΆβ β
β β V) |
24 | | ax-resscn 11115 |
. . . . 5
β’ β
β β |
25 | | sseqin2 4180 |
. . . . 5
β’ (β
β β β (β β© β) = β) |
26 | 24, 25 | mpbi 229 |
. . . 4
β’ (β
β© β) = β |
27 | | 0pval 25051 |
. . . . 5
β’ (π₯ β β β
(0πβπ₯) = 0) |
28 | 27 | adantl 483 |
. . . 4
β’ ((πΉ:ββΆβ β§
π₯ β β) β
(0πβπ₯) = 0) |
29 | | eqidd 2738 |
. . . 4
β’ ((πΉ:ββΆβ β§
π₯ β β) β
(πΉβπ₯) = (πΉβπ₯)) |
30 | 19, 9, 21, 23, 26, 28, 29 | ofrfval 7632 |
. . 3
β’ (πΉ:ββΆβ β
(0π βr β€ πΉ β βπ₯ β β 0 β€ (πΉβπ₯))) |
31 | 8, 12, 30 | 3bitr4d 311 |
. 2
β’ (πΉ:ββΆβ β
(πΉ:ββΆ(0[,)+β) β
0π βr β€ πΉ)) |
32 | 3, 31 | biadanii 821 |
1
β’ (πΉ:ββΆ(0[,)+β)
β (πΉ:ββΆβ β§
0π βr β€ πΉ)) |