Step | Hyp | Ref
| Expression |
1 | | vitali.3 |
. . . 4
β’ (π β πΉ Fn π) |
2 | | vitali.4 |
. . . . 5
β’ (π β βπ§ β π (π§ β β
β (πΉβπ§) β π§)) |
3 | | vitali.2 |
. . . . . . . . 9
β’ π = ((0[,]1) / βΌ
) |
4 | | neeq1 3007 |
. . . . . . . . 9
β’ ([π£] βΌ = π§ β ([π£] βΌ β β
β
π§ β
β
)) |
5 | | vitali.1 |
. . . . . . . . . . . . . 14
β’ βΌ =
{β¨π₯, π¦β© β£ ((π₯ β (0[,]1) β§ π¦ β (0[,]1)) β§ (π₯ β π¦) β β)} |
6 | 5 | vitalilem1 24988 |
. . . . . . . . . . . . 13
β’ βΌ Er
(0[,]1) |
7 | | erdm 8665 |
. . . . . . . . . . . . 13
β’ ( βΌ Er
(0[,]1) β dom βΌ =
(0[,]1)) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . . 12
β’ dom βΌ =
(0[,]1) |
9 | 8 | eleq2i 2830 |
. . . . . . . . . . 11
β’ (π£ β dom βΌ β π£ β
(0[,]1)) |
10 | | ecdmn0 8702 |
. . . . . . . . . . 11
β’ (π£ β dom βΌ β [π£] βΌ β
β
) |
11 | 9, 10 | bitr3i 277 |
. . . . . . . . . 10
β’ (π£ β (0[,]1) β [π£] βΌ β
β
) |
12 | 11 | biimpi 215 |
. . . . . . . . 9
β’ (π£ β (0[,]1) β [π£] βΌ β
β
) |
13 | 3, 4, 12 | ectocl 8731 |
. . . . . . . 8
β’ (π§ β π β π§ β β
) |
14 | 13 | adantl 483 |
. . . . . . 7
β’ ((π β§ π§ β π) β π§ β β
) |
15 | | sseq1 3974 |
. . . . . . . . . 10
β’ ([π€] βΌ = π§ β ([π€] βΌ β (0[,]1)
β π§ β
(0[,]1))) |
16 | 6 | a1i 11 |
. . . . . . . . . . 11
β’ (π€ β (0[,]1) β βΌ Er
(0[,]1)) |
17 | 16 | ecss 8701 |
. . . . . . . . . 10
β’ (π€ β (0[,]1) β [π€] βΌ β
(0[,]1)) |
18 | 3, 15, 17 | ectocl 8731 |
. . . . . . . . 9
β’ (π§ β π β π§ β (0[,]1)) |
19 | 18 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π§ β π) β π§ β (0[,]1)) |
20 | 19 | sseld 3948 |
. . . . . . 7
β’ ((π β§ π§ β π) β ((πΉβπ§) β π§ β (πΉβπ§) β (0[,]1))) |
21 | 14, 20 | embantd 59 |
. . . . . 6
β’ ((π β§ π§ β π) β ((π§ β β
β (πΉβπ§) β π§) β (πΉβπ§) β (0[,]1))) |
22 | 21 | ralimdva 3165 |
. . . . 5
β’ (π β (βπ§ β π (π§ β β
β (πΉβπ§) β π§) β βπ§ β π (πΉβπ§) β (0[,]1))) |
23 | 2, 22 | mpd 15 |
. . . 4
β’ (π β βπ§ β π (πΉβπ§) β (0[,]1)) |
24 | | ffnfv 7071 |
. . . 4
β’ (πΉ:πβΆ(0[,]1) β (πΉ Fn π β§ βπ§ β π (πΉβπ§) β (0[,]1))) |
25 | 1, 23, 24 | sylanbrc 584 |
. . 3
β’ (π β πΉ:πβΆ(0[,]1)) |
26 | 25 | frnd 6681 |
. 2
β’ (π β ran πΉ β (0[,]1)) |
27 | | vitali.5 |
. . . . . . . 8
β’ (π β πΊ:ββ1-1-ontoβ(β β© (-1[,]1))) |
28 | 27 | adantr 482 |
. . . . . . 7
β’ ((π β§ π£ β (0[,]1)) β πΊ:ββ1-1-ontoβ(β β© (-1[,]1))) |
29 | | f1ocnv 6801 |
. . . . . . 7
β’ (πΊ:ββ1-1-ontoβ(β β© (-1[,]1)) β β‘πΊ:(β β© (-1[,]1))β1-1-ontoββ) |
30 | | f1of 6789 |
. . . . . . 7
β’ (β‘πΊ:(β β© (-1[,]1))β1-1-ontoββ β β‘πΊ:(β β©
(-1[,]1))βΆβ) |
31 | 28, 29, 30 | 3syl 18 |
. . . . . 6
β’ ((π β§ π£ β (0[,]1)) β β‘πΊ:(β β©
(-1[,]1))βΆβ) |
32 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π£ β (0[,]1)) β π£ β (0[,]1)) |
33 | 32, 11 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π£ β (0[,]1)) β [π£] βΌ β
β
) |
34 | | neeq1 3007 |
. . . . . . . . . . . 12
β’ (π§ = [π£] βΌ β (π§ β β
β [π£] βΌ β
β
)) |
35 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π§ = [π£] βΌ β (πΉβπ§) = (πΉβ[π£] βΌ )) |
36 | | id 22 |
. . . . . . . . . . . . 13
β’ (π§ = [π£] βΌ β π§ = [π£] βΌ ) |
37 | 35, 36 | eleq12d 2832 |
. . . . . . . . . . . 12
β’ (π§ = [π£] βΌ β ((πΉβπ§) β π§ β (πΉβ[π£] βΌ ) β [π£] βΌ )) |
38 | 34, 37 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π§ = [π£] βΌ β ((π§ β β
β (πΉβπ§) β π§) β ([π£] βΌ β β
β
(πΉβ[π£] βΌ ) β [π£] βΌ
))) |
39 | 2 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π£ β (0[,]1)) β βπ§ β π (π§ β β
β (πΉβπ§) β π§)) |
40 | | ovex 7395 |
. . . . . . . . . . . . . . 15
β’ (0[,]1)
β V |
41 | | erex 8679 |
. . . . . . . . . . . . . . 15
β’ ( βΌ Er
(0[,]1) β ((0[,]1) β V β βΌ β
V)) |
42 | 6, 40, 41 | mp2 9 |
. . . . . . . . . . . . . 14
β’ βΌ β
V |
43 | 42 | ecelqsi 8719 |
. . . . . . . . . . . . 13
β’ (π£ β (0[,]1) β [π£] βΌ β ((0[,]1)
/ βΌ )) |
44 | 43 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π£ β (0[,]1)) β [π£] βΌ β ((0[,]1)
/ βΌ )) |
45 | 44, 3 | eleqtrrdi 2849 |
. . . . . . . . . . 11
β’ ((π β§ π£ β (0[,]1)) β [π£] βΌ β π) |
46 | 38, 39, 45 | rspcdva 3585 |
. . . . . . . . . 10
β’ ((π β§ π£ β (0[,]1)) β ([π£] βΌ β β
β
(πΉβ[π£] βΌ ) β [π£] βΌ )) |
47 | 33, 46 | mpd 15 |
. . . . . . . . 9
β’ ((π β§ π£ β (0[,]1)) β (πΉβ[π£] βΌ ) β [π£] βΌ ) |
48 | | fvex 6860 |
. . . . . . . . . . 11
β’ (πΉβ[π£] βΌ ) β
V |
49 | | vex 3452 |
. . . . . . . . . . 11
β’ π£ β V |
50 | 48, 49 | elec 8699 |
. . . . . . . . . 10
β’ ((πΉβ[π£] βΌ ) β [π£] βΌ β π£ βΌ (πΉβ[π£] βΌ )) |
51 | | oveq12 7371 |
. . . . . . . . . . . 12
β’ ((π₯ = π£ β§ π¦ = (πΉβ[π£] βΌ )) β (π₯ β π¦) = (π£ β (πΉβ[π£] βΌ
))) |
52 | 51 | eleq1d 2823 |
. . . . . . . . . . 11
β’ ((π₯ = π£ β§ π¦ = (πΉβ[π£] βΌ )) β ((π₯ β π¦) β β β (π£ β (πΉβ[π£] βΌ )) β
β)) |
53 | 52, 5 | brab2a 5730 |
. . . . . . . . . 10
β’ (π£ βΌ (πΉβ[π£] βΌ ) β ((π£ β (0[,]1) β§ (πΉβ[π£] βΌ ) β (0[,]1))
β§ (π£ β (πΉβ[π£] βΌ )) β
β)) |
54 | 50, 53 | bitri 275 |
. . . . . . . . 9
β’ ((πΉβ[π£] βΌ ) β [π£] βΌ β ((π£ β (0[,]1) β§ (πΉβ[π£] βΌ ) β (0[,]1))
β§ (π£ β (πΉβ[π£] βΌ )) β
β)) |
55 | 47, 54 | sylib 217 |
. . . . . . . 8
β’ ((π β§ π£ β (0[,]1)) β ((π£ β (0[,]1) β§ (πΉβ[π£] βΌ ) β (0[,]1))
β§ (π£ β (πΉβ[π£] βΌ )) β
β)) |
56 | 55 | simprd 497 |
. . . . . . 7
β’ ((π β§ π£ β (0[,]1)) β (π£ β (πΉβ[π£] βΌ )) β
β) |
57 | | elicc01 13390 |
. . . . . . . . . . 11
β’ (π£ β (0[,]1) β (π£ β β β§ 0 β€
π£ β§ π£ β€ 1)) |
58 | 32, 57 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π£ β (0[,]1)) β (π£ β β β§ 0 β€ π£ β§ π£ β€ 1)) |
59 | 58 | simp1d 1143 |
. . . . . . . . 9
β’ ((π β§ π£ β (0[,]1)) β π£ β β) |
60 | 55 | simpld 496 |
. . . . . . . . . . . 12
β’ ((π β§ π£ β (0[,]1)) β (π£ β (0[,]1) β§ (πΉβ[π£] βΌ ) β
(0[,]1))) |
61 | 60 | simprd 497 |
. . . . . . . . . . 11
β’ ((π β§ π£ β (0[,]1)) β (πΉβ[π£] βΌ ) β
(0[,]1)) |
62 | | elicc01 13390 |
. . . . . . . . . . 11
β’ ((πΉβ[π£] βΌ ) β (0[,]1)
β ((πΉβ[π£] βΌ ) β β
β§ 0 β€ (πΉβ[π£] βΌ ) β§ (πΉβ[π£] βΌ ) β€
1)) |
63 | 61, 62 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π£ β (0[,]1)) β ((πΉβ[π£] βΌ ) β β
β§ 0 β€ (πΉβ[π£] βΌ ) β§ (πΉβ[π£] βΌ ) β€
1)) |
64 | 63 | simp1d 1143 |
. . . . . . . . 9
β’ ((π β§ π£ β (0[,]1)) β (πΉβ[π£] βΌ ) β
β) |
65 | 59, 64 | resubcld 11590 |
. . . . . . . 8
β’ ((π β§ π£ β (0[,]1)) β (π£ β (πΉβ[π£] βΌ )) β
β) |
66 | 64, 59 | resubcld 11590 |
. . . . . . . . . . 11
β’ ((π β§ π£ β (0[,]1)) β ((πΉβ[π£] βΌ ) β π£) β
β) |
67 | | 1red 11163 |
. . . . . . . . . . 11
β’ ((π β§ π£ β (0[,]1)) β 1 β
β) |
68 | 58 | simp2d 1144 |
. . . . . . . . . . . 12
β’ ((π β§ π£ β (0[,]1)) β 0 β€ π£) |
69 | 64, 59 | subge02d 11754 |
. . . . . . . . . . . 12
β’ ((π β§ π£ β (0[,]1)) β (0 β€ π£ β ((πΉβ[π£] βΌ ) β π£) β€ (πΉβ[π£] βΌ
))) |
70 | 68, 69 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ π£ β (0[,]1)) β ((πΉβ[π£] βΌ ) β π£) β€ (πΉβ[π£] βΌ )) |
71 | 63 | simp3d 1145 |
. . . . . . . . . . 11
β’ ((π β§ π£ β (0[,]1)) β (πΉβ[π£] βΌ ) β€
1) |
72 | 66, 64, 67, 70, 71 | letrd 11319 |
. . . . . . . . . 10
β’ ((π β§ π£ β (0[,]1)) β ((πΉβ[π£] βΌ ) β π£) β€ 1) |
73 | 66, 67 | lenegd 11741 |
. . . . . . . . . 10
β’ ((π β§ π£ β (0[,]1)) β (((πΉβ[π£] βΌ ) β π£) β€ 1 β -1 β€ -((πΉβ[π£] βΌ ) β π£))) |
74 | 72, 73 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ π£ β (0[,]1)) β -1 β€ -((πΉβ[π£] βΌ ) β π£)) |
75 | 64 | recnd 11190 |
. . . . . . . . . 10
β’ ((π β§ π£ β (0[,]1)) β (πΉβ[π£] βΌ ) β
β) |
76 | 59 | recnd 11190 |
. . . . . . . . . 10
β’ ((π β§ π£ β (0[,]1)) β π£ β β) |
77 | 75, 76 | negsubdi2d 11535 |
. . . . . . . . 9
β’ ((π β§ π£ β (0[,]1)) β -((πΉβ[π£] βΌ ) β π£) = (π£ β (πΉβ[π£] βΌ
))) |
78 | 74, 77 | breqtrd 5136 |
. . . . . . . 8
β’ ((π β§ π£ β (0[,]1)) β -1 β€ (π£ β (πΉβ[π£] βΌ
))) |
79 | 63 | simp2d 1144 |
. . . . . . . . . 10
β’ ((π β§ π£ β (0[,]1)) β 0 β€ (πΉβ[π£] βΌ )) |
80 | 59, 64 | subge02d 11754 |
. . . . . . . . . 10
β’ ((π β§ π£ β (0[,]1)) β (0 β€ (πΉβ[π£] βΌ ) β (π£ β (πΉβ[π£] βΌ )) β€ π£)) |
81 | 79, 80 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ π£ β (0[,]1)) β (π£ β (πΉβ[π£] βΌ )) β€ π£) |
82 | 58 | simp3d 1145 |
. . . . . . . . 9
β’ ((π β§ π£ β (0[,]1)) β π£ β€ 1) |
83 | 65, 59, 67, 81, 82 | letrd 11319 |
. . . . . . . 8
β’ ((π β§ π£ β (0[,]1)) β (π£ β (πΉβ[π£] βΌ )) β€
1) |
84 | | neg1rr 12275 |
. . . . . . . . 9
β’ -1 β
β |
85 | | 1re 11162 |
. . . . . . . . 9
β’ 1 β
β |
86 | 84, 85 | elicc2i 13337 |
. . . . . . . 8
β’ ((π£ β (πΉβ[π£] βΌ )) β (-1[,]1)
β ((π£ β (πΉβ[π£] βΌ )) β β
β§ -1 β€ (π£ β
(πΉβ[π£] βΌ )) β§ (π£ β (πΉβ[π£] βΌ )) β€
1)) |
87 | 65, 78, 83, 86 | syl3anbrc 1344 |
. . . . . . 7
β’ ((π β§ π£ β (0[,]1)) β (π£ β (πΉβ[π£] βΌ )) β
(-1[,]1)) |
88 | 56, 87 | elind 4159 |
. . . . . 6
β’ ((π β§ π£ β (0[,]1)) β (π£ β (πΉβ[π£] βΌ )) β (β
β© (-1[,]1))) |
89 | 31, 88 | ffvelcdmd 7041 |
. . . . 5
β’ ((π β§ π£ β (0[,]1)) β (β‘πΊβ(π£ β (πΉβ[π£] βΌ ))) β
β) |
90 | | oveq1 7369 |
. . . . . . . 8
β’ (π = π£ β (π β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ ))))) = (π£ β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ
)))))) |
91 | 90 | eleq1d 2823 |
. . . . . . 7
β’ (π = π£ β ((π β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ ))))) β ran
πΉ β (π£ β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ ))))) β ran
πΉ)) |
92 | | f1ocnvfv2 7228 |
. . . . . . . . . . 11
β’ ((πΊ:ββ1-1-ontoβ(β β© (-1[,]1)) β§ (π£ β (πΉβ[π£] βΌ )) β (β
β© (-1[,]1))) β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ )))) = (π£ β (πΉβ[π£] βΌ
))) |
93 | 27, 88, 92 | syl2an2r 684 |
. . . . . . . . . 10
β’ ((π β§ π£ β (0[,]1)) β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ )))) = (π£ β (πΉβ[π£] βΌ
))) |
94 | 93 | oveq2d 7378 |
. . . . . . . . 9
β’ ((π β§ π£ β (0[,]1)) β (π£ β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ ))))) = (π£ β (π£ β (πΉβ[π£] βΌ
)))) |
95 | 76, 75 | nncand 11524 |
. . . . . . . . 9
β’ ((π β§ π£ β (0[,]1)) β (π£ β (π£ β (πΉβ[π£] βΌ ))) = (πΉβ[π£] βΌ )) |
96 | 94, 95 | eqtrd 2777 |
. . . . . . . 8
β’ ((π β§ π£ β (0[,]1)) β (π£ β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ ))))) = (πΉβ[π£] βΌ )) |
97 | | fnfvelrn 7036 |
. . . . . . . . 9
β’ ((πΉ Fn π β§ [π£] βΌ β π) β (πΉβ[π£] βΌ ) β ran πΉ) |
98 | 1, 45, 97 | syl2an2r 684 |
. . . . . . . 8
β’ ((π β§ π£ β (0[,]1)) β (πΉβ[π£] βΌ ) β ran πΉ) |
99 | 96, 98 | eqeltrd 2838 |
. . . . . . 7
β’ ((π β§ π£ β (0[,]1)) β (π£ β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ ))))) β ran
πΉ) |
100 | 91, 59, 99 | elrabd 3652 |
. . . . . 6
β’ ((π β§ π£ β (0[,]1)) β π£ β {π β β β£ (π β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ ))))) β ran
πΉ}) |
101 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = (β‘πΊβ(π£ β (πΉβ[π£] βΌ ))) β (πΊβπ) = (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ
))))) |
102 | 101 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = (β‘πΊβ(π£ β (πΉβ[π£] βΌ ))) β (π β (πΊβπ)) = (π β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ
)))))) |
103 | 102 | eleq1d 2823 |
. . . . . . . . 9
β’ (π = (β‘πΊβ(π£ β (πΉβ[π£] βΌ ))) β ((π β (πΊβπ)) β ran πΉ β (π β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ ))))) β ran
πΉ)) |
104 | 103 | rabbidv 3418 |
. . . . . . . 8
β’ (π = (β‘πΊβ(π£ β (πΉβ[π£] βΌ ))) β {π β β β£ (π β (πΊβπ)) β ran πΉ} = {π β β β£ (π β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ ))))) β ran
πΉ}) |
105 | | vitali.6 |
. . . . . . . 8
β’ π = (π β β β¦ {π β β β£ (π β (πΊβπ)) β ran πΉ}) |
106 | | reex 11149 |
. . . . . . . . 9
β’ β
β V |
107 | 106 | rabex 5294 |
. . . . . . . 8
β’ {π β β β£ (π β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ ))))) β ran
πΉ} β
V |
108 | 104, 105,
107 | fvmpt 6953 |
. . . . . . 7
β’ ((β‘πΊβ(π£ β (πΉβ[π£] βΌ ))) β β
β (πβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ )))) = {π β β β£ (π β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ ))))) β ran
πΉ}) |
109 | 89, 108 | syl 17 |
. . . . . 6
β’ ((π β§ π£ β (0[,]1)) β (πβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ )))) = {π β β β£ (π β (πΊβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ ))))) β ran
πΉ}) |
110 | 100, 109 | eleqtrrd 2841 |
. . . . 5
β’ ((π β§ π£ β (0[,]1)) β π£ β (πβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ
))))) |
111 | | fveq2 6847 |
. . . . . 6
β’ (π = (β‘πΊβ(π£ β (πΉβ[π£] βΌ ))) β (πβπ) = (πβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ
))))) |
112 | 111 | eliuni 4965 |
. . . . 5
β’ (((β‘πΊβ(π£ β (πΉβ[π£] βΌ ))) β β
β§ π£ β (πβ(β‘πΊβ(π£ β (πΉβ[π£] βΌ ))))) β π£ β βͺ π β β (πβπ)) |
113 | 89, 110, 112 | syl2anc 585 |
. . . 4
β’ ((π β§ π£ β (0[,]1)) β π£ β βͺ
π β β (πβπ)) |
114 | 113 | ex 414 |
. . 3
β’ (π β (π£ β (0[,]1) β π£ β βͺ
π β β (πβπ))) |
115 | 114 | ssrdv 3955 |
. 2
β’ (π β (0[,]1) β βͺ π β β (πβπ)) |
116 | | eliun 4963 |
. . . 4
β’ (π₯ β βͺ π β β (πβπ) β βπ β β π₯ β (πβπ)) |
117 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΊβπ) = (πΊβπ)) |
118 | 117 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β (πΊβπ)) = (π β (πΊβπ))) |
119 | 118 | eleq1d 2823 |
. . . . . . . . . . . . 13
β’ (π = π β ((π β (πΊβπ)) β ran πΉ β (π β (πΊβπ)) β ran πΉ)) |
120 | 119 | rabbidv 3418 |
. . . . . . . . . . . 12
β’ (π = π β {π β β β£ (π β (πΊβπ)) β ran πΉ} = {π β β β£ (π β (πΊβπ)) β ran πΉ}) |
121 | 106 | rabex 5294 |
. . . . . . . . . . . 12
β’ {π β β β£ (π β (πΊβπ)) β ran πΉ} β V |
122 | 120, 105,
121 | fvmpt 6953 |
. . . . . . . . . . 11
β’ (π β β β (πβπ) = {π β β β£ (π β (πΊβπ)) β ran πΉ}) |
123 | 122 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβπ) = {π β β β£ (π β (πΊβπ)) β ran πΉ}) |
124 | 123 | eleq2d 2824 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π₯ β (πβπ) β π₯ β {π β β β£ (π β (πΊβπ)) β ran πΉ})) |
125 | 124 | biimpa 478 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β π₯ β {π β β β£ (π β (πΊβπ)) β ran πΉ}) |
126 | | oveq1 7369 |
. . . . . . . . . 10
β’ (π = π₯ β (π β (πΊβπ)) = (π₯ β (πΊβπ))) |
127 | 126 | eleq1d 2823 |
. . . . . . . . 9
β’ (π = π₯ β ((π β (πΊβπ)) β ran πΉ β (π₯ β (πΊβπ)) β ran πΉ)) |
128 | 127 | elrab 3650 |
. . . . . . . 8
β’ (π₯ β {π β β β£ (π β (πΊβπ)) β ran πΉ} β (π₯ β β β§ (π₯ β (πΊβπ)) β ran πΉ)) |
129 | 125, 128 | sylib 217 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β (π₯ β β β§ (π₯ β (πΊβπ)) β ran πΉ)) |
130 | 129 | simpld 496 |
. . . . . 6
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β π₯ β β) |
131 | 84 | a1i 11 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β -1 β β) |
132 | | iccssre 13353 |
. . . . . . . . . 10
β’ ((-1
β β β§ 1 β β) β (-1[,]1) β
β) |
133 | 84, 85, 132 | mp2an 691 |
. . . . . . . . 9
β’ (-1[,]1)
β β |
134 | | f1of 6789 |
. . . . . . . . . . . 12
β’ (πΊ:ββ1-1-ontoβ(β β© (-1[,]1)) β πΊ:ββΆ(β β©
(-1[,]1))) |
135 | 27, 134 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΊ:ββΆ(β β©
(-1[,]1))) |
136 | 135 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΊβπ) β (β β©
(-1[,]1))) |
137 | 136 | elin2d 4164 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΊβπ) β (-1[,]1)) |
138 | 133, 137 | sselid 3947 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΊβπ) β β) |
139 | 138 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β (πΊβπ) β β) |
140 | 137 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β (πΊβπ) β (-1[,]1)) |
141 | 84, 85 | elicc2i 13337 |
. . . . . . . . 9
β’ ((πΊβπ) β (-1[,]1) β ((πΊβπ) β β β§ -1 β€ (πΊβπ) β§ (πΊβπ) β€ 1)) |
142 | 140, 141 | sylib 217 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β ((πΊβπ) β β β§ -1 β€ (πΊβπ) β§ (πΊβπ) β€ 1)) |
143 | 142 | simp2d 1144 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β -1 β€ (πΊβπ)) |
144 | 26 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β ran πΉ β (0[,]1)) |
145 | 129 | simprd 497 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β (π₯ β (πΊβπ)) β ran πΉ) |
146 | 144, 145 | sseldd 3950 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β (π₯ β (πΊβπ)) β (0[,]1)) |
147 | | elicc01 13390 |
. . . . . . . . . 10
β’ ((π₯ β (πΊβπ)) β (0[,]1) β ((π₯ β (πΊβπ)) β β β§ 0 β€ (π₯ β (πΊβπ)) β§ (π₯ β (πΊβπ)) β€ 1)) |
148 | 146, 147 | sylib 217 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β ((π₯ β (πΊβπ)) β β β§ 0 β€ (π₯ β (πΊβπ)) β§ (π₯ β (πΊβπ)) β€ 1)) |
149 | 148 | simp2d 1144 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β 0 β€ (π₯ β (πΊβπ))) |
150 | 130, 139 | subge0d 11752 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β (0 β€ (π₯ β (πΊβπ)) β (πΊβπ) β€ π₯)) |
151 | 149, 150 | mpbid 231 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β (πΊβπ) β€ π₯) |
152 | 131, 139,
130, 143, 151 | letrd 11319 |
. . . . . 6
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β -1 β€ π₯) |
153 | | peano2re 11335 |
. . . . . . . 8
β’ ((πΊβπ) β β β ((πΊβπ) + 1) β β) |
154 | 139, 153 | syl 17 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β ((πΊβπ) + 1) β β) |
155 | | 2re 12234 |
. . . . . . . 8
β’ 2 β
β |
156 | 155 | a1i 11 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β 2 β β) |
157 | 148 | simp3d 1145 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β (π₯ β (πΊβπ)) β€ 1) |
158 | | 1red 11163 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β 1 β β) |
159 | 130, 139,
158 | lesubadd2d 11761 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β ((π₯ β (πΊβπ)) β€ 1 β π₯ β€ ((πΊβπ) + 1))) |
160 | 157, 159 | mpbid 231 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β π₯ β€ ((πΊβπ) + 1)) |
161 | 142 | simp3d 1145 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β (πΊβπ) β€ 1) |
162 | 139, 158,
158, 161 | leadd1dd 11776 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β ((πΊβπ) + 1) β€ (1 + 1)) |
163 | | df-2 12223 |
. . . . . . . 8
β’ 2 = (1 +
1) |
164 | 162, 163 | breqtrrdi 5152 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β ((πΊβπ) + 1) β€ 2) |
165 | 130, 154,
156, 160, 164 | letrd 11319 |
. . . . . 6
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β π₯ β€ 2) |
166 | 84, 155 | elicc2i 13337 |
. . . . . 6
β’ (π₯ β (-1[,]2) β (π₯ β β β§ -1 β€
π₯ β§ π₯ β€ 2)) |
167 | 130, 152,
165, 166 | syl3anbrc 1344 |
. . . . 5
β’ (((π β§ π β β) β§ π₯ β (πβπ)) β π₯ β (-1[,]2)) |
168 | 167 | rexlimdva2 3155 |
. . . 4
β’ (π β (βπ β β π₯ β (πβπ) β π₯ β (-1[,]2))) |
169 | 116, 168 | biimtrid 241 |
. . 3
β’ (π β (π₯ β βͺ
π β β (πβπ) β π₯ β (-1[,]2))) |
170 | 169 | ssrdv 3955 |
. 2
β’ (π β βͺ π β β (πβπ) β (-1[,]2)) |
171 | 26, 115, 170 | 3jca 1129 |
1
β’ (π β (ran πΉ β (0[,]1) β§ (0[,]1) β
βͺ π β β (πβπ) β§ βͺ
π β β (πβπ) β (-1[,]2))) |