Step | Hyp | Ref
| Expression |
1 | | ulmss.u |
. 2
β’ (π β (π₯ β π β¦ π΄)(βπ’βπ)πΊ) |
2 | | ulmss.z |
. . . . . . . . 9
β’ π =
(β€β₯βπ) |
3 | 2 | uztrn2 12789 |
. . . . . . . 8
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
4 | | ulmss.t |
. . . . . . . . . . 11
β’ (π β π β π) |
5 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β π) |
6 | | ssralv 4015 |
. . . . . . . . . 10
β’ (π β π β (βπ§ β π (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π β βπ§ β π (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π)) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β π) β (βπ§ β π (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π β βπ§ β π (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π)) |
8 | | fvres 6866 |
. . . . . . . . . . . . . . 15
β’ (π§ β π β ((π΄ βΎ π)βπ§) = (π΄βπ§)) |
9 | 8 | ad2antll 728 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β π β§ π§ β π)) β ((π΄ βΎ π)βπ§) = (π΄βπ§)) |
10 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β π β§ π§ β π)) β π₯ β π) |
11 | | ulmss.a |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β π) β π΄ β π) |
12 | 11 | adantrr 716 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π₯ β π β§ π§ β π)) β π΄ β π) |
13 | 12 | resexd 5989 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β π β§ π§ β π)) β (π΄ βΎ π) β V) |
14 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β π β¦ (π΄ βΎ π)) = (π₯ β π β¦ (π΄ βΎ π)) |
15 | 14 | fvmpt2 6964 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β π β§ (π΄ βΎ π) β V) β ((π₯ β π β¦ (π΄ βΎ π))βπ₯) = (π΄ βΎ π)) |
16 | 10, 13, 15 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β π β§ π§ β π)) β ((π₯ β π β¦ (π΄ βΎ π))βπ₯) = (π΄ βΎ π)) |
17 | 16 | fveq1d 6849 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β π β§ π§ β π)) β (((π₯ β π β¦ (π΄ βΎ π))βπ₯)βπ§) = ((π΄ βΎ π)βπ§)) |
18 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β π β¦ π΄) = (π₯ β π β¦ π΄) |
19 | 18 | fvmpt2 6964 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β π β§ π΄ β π) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
20 | 10, 12, 19 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β π β§ π§ β π)) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
21 | 20 | fveq1d 6849 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β π β§ π§ β π)) β (((π₯ β π β¦ π΄)βπ₯)βπ§) = (π΄βπ§)) |
22 | 9, 17, 21 | 3eqtr4d 2787 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π β§ π§ β π)) β (((π₯ β π β¦ (π΄ βΎ π))βπ₯)βπ§) = (((π₯ β π β¦ π΄)βπ₯)βπ§)) |
23 | 22 | ralrimivva 3198 |
. . . . . . . . . . . 12
β’ (π β βπ₯ β π βπ§ β π (((π₯ β π β¦ (π΄ βΎ π))βπ₯)βπ§) = (((π₯ β π β¦ π΄)βπ₯)βπ§)) |
24 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²πβπ§ β π (((π₯ β π β¦ (π΄ βΎ π))βπ₯)βπ§) = (((π₯ β π β¦ π΄)βπ₯)βπ§) |
25 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²π₯π |
26 | | nffvmpt1 6858 |
. . . . . . . . . . . . . . . 16
β’
β²π₯((π₯ β π β¦ (π΄ βΎ π))βπ) |
27 | | nfcv 2908 |
. . . . . . . . . . . . . . . 16
β’
β²π₯π§ |
28 | 26, 27 | nffv 6857 |
. . . . . . . . . . . . . . 15
β’
β²π₯(((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) |
29 | | nffvmpt1 6858 |
. . . . . . . . . . . . . . . 16
β’
β²π₯((π₯ β π β¦ π΄)βπ) |
30 | 29, 27 | nffv 6857 |
. . . . . . . . . . . . . . 15
β’
β²π₯(((π₯ β π β¦ π΄)βπ)βπ§) |
31 | 28, 30 | nfeq 2921 |
. . . . . . . . . . . . . 14
β’
β²π₯(((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) = (((π₯ β π β¦ π΄)βπ)βπ§) |
32 | 25, 31 | nfralw 3297 |
. . . . . . . . . . . . 13
β’
β²π₯βπ§ β π (((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) = (((π₯ β π β¦ π΄)βπ)βπ§) |
33 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β ((π₯ β π β¦ (π΄ βΎ π))βπ₯) = ((π₯ β π β¦ (π΄ βΎ π))βπ)) |
34 | 33 | fveq1d 6849 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (((π₯ β π β¦ (π΄ βΎ π))βπ₯)βπ§) = (((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§)) |
35 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β ((π₯ β π β¦ π΄)βπ₯) = ((π₯ β π β¦ π΄)βπ)) |
36 | 35 | fveq1d 6849 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (((π₯ β π β¦ π΄)βπ₯)βπ§) = (((π₯ β π β¦ π΄)βπ)βπ§)) |
37 | 34, 36 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β ((((π₯ β π β¦ (π΄ βΎ π))βπ₯)βπ§) = (((π₯ β π β¦ π΄)βπ₯)βπ§) β (((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) = (((π₯ β π β¦ π΄)βπ)βπ§))) |
38 | 37 | ralbidv 3175 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (βπ§ β π (((π₯ β π β¦ (π΄ βΎ π))βπ₯)βπ§) = (((π₯ β π β¦ π΄)βπ₯)βπ§) β βπ§ β π (((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) = (((π₯ β π β¦ π΄)βπ)βπ§))) |
39 | 24, 32, 38 | cbvralw 3292 |
. . . . . . . . . . . 12
β’
(βπ₯ β
π βπ§ β π (((π₯ β π β¦ (π΄ βΎ π))βπ₯)βπ§) = (((π₯ β π β¦ π΄)βπ₯)βπ§) β βπ β π βπ§ β π (((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) = (((π₯ β π β¦ π΄)βπ)βπ§)) |
40 | 23, 39 | sylib 217 |
. . . . . . . . . . 11
β’ (π β βπ β π βπ§ β π (((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) = (((π₯ β π β¦ π΄)βπ)βπ§)) |
41 | 40 | r19.21bi 3237 |
. . . . . . . . . 10
β’ ((π β§ π β π) β βπ§ β π (((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) = (((π₯ β π β¦ π΄)βπ)βπ§)) |
42 | | fvoveq1 7385 |
. . . . . . . . . . . 12
β’ ((((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) = (((π₯ β π β¦ π΄)βπ)βπ§) β (absβ((((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) β (πΊβπ§))) = (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§)))) |
43 | 42 | breq1d 5120 |
. . . . . . . . . . 11
β’ ((((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) = (((π₯ β π β¦ π΄)βπ)βπ§) β ((absβ((((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) β (πΊβπ§))) < π β (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π)) |
44 | 43 | ralimi 3087 |
. . . . . . . . . 10
β’
(βπ§ β
π (((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) = (((π₯ β π β¦ π΄)βπ)βπ§) β βπ§ β π ((absβ((((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) β (πΊβπ§))) < π β (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π)) |
45 | | ralbi 3107 |
. . . . . . . . . 10
β’
(βπ§ β
π ((absβ((((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) β (πΊβπ§))) < π β (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π) β (βπ§ β π (absβ((((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) β (πΊβπ§))) < π β βπ§ β π (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π)) |
46 | 41, 44, 45 | 3syl 18 |
. . . . . . . . 9
β’ ((π β§ π β π) β (βπ§ β π (absβ((((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) β (πΊβπ§))) < π β βπ§ β π (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π)) |
47 | 7, 46 | sylibrd 259 |
. . . . . . . 8
β’ ((π β§ π β π) β (βπ§ β π (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π β βπ§ β π (absβ((((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) β (πΊβπ§))) < π)) |
48 | 3, 47 | sylan2 594 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β (βπ§ β π (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π β βπ§ β π (absβ((((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) β (πΊβπ§))) < π)) |
49 | 48 | anassrs 469 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (βπ§ β π (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π β βπ§ β π (absβ((((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) β (πΊβπ§))) < π)) |
50 | 49 | ralimdva 3165 |
. . . . 5
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)βπ§ β π (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π β βπ β (β€β₯βπ)βπ§ β π (absβ((((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) β (πΊβπ§))) < π)) |
51 | 50 | reximdva 3166 |
. . . 4
β’ (π β (βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ((((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) β (πΊβπ§))) < π)) |
52 | 51 | ralimdv 3167 |
. . 3
β’ (π β (βπ β β+
βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π β βπ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ((((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) β (πΊβπ§))) < π)) |
53 | | ulmf 25757 |
. . . . . 6
β’ ((π₯ β π β¦ π΄)(βπ’βπ)πΊ β βπ β β€ (π₯ β π β¦ π΄):(β€β₯βπ)βΆ(β
βm π)) |
54 | 1, 53 | syl 17 |
. . . . 5
β’ (π β βπ β β€ (π₯ β π β¦ π΄):(β€β₯βπ)βΆ(β
βm π)) |
55 | | fdm 6682 |
. . . . . . . 8
β’ ((π₯ β π β¦ π΄):(β€β₯βπ)βΆ(β
βm π)
β dom (π₯ β π β¦ π΄) = (β€β₯βπ)) |
56 | 18 | dmmptss 6198 |
. . . . . . . 8
β’ dom
(π₯ β π β¦ π΄) β π |
57 | 55, 56 | eqsstrrdi 4004 |
. . . . . . 7
β’ ((π₯ β π β¦ π΄):(β€β₯βπ)βΆ(β
βm π)
β (β€β₯βπ) β π) |
58 | | uzid 12785 |
. . . . . . . 8
β’ (π β β€ β π β
(β€β₯βπ)) |
59 | 58 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β β€) β π β (β€β₯βπ)) |
60 | | ssel 3942 |
. . . . . . . 8
β’
((β€β₯βπ) β π β (π β (β€β₯βπ) β π β π)) |
61 | | eluzel2 12775 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β π β β€) |
62 | 61, 2 | eleq2s 2856 |
. . . . . . . 8
β’ (π β π β π β β€) |
63 | 60, 62 | syl6 35 |
. . . . . . 7
β’
((β€β₯βπ) β π β (π β (β€β₯βπ) β π β β€)) |
64 | 57, 59, 63 | syl2imc 41 |
. . . . . 6
β’ ((π β§ π β β€) β ((π₯ β π β¦ π΄):(β€β₯βπ)βΆ(β
βm π)
β π β
β€)) |
65 | 64 | rexlimdva 3153 |
. . . . 5
β’ (π β (βπ β β€ (π₯ β π β¦ π΄):(β€β₯βπ)βΆ(β
βm π)
β π β
β€)) |
66 | 54, 65 | mpd 15 |
. . . 4
β’ (π β π β β€) |
67 | 11 | ralrimiva 3144 |
. . . . . 6
β’ (π β βπ₯ β π π΄ β π) |
68 | 18 | fnmpt 6646 |
. . . . . 6
β’
(βπ₯ β
π π΄ β π β (π₯ β π β¦ π΄) Fn π) |
69 | 67, 68 | syl 17 |
. . . . 5
β’ (π β (π₯ β π β¦ π΄) Fn π) |
70 | | frn 6680 |
. . . . . . 7
β’ ((π₯ β π β¦ π΄):(β€β₯βπ)βΆ(β
βm π)
β ran (π₯ β π β¦ π΄) β (β βm π)) |
71 | 70 | rexlimivw 3149 |
. . . . . 6
β’
(βπ β
β€ (π₯ β π β¦ π΄):(β€β₯βπ)βΆ(β
βm π)
β ran (π₯ β π β¦ π΄) β (β βm π)) |
72 | 54, 71 | syl 17 |
. . . . 5
β’ (π β ran (π₯ β π β¦ π΄) β (β βm π)) |
73 | | df-f 6505 |
. . . . 5
β’ ((π₯ β π β¦ π΄):πβΆ(β βm π) β ((π₯ β π β¦ π΄) Fn π β§ ran (π₯ β π β¦ π΄) β (β βm π))) |
74 | 69, 72, 73 | sylanbrc 584 |
. . . 4
β’ (π β (π₯ β π β¦ π΄):πβΆ(β βm π)) |
75 | | eqidd 2738 |
. . . 4
β’ ((π β§ (π β π β§ π§ β π)) β (((π₯ β π β¦ π΄)βπ)βπ§) = (((π₯ β π β¦ π΄)βπ)βπ§)) |
76 | | eqidd 2738 |
. . . 4
β’ ((π β§ π§ β π) β (πΊβπ§) = (πΊβπ§)) |
77 | | ulmcl 25756 |
. . . . 5
β’ ((π₯ β π β¦ π΄)(βπ’βπ)πΊ β πΊ:πβΆβ) |
78 | 1, 77 | syl 17 |
. . . 4
β’ (π β πΊ:πβΆβ) |
79 | | ulmscl 25754 |
. . . . 5
β’ ((π₯ β π β¦ π΄)(βπ’βπ)πΊ β π β V) |
80 | 1, 79 | syl 17 |
. . . 4
β’ (π β π β V) |
81 | 2, 66, 74, 75, 76, 78, 80 | ulm2 25760 |
. . 3
β’ (π β ((π₯ β π β¦ π΄)(βπ’βπ)πΊ β βπ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ((((π₯ β π β¦ π΄)βπ)βπ§) β (πΊβπ§))) < π)) |
82 | 74 | fvmptelcdm 7066 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β π΄ β (β βm π)) |
83 | | elmapi 8794 |
. . . . . . . 8
β’ (π΄ β (β
βm π)
β π΄:πβΆβ) |
84 | 82, 83 | syl 17 |
. . . . . . 7
β’ ((π β§ π₯ β π) β π΄:πβΆβ) |
85 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π) β π β π) |
86 | 84, 85 | fssresd 6714 |
. . . . . 6
β’ ((π β§ π₯ β π) β (π΄ βΎ π):πβΆβ) |
87 | | cnex 11139 |
. . . . . . 7
β’ β
β V |
88 | 80, 4 | ssexd 5286 |
. . . . . . . 8
β’ (π β π β V) |
89 | 88 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π) β π β V) |
90 | | elmapg 8785 |
. . . . . . 7
β’ ((β
β V β§ π β V)
β ((π΄ βΎ π) β (β
βm π)
β (π΄ βΎ π):πβΆβ)) |
91 | 87, 89, 90 | sylancr 588 |
. . . . . 6
β’ ((π β§ π₯ β π) β ((π΄ βΎ π) β (β βm π) β (π΄ βΎ π):πβΆβ)) |
92 | 86, 91 | mpbird 257 |
. . . . 5
β’ ((π β§ π₯ β π) β (π΄ βΎ π) β (β βm π)) |
93 | 92 | fmpttd 7068 |
. . . 4
β’ (π β (π₯ β π β¦ (π΄ βΎ π)):πβΆ(β βm π)) |
94 | | eqidd 2738 |
. . . 4
β’ ((π β§ (π β π β§ π§ β π)) β (((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) = (((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§)) |
95 | | fvres 6866 |
. . . . 5
β’ (π§ β π β ((πΊ βΎ π)βπ§) = (πΊβπ§)) |
96 | 95 | adantl 483 |
. . . 4
β’ ((π β§ π§ β π) β ((πΊ βΎ π)βπ§) = (πΊβπ§)) |
97 | 78, 4 | fssresd 6714 |
. . . 4
β’ (π β (πΊ βΎ π):πβΆβ) |
98 | 2, 66, 93, 94, 96, 97, 88 | ulm2 25760 |
. . 3
β’ (π β ((π₯ β π β¦ (π΄ βΎ π))(βπ’βπ)(πΊ βΎ π) β βπ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ((((π₯ β π β¦ (π΄ βΎ π))βπ)βπ§) β (πΊβπ§))) < π)) |
99 | 52, 81, 98 | 3imtr4d 294 |
. 2
β’ (π β ((π₯ β π β¦ π΄)(βπ’βπ)πΊ β (π₯ β π β¦ (π΄ βΎ π))(βπ’βπ)(πΊ βΎ π))) |
100 | 1, 99 | mpd 15 |
1
β’ (π β (π₯ β π β¦ (π΄ βΎ π))(βπ’βπ)(πΊ βΎ π)) |