Step | Hyp | Ref
| Expression |
1 | | ffn 6664 |
. . 3
β’ (πΉ:ββΆβ β
πΉ Fn
β) |
2 | 1 | adantr 482 |
. 2
β’ ((πΉ:ββΆβ β§
0π βr β€ πΉ) β πΉ Fn β) |
3 | | ax-resscn 11042 |
. . . . . 6
β’ β
β β |
4 | 3 | a1i 11 |
. . . . 5
β’ (πΉ:ββΆβ β
β β β) |
5 | 4, 1 | 0pledm 24959 |
. . . 4
β’ (πΉ:ββΆβ β
(0π βr β€ πΉ β (β Γ {0})
βr β€ πΉ)) |
6 | | 0re 11091 |
. . . . . 6
β’ 0 β
β |
7 | | fnconstg 6726 |
. . . . . 6
β’ (0 β
β β (β Γ {0}) Fn β) |
8 | 6, 7 | mp1i 13 |
. . . . 5
β’ (πΉ:ββΆβ β
(β Γ {0}) Fn β) |
9 | | reex 11076 |
. . . . . 6
β’ β
β V |
10 | 9 | a1i 11 |
. . . . 5
β’ (πΉ:ββΆβ β
β β V) |
11 | | inidm 4177 |
. . . . 5
β’ (β
β© β) = β |
12 | | c0ex 11083 |
. . . . . . 7
β’ 0 β
V |
13 | 12 | fvconst2 7148 |
. . . . . 6
β’ (π₯ β β β ((β
Γ {0})βπ₯) =
0) |
14 | 13 | adantl 483 |
. . . . 5
β’ ((πΉ:ββΆβ β§
π₯ β β) β
((β Γ {0})βπ₯) = 0) |
15 | | eqidd 2739 |
. . . . 5
β’ ((πΉ:ββΆβ β§
π₯ β β) β
(πΉβπ₯) = (πΉβπ₯)) |
16 | 8, 1, 10, 10, 11, 14, 15 | ofrfval 7618 |
. . . 4
β’ (πΉ:ββΆβ β
((β Γ {0}) βr β€ πΉ β βπ₯ β β 0 β€ (πΉβπ₯))) |
17 | | ffvelcdm 7028 |
. . . . . . . 8
β’ ((πΉ:ββΆβ β§
π₯ β β) β
(πΉβπ₯) β β) |
18 | 17 | rexrd 11139 |
. . . . . . 7
β’ ((πΉ:ββΆβ β§
π₯ β β) β
(πΉβπ₯) β
β*) |
19 | 18 | biantrurd 534 |
. . . . . 6
β’ ((πΉ:ββΆβ β§
π₯ β β) β (0
β€ (πΉβπ₯) β ((πΉβπ₯) β β* β§ 0 β€
(πΉβπ₯)))) |
20 | | elxrge0 13303 |
. . . . . 6
β’ ((πΉβπ₯) β (0[,]+β) β ((πΉβπ₯) β β* β§ 0 β€
(πΉβπ₯))) |
21 | 19, 20 | bitr4di 289 |
. . . . 5
β’ ((πΉ:ββΆβ β§
π₯ β β) β (0
β€ (πΉβπ₯) β (πΉβπ₯) β (0[,]+β))) |
22 | 21 | ralbidva 3171 |
. . . 4
β’ (πΉ:ββΆβ β
(βπ₯ β β 0
β€ (πΉβπ₯) β βπ₯ β β (πΉβπ₯) β (0[,]+β))) |
23 | 5, 16, 22 | 3bitrd 305 |
. . 3
β’ (πΉ:ββΆβ β
(0π βr β€ πΉ β βπ₯ β β (πΉβπ₯) β (0[,]+β))) |
24 | 23 | biimpa 478 |
. 2
β’ ((πΉ:ββΆβ β§
0π βr β€ πΉ) β βπ₯ β β (πΉβπ₯) β (0[,]+β)) |
25 | | ffnfv 7061 |
. 2
β’ (πΉ:ββΆ(0[,]+β)
β (πΉ Fn β β§
βπ₯ β β
(πΉβπ₯) β (0[,]+β))) |
26 | 2, 24, 25 | sylanbrc 584 |
1
β’ ((πΉ:ββΆβ β§
0π βr β€ πΉ) β πΉ:ββΆ(0[,]+β)) |