Step | Hyp | Ref
| Expression |
1 | | forn 6764 |
. . . 4
β’ (πΉ:ββontoββ β ran πΉ = β) |
2 | 1 | difeq2d 4087 |
. . 3
β’ (πΉ:ββontoββ β (β β ran πΉ) = (β β
β)) |
3 | | difid 4335 |
. . 3
β’ (β
β β) = β
|
4 | 2, 3 | eqtrdi 2793 |
. 2
β’ (πΉ:ββontoββ β (β β ran πΉ) = β
) |
5 | | reex 11149 |
. . . . . 6
β’ β
β V |
6 | 5, 5 | xpex 7692 |
. . . . 5
β’ (β
Γ β) β V |
7 | 6, 5 | mpoex 8017 |
. . . 4
β’ (π₯ β (β Γ
β), π¦ β β
β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©)) β
V |
8 | 7 | isseti 3463 |
. . 3
β’
βπ π = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©)) |
9 | | fof 6761 |
. . . . . . . 8
β’ (πΉ:ββontoββ β πΉ:ββΆβ) |
10 | 9 | adantr 482 |
. . . . . . 7
β’ ((πΉ:ββontoββ β§ π = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) β πΉ:ββΆβ) |
11 | | simpr 486 |
. . . . . . 7
β’ ((πΉ:ββontoββ β§ π = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) β π = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) |
12 | | eqid 2737 |
. . . . . . 7
β’
({β¨0, β¨0, 1β©β©} βͺ πΉ) = ({β¨0, β¨0, 1β©β©} βͺ
πΉ) |
13 | | eqid 2737 |
. . . . . . 7
β’
seq0(π, ({β¨0,
β¨0, 1β©β©} βͺ πΉ)) = seq0(π, ({β¨0, β¨0, 1β©β©} βͺ
πΉ)) |
14 | | eqid 2737 |
. . . . . . 7
β’ sup(ran
(1st β seq0(π, ({β¨0, β¨0, 1β©β©} βͺ
πΉ))), β, < ) =
sup(ran (1st β seq0(π, ({β¨0, β¨0, 1β©β©} βͺ
πΉ))), β, <
) |
15 | 10, 11, 12, 13, 14 | ruclem12 16130 |
. . . . . 6
β’ ((πΉ:ββontoββ β§ π = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) β sup(ran
(1st β seq0(π, ({β¨0, β¨0, 1β©β©} βͺ
πΉ))), β, < )
β (β β ran πΉ)) |
16 | | n0i 4298 |
. . . . . 6
β’ (sup(ran
(1st β seq0(π, ({β¨0, β¨0, 1β©β©} βͺ
πΉ))), β, < )
β (β β ran πΉ) β Β¬ (β β ran πΉ) = β
) |
17 | 15, 16 | syl 17 |
. . . . 5
β’ ((πΉ:ββontoββ β§ π = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) β Β¬ (β
β ran πΉ) =
β
) |
18 | 17 | ex 414 |
. . . 4
β’ (πΉ:ββontoββ β (π = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©)) β Β¬ (β
β ran πΉ) =
β
)) |
19 | 18 | exlimdv 1937 |
. . 3
β’ (πΉ:ββontoββ β (βπ π = (π₯ β (β Γ β), π¦ β β β¦
β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©)) β Β¬ (β
β ran πΉ) =
β
)) |
20 | 8, 19 | mpi 20 |
. 2
β’ (πΉ:ββontoββ β Β¬ (β β ran
πΉ) =
β
) |
21 | 4, 20 | pm2.65i 193 |
1
β’ Β¬
πΉ:ββontoββ |