Step | Hyp | Ref
| Expression |
1 | | dvcnvre.d |
. . . . . 6
β’ (π β dom (β D πΉ) = π) |
2 | | dvbsss 25289 |
. . . . . 6
β’ dom
(β D πΉ) β
β |
3 | 1, 2 | eqsstrrdi 4003 |
. . . . 5
β’ (π β π β β) |
4 | | dvcnvre.c |
. . . . 5
β’ (π β πΆ β π) |
5 | 3, 4 | sseldd 3949 |
. . . 4
β’ (π β πΆ β β) |
6 | | dvcnvre.r |
. . . . 5
β’ (π β π
β
β+) |
7 | 6 | rpred 12965 |
. . . 4
β’ (π β π
β β) |
8 | 5, 7 | resubcld 11591 |
. . 3
β’ (π β (πΆ β π
) β β) |
9 | 5, 7 | readdcld 11192 |
. . 3
β’ (π β (πΆ + π
) β β) |
10 | 5, 6 | ltsubrpd 12997 |
. . . . 5
β’ (π β (πΆ β π
) < πΆ) |
11 | 5, 6 | ltaddrpd 12998 |
. . . . 5
β’ (π β πΆ < (πΆ + π
)) |
12 | 8, 5, 9, 10, 11 | lttrd 11324 |
. . . 4
β’ (π β (πΆ β π
) < (πΆ + π
)) |
13 | 8, 9, 12 | ltled 11311 |
. . 3
β’ (π β (πΆ β π
) β€ (πΆ + π
)) |
14 | | dvcnvre.s |
. . . 4
β’ (π β ((πΆ β π
)[,](πΆ + π
)) β π) |
15 | | dvcnvre.f |
. . . 4
β’ (π β πΉ β (πβcnββ)) |
16 | | rescncf 24283 |
. . . 4
β’ (((πΆ β π
)[,](πΆ + π
)) β π β (πΉ β (πβcnββ) β (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) β (((πΆ β π
)[,](πΆ + π
))βcnββ))) |
17 | 14, 15, 16 | sylc 65 |
. . 3
β’ (π β (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) β (((πΆ β π
)[,](πΆ + π
))βcnββ)) |
18 | 8, 9, 13, 17 | evthicc2 24847 |
. 2
β’ (π β βπ₯ β β βπ¦ β β ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦)) |
19 | | cncff 24279 |
. . . . . . . . 9
β’ (πΉ β (πβcnββ) β πΉ:πβΆβ) |
20 | 15, 19 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:πβΆβ) |
21 | 20, 4 | ffvelcdmd 7040 |
. . . . . . 7
β’ (π β (πΉβπΆ) β β) |
22 | 21 | adantr 482 |
. . . . . 6
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΉβπΆ) β β) |
23 | 8 | rexrd 11213 |
. . . . . . . . . . . 12
β’ (π β (πΆ β π
) β
β*) |
24 | 9 | rexrd 11213 |
. . . . . . . . . . . 12
β’ (π β (πΆ + π
) β
β*) |
25 | | lbicc2 13390 |
. . . . . . . . . . . 12
β’ (((πΆ β π
) β β* β§ (πΆ + π
) β β* β§ (πΆ β π
) β€ (πΆ + π
)) β (πΆ β π
) β ((πΆ β π
)[,](πΆ + π
))) |
26 | 23, 24, 13, 25 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (πΆ β π
) β ((πΆ β π
)[,](πΆ + π
))) |
27 | 26 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΆ β π
) β ((πΆ β π
)[,](πΆ + π
))) |
28 | 8, 5, 10 | ltled 11311 |
. . . . . . . . . . . 12
β’ (π β (πΆ β π
) β€ πΆ) |
29 | 5, 9, 11 | ltled 11311 |
. . . . . . . . . . . 12
β’ (π β πΆ β€ (πΆ + π
)) |
30 | | elicc2 13338 |
. . . . . . . . . . . . 13
β’ (((πΆ β π
) β β β§ (πΆ + π
) β β) β (πΆ β ((πΆ β π
)[,](πΆ + π
)) β (πΆ β β β§ (πΆ β π
) β€ πΆ β§ πΆ β€ (πΆ + π
)))) |
31 | 8, 9, 30 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (πΆ β ((πΆ β π
)[,](πΆ + π
)) β (πΆ β β β§ (πΆ β π
) β€ πΆ β§ πΆ β€ (πΆ + π
)))) |
32 | 5, 28, 29, 31 | mpbir3and 1343 |
. . . . . . . . . . 11
β’ (π β πΆ β ((πΆ β π
)[,](πΆ + π
))) |
33 | 32 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β πΆ β ((πΆ β π
)[,](πΆ + π
))) |
34 | 10 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΆ β π
) < πΆ) |
35 | | isorel 7275 |
. . . . . . . . . . . . 13
β’ (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β§ ((πΆ β π
) β ((πΆ β π
)[,](πΆ + π
)) β§ πΆ β ((πΆ β π
)[,](πΆ + π
)))) β ((πΆ β π
) < πΆ β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
)) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ))) |
36 | 35 | biimpd 228 |
. . . . . . . . . . . 12
β’ (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β§ ((πΆ β π
) β ((πΆ β π
)[,](πΆ + π
)) β§ πΆ β ((πΆ β π
)[,](πΆ + π
)))) β ((πΆ β π
) < πΆ β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
)) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ))) |
37 | 36 | exp32 422 |
. . . . . . . . . . 11
β’ ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β ((πΆ β π
) β ((πΆ β π
)[,](πΆ + π
)) β (πΆ β ((πΆ β π
)[,](πΆ + π
)) β ((πΆ β π
) < πΆ β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
)) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ))))) |
38 | 37 | com4l 92 |
. . . . . . . . . 10
β’ ((πΆ β π
) β ((πΆ β π
)[,](πΆ + π
)) β (πΆ β ((πΆ β π
)[,](πΆ + π
)) β ((πΆ β π
) < πΆ β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
)) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ))))) |
39 | 27, 33, 34, 38 | syl3c 66 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
)) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ))) |
40 | 27 | fvresd 6866 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
)) = (πΉβ(πΆ β π
))) |
41 | 33 | fvresd 6866 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ) = (πΉβπΆ)) |
42 | 40, 41 | breq12d 5122 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
)) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ) β (πΉβ(πΆ β π
)) < (πΉβπΆ))) |
43 | 39, 42 | sylibd 238 |
. . . . . . . 8
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β (πΉβ(πΆ β π
)) < (πΉβπΆ))) |
44 | 20 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β πΉ:πβΆβ) |
45 | 44 | ffund 6676 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β Fun πΉ) |
46 | 14 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΆ β π
)[,](πΆ + π
)) β π) |
47 | 44 | fdmd 6683 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β dom πΉ = π) |
48 | 46, 47 | sseqtrrd 3989 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΆ β π
)[,](πΆ + π
)) β dom πΉ) |
49 | | funfvima2 7185 |
. . . . . . . . . . . . . 14
β’ ((Fun
πΉ β§ ((πΆ β π
)[,](πΆ + π
)) β dom πΉ) β ((πΆ β π
) β ((πΆ β π
)[,](πΆ + π
)) β (πΉβ(πΆ β π
)) β (πΉ β ((πΆ β π
)[,](πΆ + π
))))) |
50 | 45, 48, 49 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΆ β π
) β ((πΆ β π
)[,](πΆ + π
)) β (πΉβ(πΆ β π
)) β (πΉ β ((πΆ β π
)[,](πΆ + π
))))) |
51 | 27, 50 | mpd 15 |
. . . . . . . . . . . 12
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΉβ(πΆ β π
)) β (πΉ β ((πΆ β π
)[,](πΆ + π
)))) |
52 | | df-ima 5650 |
. . . . . . . . . . . . 13
β’ (πΉ β ((πΆ β π
)[,](πΆ + π
))) = ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) |
53 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦)) |
54 | 52, 53 | eqtrid 2785 |
. . . . . . . . . . . 12
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΉ β ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦)) |
55 | 51, 54 | eleqtrd 2836 |
. . . . . . . . . . 11
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΉβ(πΆ β π
)) β (π₯[,]π¦)) |
56 | | elicc2 13338 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π¦ β β) β ((πΉβ(πΆ β π
)) β (π₯[,]π¦) β ((πΉβ(πΆ β π
)) β β β§ π₯ β€ (πΉβ(πΆ β π
)) β§ (πΉβ(πΆ β π
)) β€ π¦))) |
57 | 56 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉβ(πΆ β π
)) β (π₯[,]π¦) β ((πΉβ(πΆ β π
)) β β β§ π₯ β€ (πΉβ(πΆ β π
)) β§ (πΉβ(πΆ β π
)) β€ π¦))) |
58 | 55, 57 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉβ(πΆ β π
)) β β β§ π₯ β€ (πΉβ(πΆ β π
)) β§ (πΉβ(πΆ β π
)) β€ π¦)) |
59 | 58 | simp2d 1144 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β π₯ β€ (πΉβ(πΆ β π
))) |
60 | | simprll 778 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β π₯ β β) |
61 | 14, 26 | sseldd 3949 |
. . . . . . . . . . . 12
β’ (π β (πΆ β π
) β π) |
62 | 20, 61 | ffvelcdmd 7040 |
. . . . . . . . . . 11
β’ (π β (πΉβ(πΆ β π
)) β β) |
63 | 62 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΉβ(πΆ β π
)) β β) |
64 | | lelttr 11253 |
. . . . . . . . . 10
β’ ((π₯ β β β§ (πΉβ(πΆ β π
)) β β β§ (πΉβπΆ) β β) β ((π₯ β€ (πΉβ(πΆ β π
)) β§ (πΉβ(πΆ β π
)) < (πΉβπΆ)) β π₯ < (πΉβπΆ))) |
65 | 60, 63, 22, 64 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((π₯ β€ (πΉβ(πΆ β π
)) β§ (πΉβ(πΆ β π
)) < (πΉβπΆ)) β π₯ < (πΉβπΆ))) |
66 | 59, 65 | mpand 694 |
. . . . . . . 8
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉβ(πΆ β π
)) < (πΉβπΆ) β π₯ < (πΉβπΆ))) |
67 | 43, 66 | syld 47 |
. . . . . . 7
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β π₯ < (πΉβπΆ))) |
68 | | ubicc2 13391 |
. . . . . . . . . . . 12
β’ (((πΆ β π
) β β* β§ (πΆ + π
) β β* β§ (πΆ β π
) β€ (πΆ + π
)) β (πΆ + π
) β ((πΆ β π
)[,](πΆ + π
))) |
69 | 23, 24, 13, 68 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (πΆ + π
) β ((πΆ β π
)[,](πΆ + π
))) |
70 | 69 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΆ + π
) β ((πΆ β π
)[,](πΆ + π
))) |
71 | 11 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β πΆ < (πΆ + π
)) |
72 | | isorel 7275 |
. . . . . . . . . . . . 13
β’ (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β§ (πΆ β ((πΆ β π
)[,](πΆ + π
)) β§ (πΆ + π
) β ((πΆ β π
)[,](πΆ + π
)))) β (πΆ < (πΆ + π
) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ)β‘
< ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)))) |
73 | 72 | biimpd 228 |
. . . . . . . . . . . 12
β’ (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β§ (πΆ β ((πΆ β π
)[,](πΆ + π
)) β§ (πΆ + π
) β ((πΆ β π
)[,](πΆ + π
)))) β (πΆ < (πΆ + π
) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ)β‘
< ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)))) |
74 | 73 | exp32 422 |
. . . . . . . . . . 11
β’ ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β (πΆ β ((πΆ β π
)[,](πΆ + π
)) β ((πΆ + π
) β ((πΆ β π
)[,](πΆ + π
)) β (πΆ < (πΆ + π
) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ)β‘
< ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)))))) |
75 | 74 | com4l 92 |
. . . . . . . . . 10
β’ (πΆ β ((πΆ β π
)[,](πΆ + π
)) β ((πΆ + π
) β ((πΆ β π
)[,](πΆ + π
)) β (πΆ < (πΆ + π
) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ)β‘
< ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)))))) |
76 | 33, 70, 71, 75 | syl3c 66 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ)β‘
< ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)))) |
77 | | fvex 6859 |
. . . . . . . . . . 11
β’ ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ) β V |
78 | | fvex 6859 |
. . . . . . . . . . 11
β’ ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)) β V |
79 | 77, 78 | brcnv 5842 |
. . . . . . . . . 10
β’ (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ)β‘
< ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ)) |
80 | 70 | fvresd 6866 |
. . . . . . . . . . 11
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)) = (πΉβ(πΆ + π
))) |
81 | 80, 41 | breq12d 5122 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ) β (πΉβ(πΆ + π
)) < (πΉβπΆ))) |
82 | 79, 81 | bitrid 283 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ)β‘
< ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)) β (πΉβ(πΆ + π
)) < (πΉβπΆ))) |
83 | 76, 82 | sylibd 238 |
. . . . . . . 8
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β (πΉβ(πΆ + π
)) < (πΉβπΆ))) |
84 | | funfvima2 7185 |
. . . . . . . . . . . . . 14
β’ ((Fun
πΉ β§ ((πΆ β π
)[,](πΆ + π
)) β dom πΉ) β ((πΆ + π
) β ((πΆ β π
)[,](πΆ + π
)) β (πΉβ(πΆ + π
)) β (πΉ β ((πΆ β π
)[,](πΆ + π
))))) |
85 | 45, 48, 84 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΆ + π
) β ((πΆ β π
)[,](πΆ + π
)) β (πΉβ(πΆ + π
)) β (πΉ β ((πΆ β π
)[,](πΆ + π
))))) |
86 | 70, 85 | mpd 15 |
. . . . . . . . . . . 12
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΉβ(πΆ + π
)) β (πΉ β ((πΆ β π
)[,](πΆ + π
)))) |
87 | 86, 54 | eleqtrd 2836 |
. . . . . . . . . . 11
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΉβ(πΆ + π
)) β (π₯[,]π¦)) |
88 | | elicc2 13338 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π¦ β β) β ((πΉβ(πΆ + π
)) β (π₯[,]π¦) β ((πΉβ(πΆ + π
)) β β β§ π₯ β€ (πΉβ(πΆ + π
)) β§ (πΉβ(πΆ + π
)) β€ π¦))) |
89 | 88 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉβ(πΆ + π
)) β (π₯[,]π¦) β ((πΉβ(πΆ + π
)) β β β§ π₯ β€ (πΉβ(πΆ + π
)) β§ (πΉβ(πΆ + π
)) β€ π¦))) |
90 | 87, 89 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉβ(πΆ + π
)) β β β§ π₯ β€ (πΉβ(πΆ + π
)) β§ (πΉβ(πΆ + π
)) β€ π¦)) |
91 | 90 | simp2d 1144 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β π₯ β€ (πΉβ(πΆ + π
))) |
92 | 14, 69 | sseldd 3949 |
. . . . . . . . . . . 12
β’ (π β (πΆ + π
) β π) |
93 | 20, 92 | ffvelcdmd 7040 |
. . . . . . . . . . 11
β’ (π β (πΉβ(πΆ + π
)) β β) |
94 | 93 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΉβ(πΆ + π
)) β β) |
95 | | lelttr 11253 |
. . . . . . . . . 10
β’ ((π₯ β β β§ (πΉβ(πΆ + π
)) β β β§ (πΉβπΆ) β β) β ((π₯ β€ (πΉβ(πΆ + π
)) β§ (πΉβ(πΆ + π
)) < (πΉβπΆ)) β π₯ < (πΉβπΆ))) |
96 | 60, 94, 22, 95 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((π₯ β€ (πΉβ(πΆ + π
)) β§ (πΉβ(πΆ + π
)) < (πΉβπΆ)) β π₯ < (πΉβπΆ))) |
97 | 91, 96 | mpand 694 |
. . . . . . . 8
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉβ(πΆ + π
)) < (πΉβπΆ) β π₯ < (πΉβπΆ))) |
98 | 83, 97 | syld 47 |
. . . . . . 7
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β π₯ < (πΉβπΆ))) |
99 | | ax-resscn 11116 |
. . . . . . . . . . . . . 14
β’ β
β β |
100 | 99 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β β β
β) |
101 | | fss 6689 |
. . . . . . . . . . . . . 14
β’ ((πΉ:πβΆβ β§ β β
β) β πΉ:πβΆβ) |
102 | 20, 99, 101 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (π β πΉ:πβΆβ) |
103 | 14, 3 | sstrd 3958 |
. . . . . . . . . . . . 13
β’ (π β ((πΆ β π
)[,](πΆ + π
)) β β) |
104 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(TopOpenββfld) =
(TopOpenββfld) |
105 | 104 | tgioo2 24189 |
. . . . . . . . . . . . . 14
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
106 | 104, 105 | dvres 25298 |
. . . . . . . . . . . . 13
β’
(((β β β β§ πΉ:πβΆβ) β§ (π β β β§ ((πΆ β π
)[,](πΆ + π
)) β β)) β (β D
(πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) = ((β D πΉ) βΎ ((intβ(topGenβran
(,)))β((πΆ β
π
)[,](πΆ + π
))))) |
107 | 100, 102,
3, 103, 106 | syl22anc 838 |
. . . . . . . . . . . 12
β’ (π β (β D (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) = ((β D πΉ) βΎ ((intβ(topGenβran
(,)))β((πΆ β
π
)[,](πΆ + π
))))) |
108 | | iccntr 24207 |
. . . . . . . . . . . . . 14
β’ (((πΆ β π
) β β β§ (πΆ + π
) β β) β
((intβ(topGenβran (,)))β((πΆ β π
)[,](πΆ + π
))) = ((πΆ β π
)(,)(πΆ + π
))) |
109 | 8, 9, 108 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β
((intβ(topGenβran (,)))β((πΆ β π
)[,](πΆ + π
))) = ((πΆ β π
)(,)(πΆ + π
))) |
110 | 109 | reseq2d 5941 |
. . . . . . . . . . . 12
β’ (π β ((β D πΉ) βΎ
((intβ(topGenβran (,)))β((πΆ β π
)[,](πΆ + π
)))) = ((β D πΉ) βΎ ((πΆ β π
)(,)(πΆ + π
)))) |
111 | 107, 110 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π β (β D (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) = ((β D πΉ) βΎ ((πΆ β π
)(,)(πΆ + π
)))) |
112 | 111 | dmeqd 5865 |
. . . . . . . . . 10
β’ (π β dom (β D (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) = dom ((β D πΉ) βΎ ((πΆ β π
)(,)(πΆ + π
)))) |
113 | | dmres 5963 |
. . . . . . . . . . 11
β’ dom
((β D πΉ) βΎ
((πΆ β π
)(,)(πΆ + π
))) = (((πΆ β π
)(,)(πΆ + π
)) β© dom (β D πΉ)) |
114 | | ioossicc 13359 |
. . . . . . . . . . . . . 14
β’ ((πΆ β π
)(,)(πΆ + π
)) β ((πΆ β π
)[,](πΆ + π
)) |
115 | 114, 14 | sstrid 3959 |
. . . . . . . . . . . . 13
β’ (π β ((πΆ β π
)(,)(πΆ + π
)) β π) |
116 | 115, 1 | sseqtrrd 3989 |
. . . . . . . . . . . 12
β’ (π β ((πΆ β π
)(,)(πΆ + π
)) β dom (β D πΉ)) |
117 | | df-ss 3931 |
. . . . . . . . . . . 12
β’ (((πΆ β π
)(,)(πΆ + π
)) β dom (β D πΉ) β (((πΆ β π
)(,)(πΆ + π
)) β© dom (β D πΉ)) = ((πΆ β π
)(,)(πΆ + π
))) |
118 | 116, 117 | sylib 217 |
. . . . . . . . . . 11
β’ (π β (((πΆ β π
)(,)(πΆ + π
)) β© dom (β D πΉ)) = ((πΆ β π
)(,)(πΆ + π
))) |
119 | 113, 118 | eqtrid 2785 |
. . . . . . . . . 10
β’ (π β dom ((β D πΉ) βΎ ((πΆ β π
)(,)(πΆ + π
))) = ((πΆ β π
)(,)(πΆ + π
))) |
120 | 112, 119 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β dom (β D (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) = ((πΆ β π
)(,)(πΆ + π
))) |
121 | | resss 5966 |
. . . . . . . . . . . 12
β’ ((β
D πΉ) βΎ ((πΆ β π
)(,)(πΆ + π
))) β (β D πΉ) |
122 | 111, 121 | eqsstrdi 4002 |
. . . . . . . . . . 11
β’ (π β (β D (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β (β D πΉ)) |
123 | | rnss 5898 |
. . . . . . . . . . 11
β’ ((β
D (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β (β D πΉ) β ran (β D (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β ran (β D πΉ)) |
124 | 122, 123 | syl 17 |
. . . . . . . . . 10
β’ (π β ran (β D (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β ran (β D πΉ)) |
125 | | dvcnvre.z |
. . . . . . . . . 10
β’ (π β Β¬ 0 β ran
(β D πΉ)) |
126 | 124, 125 | ssneldd 3951 |
. . . . . . . . 9
β’ (π β Β¬ 0 β ran
(β D (πΉ βΎ
((πΆ β π
)[,](πΆ + π
))))) |
127 | 8, 9, 17, 120, 126 | dvne0 25398 |
. . . . . . . 8
β’ (π β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β¨ (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))))) |
128 | 127 | adantr 482 |
. . . . . . 7
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β¨ (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))))) |
129 | 67, 98, 128 | mpjaod 859 |
. . . . . 6
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β π₯ < (πΉβπΆ)) |
130 | | isorel 7275 |
. . . . . . . . . . . . 13
β’ (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β§ (πΆ β ((πΆ β π
)[,](πΆ + π
)) β§ (πΆ + π
) β ((πΆ β π
)[,](πΆ + π
)))) β (πΆ < (πΆ + π
) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)))) |
131 | 130 | biimpd 228 |
. . . . . . . . . . . 12
β’ (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β§ (πΆ β ((πΆ β π
)[,](πΆ + π
)) β§ (πΆ + π
) β ((πΆ β π
)[,](πΆ + π
)))) β (πΆ < (πΆ + π
) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)))) |
132 | 131 | exp32 422 |
. . . . . . . . . . 11
β’ ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β (πΆ β ((πΆ β π
)[,](πΆ + π
)) β ((πΆ + π
) β ((πΆ β π
)[,](πΆ + π
)) β (πΆ < (πΆ + π
) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)))))) |
133 | 132 | com4l 92 |
. . . . . . . . . 10
β’ (πΆ β ((πΆ β π
)[,](πΆ + π
)) β ((πΆ + π
) β ((πΆ β π
)[,](πΆ + π
)) β (πΆ < (πΆ + π
) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)))))) |
134 | 33, 70, 71, 133 | syl3c 66 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)))) |
135 | 41, 80 | breq12d 5122 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ + π
)) β (πΉβπΆ) < (πΉβ(πΆ + π
)))) |
136 | 134, 135 | sylibd 238 |
. . . . . . . 8
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β (πΉβπΆ) < (πΉβ(πΆ + π
)))) |
137 | 90 | simp3d 1145 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΉβ(πΆ + π
)) β€ π¦) |
138 | | simprlr 779 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β π¦ β β) |
139 | | ltletr 11255 |
. . . . . . . . . 10
β’ (((πΉβπΆ) β β β§ (πΉβ(πΆ + π
)) β β β§ π¦ β β) β (((πΉβπΆ) < (πΉβ(πΆ + π
)) β§ (πΉβ(πΆ + π
)) β€ π¦) β (πΉβπΆ) < π¦)) |
140 | 22, 94, 138, 139 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (((πΉβπΆ) < (πΉβ(πΆ + π
)) β§ (πΉβ(πΆ + π
)) β€ π¦) β (πΉβπΆ) < π¦)) |
141 | 137, 140 | mpan2d 693 |
. . . . . . . 8
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉβπΆ) < (πΉβ(πΆ + π
)) β (πΉβπΆ) < π¦)) |
142 | 136, 141 | syld 47 |
. . . . . . 7
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β (πΉβπΆ) < π¦)) |
143 | | isorel 7275 |
. . . . . . . . . . . . 13
β’ (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β§ ((πΆ β π
) β ((πΆ β π
)[,](πΆ + π
)) β§ πΆ β ((πΆ β π
)[,](πΆ + π
)))) β ((πΆ β π
) < πΆ β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
))β‘
< ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ))) |
144 | 143 | biimpd 228 |
. . . . . . . . . . . 12
β’ (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β§ ((πΆ β π
) β ((πΆ β π
)[,](πΆ + π
)) β§ πΆ β ((πΆ β π
)[,](πΆ + π
)))) β ((πΆ β π
) < πΆ β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
))β‘
< ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ))) |
145 | 144 | exp32 422 |
. . . . . . . . . . 11
β’ ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β ((πΆ β π
) β ((πΆ β π
)[,](πΆ + π
)) β (πΆ β ((πΆ β π
)[,](πΆ + π
)) β ((πΆ β π
) < πΆ β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
))β‘
< ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ))))) |
146 | 145 | com4l 92 |
. . . . . . . . . 10
β’ ((πΆ β π
) β ((πΆ β π
)[,](πΆ + π
)) β (πΆ β ((πΆ β π
)[,](πΆ + π
)) β ((πΆ β π
) < πΆ β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
))β‘
< ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ))))) |
147 | 27, 33, 34, 146 | syl3c 66 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
))β‘
< ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ))) |
148 | | fvex 6859 |
. . . . . . . . . . 11
β’ ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
)) β V |
149 | 148, 77 | brcnv 5842 |
. . . . . . . . . 10
β’ (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
))β‘
< ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
))) |
150 | 41, 40 | breq12d 5122 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ) < ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
)) β (πΉβπΆ) < (πΉβ(πΆ β π
)))) |
151 | 149, 150 | bitrid 283 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))β(πΆ β π
))β‘
< ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))βπΆ) β (πΉβπΆ) < (πΉβ(πΆ β π
)))) |
152 | 147, 151 | sylibd 238 |
. . . . . . . 8
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β (πΉβπΆ) < (πΉβ(πΆ β π
)))) |
153 | 58 | simp3d 1145 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΉβ(πΆ β π
)) β€ π¦) |
154 | | ltletr 11255 |
. . . . . . . . . 10
β’ (((πΉβπΆ) β β β§ (πΉβ(πΆ β π
)) β β β§ π¦ β β) β (((πΉβπΆ) < (πΉβ(πΆ β π
)) β§ (πΉβ(πΆ β π
)) β€ π¦) β (πΉβπΆ) < π¦)) |
155 | 22, 63, 138, 154 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (((πΉβπΆ) < (πΉβ(πΆ β π
)) β§ (πΉβ(πΆ β π
)) β€ π¦) β (πΉβπΆ) < π¦)) |
156 | 153, 155 | mpan2d 693 |
. . . . . . . 8
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉβπΆ) < (πΉβ(πΆ β π
)) β (πΉβπΆ) < π¦)) |
157 | 152, 156 | syld 47 |
. . . . . . 7
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) Isom < , β‘ < (((πΆ β π
)[,](πΆ + π
)), ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
)))) β (πΉβπΆ) < π¦)) |
158 | 142, 157,
128 | mpjaod 859 |
. . . . . 6
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΉβπΆ) < π¦) |
159 | 60 | rexrd 11213 |
. . . . . . 7
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β π₯ β β*) |
160 | 138 | rexrd 11213 |
. . . . . . 7
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β π¦ β β*) |
161 | | elioo2 13314 |
. . . . . . 7
β’ ((π₯ β β*
β§ π¦ β
β*) β ((πΉβπΆ) β (π₯(,)π¦) β ((πΉβπΆ) β β β§ π₯ < (πΉβπΆ) β§ (πΉβπΆ) < π¦))) |
162 | 159, 160,
161 | syl2anc 585 |
. . . . . 6
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((πΉβπΆ) β (π₯(,)π¦) β ((πΉβπΆ) β β β§ π₯ < (πΉβπΆ) β§ (πΉβπΆ) < π¦))) |
163 | 22, 129, 158, 162 | mpbir3and 1343 |
. . . . 5
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΉβπΆ) β (π₯(,)π¦)) |
164 | 54 | fveq2d 6850 |
. . . . . 6
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((intβ(topGenβran
(,)))β(πΉ β
((πΆ β π
)[,](πΆ + π
)))) = ((intβ(topGenβran
(,)))β(π₯[,]π¦))) |
165 | | iccntr 24207 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β
((intβ(topGenβran (,)))β(π₯[,]π¦)) = (π₯(,)π¦)) |
166 | 165 | ad2antrl 727 |
. . . . . 6
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((intβ(topGenβran
(,)))β(π₯[,]π¦)) = (π₯(,)π¦)) |
167 | 164, 166 | eqtrd 2773 |
. . . . 5
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β ((intβ(topGenβran
(,)))β(πΉ β
((πΆ β π
)[,](πΆ + π
)))) = (π₯(,)π¦)) |
168 | 163, 167 | eleqtrrd 2837 |
. . . 4
β’ ((π β§ ((π₯ β β β§ π¦ β β) β§ ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦))) β (πΉβπΆ) β ((intβ(topGenβran
(,)))β(πΉ β
((πΆ β π
)[,](πΆ + π
))))) |
169 | 168 | expr 458 |
. . 3
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦) β (πΉβπΆ) β ((intβ(topGenβran
(,)))β(πΉ β
((πΆ β π
)[,](πΆ + π
)))))) |
170 | 169 | rexlimdvva 3202 |
. 2
β’ (π β (βπ₯ β β βπ¦ β β ran (πΉ βΎ ((πΆ β π
)[,](πΆ + π
))) = (π₯[,]π¦) β (πΉβπΆ) β ((intβ(topGenβran
(,)))β(πΉ β
((πΆ β π
)[,](πΆ + π
)))))) |
171 | 18, 170 | mpd 15 |
1
β’ (π β (πΉβπΆ) β ((intβ(topGenβran
(,)))β(πΉ β
((πΆ β π
)[,](πΆ + π
))))) |