Step | Hyp | Ref
| Expression |
1 | | stoweidlem27.4 |
. . . 4
β’ (π β π Fn ran πΊ) |
2 | | stoweidlem27.5 |
. . . 4
β’ (π β ran πΊ β V) |
3 | | fnex 7172 |
. . . 4
β’ ((π Fn ran πΊ β§ ran πΊ β V) β π β V) |
4 | 1, 2, 3 | syl2anc 585 |
. . 3
β’ (π β π β V) |
5 | | stoweidlem27.7 |
. . . . 5
β’ (π β πΉ:(1...π)β1-1-ontoβran
πΊ) |
6 | | f1ofn 6790 |
. . . . 5
β’ (πΉ:(1...π)β1-1-ontoβran
πΊ β πΉ Fn (1...π)) |
7 | 5, 6 | syl 17 |
. . . 4
β’ (π β πΉ Fn (1...π)) |
8 | | ovex 7395 |
. . . 4
β’
(1...π) β
V |
9 | | fnex 7172 |
. . . 4
β’ ((πΉ Fn (1...π) β§ (1...π) β V) β πΉ β V) |
10 | 7, 8, 9 | sylancl 587 |
. . 3
β’ (π β πΉ β V) |
11 | | coexg 7871 |
. . 3
β’ ((π β V β§ πΉ β V) β (π β πΉ) β V) |
12 | 4, 10, 11 | syl2anc 585 |
. 2
β’ (π β (π β πΉ) β V) |
13 | | stoweidlem27.3 |
. . 3
β’ (π β π β β) |
14 | | f1of 6789 |
. . . . . 6
β’ (πΉ:(1...π)β1-1-ontoβran
πΊ β πΉ:(1...π)βΆran πΊ) |
15 | 5, 14 | syl 17 |
. . . . 5
β’ (π β πΉ:(1...π)βΆran πΊ) |
16 | | fnfco 6712 |
. . . . 5
β’ ((π Fn ran πΊ β§ πΉ:(1...π)βΆran πΊ) β (π β πΉ) Fn (1...π)) |
17 | 1, 15, 16 | syl2anc 585 |
. . . 4
β’ (π β (π β πΉ) Fn (1...π)) |
18 | | rncoss 5932 |
. . . . 5
β’ ran
(π β πΉ) β ran π |
19 | | fvelrnb 6908 |
. . . . . . . . . . 11
β’ (π Fn ran πΊ β (π β ran π β βπ β ran πΊ(πβπ) = π)) |
20 | 1, 19 | syl 17 |
. . . . . . . . . 10
β’ (π β (π β ran π β βπ β ran πΊ(πβπ) = π)) |
21 | 20 | biimpa 478 |
. . . . . . . . 9
β’ ((π β§ π β ran π) β βπ β ran πΊ(πβπ) = π) |
22 | | stoweidlem27.10 |
. . . . . . . . . . . . . 14
β’
β²π€π |
23 | | stoweidlem27.1 |
. . . . . . . . . . . . . . . . 17
β’ πΊ = (π€ β π β¦ {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
24 | | nfmpt1 5218 |
. . . . . . . . . . . . . . . . 17
β’
β²π€(π€ β π β¦ {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
25 | 23, 24 | nfcxfr 2906 |
. . . . . . . . . . . . . . . 16
β’
β²π€πΊ |
26 | 25 | nfrn 5912 |
. . . . . . . . . . . . . . 15
β’
β²π€ran
πΊ |
27 | 26 | nfcri 2895 |
. . . . . . . . . . . . . 14
β’
β²π€ π β ran πΊ |
28 | 22, 27 | nfan 1903 |
. . . . . . . . . . . . 13
β’
β²π€(π β§ π β ran πΊ) |
29 | | stoweidlem27.6 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β ran πΊ) β (πβπ) β π) |
30 | 29 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β ran πΊ) β§ π€ β π) β§ π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) β (πβπ) β π) |
31 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β ran πΊ) β§ π€ β π) β§ π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) β π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
32 | 30, 31 | eleqtrd 2840 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β ran πΊ) β§ π€ β π) β§ π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) β (πβπ) β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
33 | | nfcv 2908 |
. . . . . . . . . . . . . . . 16
β’
β²β(πβπ) |
34 | | stoweidlem27.11 |
. . . . . . . . . . . . . . . 16
β’
β²βπ |
35 | | nfv 1918 |
. . . . . . . . . . . . . . . 16
β’
β²β π€ = {π‘ β π β£ 0 < ((πβπ)βπ‘)} |
36 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . 19
β’ (β = (πβπ) β (ββπ‘) = ((πβπ)βπ‘)) |
37 | 36 | breq2d 5122 |
. . . . . . . . . . . . . . . . . 18
β’ (β = (πβπ) β (0 < (ββπ‘) β 0 < ((πβπ)βπ‘))) |
38 | 37 | rabbidv 3418 |
. . . . . . . . . . . . . . . . 17
β’ (β = (πβπ) β {π‘ β π β£ 0 < (ββπ‘)} = {π‘ β π β£ 0 < ((πβπ)βπ‘)}) |
39 | 38 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
β’ (β = (πβπ) β (π€ = {π‘ β π β£ 0 < (ββπ‘)} β π€ = {π‘ β π β£ 0 < ((πβπ)βπ‘)})) |
40 | 33, 34, 35, 39 | elrabf 3646 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β ((πβπ) β π β§ π€ = {π‘ β π β£ 0 < ((πβπ)βπ‘)})) |
41 | 32, 40 | sylib 217 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β ran πΊ) β§ π€ β π) β§ π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) β ((πβπ) β π β§ π€ = {π‘ β π β£ 0 < ((πβπ)βπ‘)})) |
42 | 41 | simpld 496 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β ran πΊ) β§ π€ β π) β§ π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) β (πβπ) β π) |
43 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ran πΊ) β π β ran πΊ) |
44 | 23 | elrnmpt 5916 |
. . . . . . . . . . . . . . 15
β’ (π β ran πΊ β (π β ran πΊ β βπ€ β π π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}})) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ran πΊ) β (π β ran πΊ β βπ€ β π π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}})) |
46 | 43, 45 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ran πΊ) β βπ€ β π π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
47 | 28, 42, 46 | r19.29af 3254 |
. . . . . . . . . . . 12
β’ ((π β§ π β ran πΊ) β (πβπ) β π) |
48 | 47 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β ran π) β§ π β ran πΊ) β (πβπ) β π) |
49 | | eleq1 2826 |
. . . . . . . . . . 11
β’ ((πβπ) = π β ((πβπ) β π β π β π)) |
50 | 48, 49 | syl5ibcom 244 |
. . . . . . . . . 10
β’ (((π β§ π β ran π) β§ π β ran πΊ) β ((πβπ) = π β π β π)) |
51 | 50 | reximdva 3166 |
. . . . . . . . 9
β’ ((π β§ π β ran π) β (βπ β ran πΊ(πβπ) = π β βπ β ran πΊ π β π)) |
52 | 21, 51 | mpd 15 |
. . . . . . . 8
β’ ((π β§ π β ran π) β βπ β ran πΊ π β π) |
53 | | idd 24 |
. . . . . . . . . 10
β’ (π β ran πΊ β (π β π β π β π)) |
54 | 53 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β ran π) β (π β ran πΊ β (π β π β π β π))) |
55 | 54 | rexlimdv 3151 |
. . . . . . . 8
β’ ((π β§ π β ran π) β (βπ β ran πΊ π β π β π β π)) |
56 | 52, 55 | mpd 15 |
. . . . . . 7
β’ ((π β§ π β ran π) β π β π) |
57 | 56 | ex 414 |
. . . . . 6
β’ (π β (π β ran π β π β π)) |
58 | 57 | ssrdv 3955 |
. . . . 5
β’ (π β ran π β π) |
59 | 18, 58 | sstrid 3960 |
. . . 4
β’ (π β ran (π β πΉ) β π) |
60 | | df-f 6505 |
. . . 4
β’ ((π β πΉ):(1...π)βΆπ β ((π β πΉ) Fn (1...π) β§ ran (π β πΉ) β π)) |
61 | 17, 59, 60 | sylanbrc 584 |
. . 3
β’ (π β (π β πΉ):(1...π)βΆπ) |
62 | | stoweidlem27.9 |
. . . 4
β’
β²π‘π |
63 | | nfv 1918 |
. . . . . . 7
β’
β²π€ π‘ β (π β π) |
64 | 22, 63 | nfan 1903 |
. . . . . 6
β’
β²π€(π β§ π‘ β (π β π)) |
65 | | nfv 1918 |
. . . . . 6
β’
β²π€βπ β (1...π)0 < (((π β πΉ)βπ)βπ‘) |
66 | | stoweidlem27.8 |
. . . . . . . 8
β’ (π β (π β π) β βͺ π) |
67 | 66 | sselda 3949 |
. . . . . . 7
β’ ((π β§ π‘ β (π β π)) β π‘ β βͺ π) |
68 | | eluni 4873 |
. . . . . . 7
β’ (π‘ β βͺ π
β βπ€(π‘ β π€ β§ π€ β π)) |
69 | 67, 68 | sylib 217 |
. . . . . 6
β’ ((π β§ π‘ β (π β π)) β βπ€(π‘ β π€ β§ π€ β π)) |
70 | 23 | funmpt2 6545 |
. . . . . . . . . . . 12
β’ Fun πΊ |
71 | 23 | dmeqi 5865 |
. . . . . . . . . . . . . . 15
β’ dom πΊ = dom (π€ β π β¦ {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
72 | | stoweidlem27.2 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β V) |
73 | 34 | rabexgf 43303 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β V β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β V) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β V) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π€ β π) β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β V) |
76 | 75 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π€ β π β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β V)) |
77 | 22, 76 | ralrimi 3243 |
. . . . . . . . . . . . . . . 16
β’ (π β βπ€ β π {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β V) |
78 | | dmmptg 6199 |
. . . . . . . . . . . . . . . 16
β’
(βπ€ β
π {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β V β dom (π€ β π β¦ {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) = π) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β dom (π€ β π β¦ {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) = π) |
80 | 71, 79 | eqtrid 2789 |
. . . . . . . . . . . . . 14
β’ (π β dom πΊ = π) |
81 | 80 | eleq2d 2824 |
. . . . . . . . . . . . 13
β’ (π β (π€ β dom πΊ β π€ β π)) |
82 | 81 | biimpar 479 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β π) β π€ β dom πΊ) |
83 | | fvelrn 7032 |
. . . . . . . . . . . 12
β’ ((Fun
πΊ β§ π€ β dom πΊ) β (πΊβπ€) β ran πΊ) |
84 | 70, 82, 83 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π β§ π€ β π) β (πΊβπ€) β ran πΊ) |
85 | 84 | adantrl 715 |
. . . . . . . . . 10
β’ ((π β§ (π‘ β π€ β§ π€ β π)) β (πΊβπ€) β ran πΊ) |
86 | 15 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΊβπ€) β ran πΊ) β§ (π β (1...π) β§ (πΉβπ) = (πΊβπ€))) β πΉ:(1...π)βΆran πΊ) |
87 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ (((π β§ (πΊβπ€) β ran πΊ) β§ (π β (1...π) β§ (πΉβπ) = (πΊβπ€))) β π β (1...π)) |
88 | | fvco3 6945 |
. . . . . . . . . . . . . 14
β’ ((πΉ:(1...π)βΆran πΊ β§ π β (1...π)) β ((π β πΉ)βπ) = (πβ(πΉβπ))) |
89 | 86, 87, 88 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΊβπ€) β ran πΊ) β§ (π β (1...π) β§ (πΉβπ) = (πΊβπ€))) β ((π β πΉ)βπ) = (πβ(πΉβπ))) |
90 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ) = (πΊβπ€) β (πβ(πΉβπ)) = (πβ(πΊβπ€))) |
91 | 90 | ad2antll 728 |
. . . . . . . . . . . . 13
β’ (((π β§ (πΊβπ€) β ran πΊ) β§ (π β (1...π) β§ (πΉβπ) = (πΊβπ€))) β (πβ(πΉβπ)) = (πβ(πΊβπ€))) |
92 | 89, 91 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊβπ€) β ran πΊ) β§ (π β (1...π) β§ (πΉβπ) = (πΊβπ€))) β ((π β πΉ)βπ) = (πβ(πΊβπ€))) |
93 | | eleq1 2826 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πΊβπ€) β (π β ran πΊ β (πΊβπ€) β ran πΊ)) |
94 | 93 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
β’ (π = (πΊβπ€) β ((π β§ π β ran πΊ) β (π β§ (πΊβπ€) β ran πΊ))) |
95 | | eleq2 2827 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πΊβπ€) β ((πβπ) β π β (πβπ) β (πΊβπ€))) |
96 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πΊβπ€) β (πβπ) = (πβ(πΊβπ€))) |
97 | 96 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πΊβπ€) β ((πβπ) β (πΊβπ€) β (πβ(πΊβπ€)) β (πΊβπ€))) |
98 | 95, 97 | bitrd 279 |
. . . . . . . . . . . . . . . 16
β’ (π = (πΊβπ€) β ((πβπ) β π β (πβ(πΊβπ€)) β (πΊβπ€))) |
99 | 94, 98 | imbi12d 345 |
. . . . . . . . . . . . . . 15
β’ (π = (πΊβπ€) β (((π β§ π β ran πΊ) β (πβπ) β π) β ((π β§ (πΊβπ€) β ran πΊ) β (πβ(πΊβπ€)) β (πΊβπ€)))) |
100 | 99, 29 | vtoclg 3528 |
. . . . . . . . . . . . . 14
β’ ((πΊβπ€) β ran πΊ β ((π β§ (πΊβπ€) β ran πΊ) β (πβ(πΊβπ€)) β (πΊβπ€))) |
101 | 100 | anabsi7 670 |
. . . . . . . . . . . . 13
β’ ((π β§ (πΊβπ€) β ran πΊ) β (πβ(πΊβπ€)) β (πΊβπ€)) |
102 | 101 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (πΊβπ€) β ran πΊ) β§ (π β (1...π) β§ (πΉβπ) = (πΊβπ€))) β (πβ(πΊβπ€)) β (πΊβπ€)) |
103 | 92, 102 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ (((π β§ (πΊβπ€) β ran πΊ) β§ (π β (1...π) β§ (πΉβπ) = (πΊβπ€))) β ((π β πΉ)βπ) β (πΊβπ€)) |
104 | | f1ofo 6796 |
. . . . . . . . . . . . . . 15
β’ (πΉ:(1...π)β1-1-ontoβran
πΊ β πΉ:(1...π)βontoβran πΊ) |
105 | | forn 6764 |
. . . . . . . . . . . . . . 15
β’ (πΉ:(1...π)βontoβran πΊ β ran πΉ = ran πΊ) |
106 | 5, 104, 105 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β ran πΉ = ran πΊ) |
107 | 106 | eleq2d 2824 |
. . . . . . . . . . . . 13
β’ (π β ((πΊβπ€) β ran πΉ β (πΊβπ€) β ran πΊ)) |
108 | 107 | biimpar 479 |
. . . . . . . . . . . 12
β’ ((π β§ (πΊβπ€) β ran πΊ) β (πΊβπ€) β ran πΉ) |
109 | 7 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (πΊβπ€) β ran πΊ) β πΉ Fn (1...π)) |
110 | | fvelrnb 6908 |
. . . . . . . . . . . . 13
β’ (πΉ Fn (1...π) β ((πΊβπ€) β ran πΉ β βπ β (1...π)(πΉβπ) = (πΊβπ€))) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ (πΊβπ€) β ran πΊ) β ((πΊβπ€) β ran πΉ β βπ β (1...π)(πΉβπ) = (πΊβπ€))) |
112 | 108, 111 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ (πΊβπ€) β ran πΊ) β βπ β (1...π)(πΉβπ) = (πΊβπ€)) |
113 | 103, 112 | reximddv 3169 |
. . . . . . . . . 10
β’ ((π β§ (πΊβπ€) β ran πΊ) β βπ β (1...π)((π β πΉ)βπ) β (πΊβπ€)) |
114 | 85, 113 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ (π‘ β π€ β§ π€ β π)) β βπ β (1...π)((π β πΉ)βπ) β (πΊβπ€)) |
115 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π‘ β π€ β§ π€ β π)) β§ ((π β πΉ)βπ) β (πΊβπ€)) β π‘ β π€) |
116 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π€ β π) β π€ β π) |
117 | 23 | fvmpt2 6964 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π€ β π β§ {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β V) β (πΊβπ€) = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
118 | 116, 75, 117 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π€ β π) β (πΊβπ€) = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
119 | 118 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π€ β π) β (((π β πΉ)βπ) β (πΊβπ€) β ((π β πΉ)βπ) β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}})) |
120 | 119 | biimpa 478 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π€ β π) β§ ((π β πΉ)βπ) β (πΊβπ€)) β ((π β πΉ)βπ) β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
121 | 120 | adantlrl 719 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π‘ β π€ β§ π€ β π)) β§ ((π β πΉ)βπ) β (πΊβπ€)) β ((π β πΉ)βπ) β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
122 | | nfcv 2908 |
. . . . . . . . . . . . . . . . 17
β’
β²β((π β πΉ)βπ) |
123 | | nfv 1918 |
. . . . . . . . . . . . . . . . 17
β’
β²β π€ = {π‘ β π β£ 0 < (((π β πΉ)βπ)βπ‘)} |
124 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β = ((π β πΉ)βπ) β (ββπ‘) = (((π β πΉ)βπ)βπ‘)) |
125 | 124 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . 19
β’ (β = ((π β πΉ)βπ) β (0 < (ββπ‘) β 0 < (((π β πΉ)βπ)βπ‘))) |
126 | 125 | rabbidv 3418 |
. . . . . . . . . . . . . . . . . 18
β’ (β = ((π β πΉ)βπ) β {π‘ β π β£ 0 < (ββπ‘)} = {π‘ β π β£ 0 < (((π β πΉ)βπ)βπ‘)}) |
127 | 126 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . 17
β’ (β = ((π β πΉ)βπ) β (π€ = {π‘ β π β£ 0 < (ββπ‘)} β π€ = {π‘ β π β£ 0 < (((π β πΉ)βπ)βπ‘)})) |
128 | 122, 34, 123, 127 | elrabf 3646 |
. . . . . . . . . . . . . . . 16
β’ (((π β πΉ)βπ) β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β (((π β πΉ)βπ) β π β§ π€ = {π‘ β π β£ 0 < (((π β πΉ)βπ)βπ‘)})) |
129 | 121, 128 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π‘ β π€ β§ π€ β π)) β§ ((π β πΉ)βπ) β (πΊβπ€)) β (((π β πΉ)βπ) β π β§ π€ = {π‘ β π β£ 0 < (((π β πΉ)βπ)βπ‘)})) |
130 | 129 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π‘ β π€ β§ π€ β π)) β§ ((π β πΉ)βπ) β (πΊβπ€)) β π€ = {π‘ β π β£ 0 < (((π β πΉ)βπ)βπ‘)}) |
131 | 115, 130 | eleqtrd 2840 |
. . . . . . . . . . . . 13
β’ (((π β§ (π‘ β π€ β§ π€ β π)) β§ ((π β πΉ)βπ) β (πΊβπ€)) β π‘ β {π‘ β π β£ 0 < (((π β πΉ)βπ)βπ‘)}) |
132 | | rabid 3430 |
. . . . . . . . . . . . 13
β’ (π‘ β {π‘ β π β£ 0 < (((π β πΉ)βπ)βπ‘)} β (π‘ β π β§ 0 < (((π β πΉ)βπ)βπ‘))) |
133 | 131, 132 | sylib 217 |
. . . . . . . . . . . 12
β’ (((π β§ (π‘ β π€ β§ π€ β π)) β§ ((π β πΉ)βπ) β (πΊβπ€)) β (π‘ β π β§ 0 < (((π β πΉ)βπ)βπ‘))) |
134 | 133 | simprd 497 |
. . . . . . . . . . 11
β’ (((π β§ (π‘ β π€ β§ π€ β π)) β§ ((π β πΉ)βπ) β (πΊβπ€)) β 0 < (((π β πΉ)βπ)βπ‘)) |
135 | 134 | ex 414 |
. . . . . . . . . 10
β’ ((π β§ (π‘ β π€ β§ π€ β π)) β (((π β πΉ)βπ) β (πΊβπ€) β 0 < (((π β πΉ)βπ)βπ‘))) |
136 | 135 | reximdv 3168 |
. . . . . . . . 9
β’ ((π β§ (π‘ β π€ β§ π€ β π)) β (βπ β (1...π)((π β πΉ)βπ) β (πΊβπ€) β βπ β (1...π)0 < (((π β πΉ)βπ)βπ‘))) |
137 | 114, 136 | mpd 15 |
. . . . . . . 8
β’ ((π β§ (π‘ β π€ β§ π€ β π)) β βπ β (1...π)0 < (((π β πΉ)βπ)βπ‘)) |
138 | 137 | ex 414 |
. . . . . . 7
β’ (π β ((π‘ β π€ β§ π€ β π) β βπ β (1...π)0 < (((π β πΉ)βπ)βπ‘))) |
139 | 138 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β (π β π)) β ((π‘ β π€ β§ π€ β π) β βπ β (1...π)0 < (((π β πΉ)βπ)βπ‘))) |
140 | 64, 65, 69, 139 | exlimimdd 2213 |
. . . . 5
β’ ((π β§ π‘ β (π β π)) β βπ β (1...π)0 < (((π β πΉ)βπ)βπ‘)) |
141 | 140 | ex 414 |
. . . 4
β’ (π β (π‘ β (π β π) β βπ β (1...π)0 < (((π β πΉ)βπ)βπ‘))) |
142 | 62, 141 | ralrimi 3243 |
. . 3
β’ (π β βπ‘ β (π β π)βπ β (1...π)0 < (((π β πΉ)βπ)βπ‘)) |
143 | 13, 61, 142 | jca32 517 |
. 2
β’ (π β (π β β β§ ((π β πΉ):(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < (((π β πΉ)βπ)βπ‘)))) |
144 | | feq1 6654 |
. . . . 5
β’ (π = (π β πΉ) β (π:(1...π)βΆπ β (π β πΉ):(1...π)βΆπ)) |
145 | | fveq1 6846 |
. . . . . . . . 9
β’ (π = (π β πΉ) β (πβπ) = ((π β πΉ)βπ)) |
146 | 145 | fveq1d 6849 |
. . . . . . . 8
β’ (π = (π β πΉ) β ((πβπ)βπ‘) = (((π β πΉ)βπ)βπ‘)) |
147 | 146 | breq2d 5122 |
. . . . . . 7
β’ (π = (π β πΉ) β (0 < ((πβπ)βπ‘) β 0 < (((π β πΉ)βπ)βπ‘))) |
148 | 147 | rexbidv 3176 |
. . . . . 6
β’ (π = (π β πΉ) β (βπ β (1...π)0 < ((πβπ)βπ‘) β βπ β (1...π)0 < (((π β πΉ)βπ)βπ‘))) |
149 | 148 | ralbidv 3175 |
. . . . 5
β’ (π = (π β πΉ) β (βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘) β βπ‘ β (π β π)βπ β (1...π)0 < (((π β πΉ)βπ)βπ‘))) |
150 | 144, 149 | anbi12d 632 |
. . . 4
β’ (π = (π β πΉ) β ((π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)) β ((π β πΉ):(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < (((π β πΉ)βπ)βπ‘)))) |
151 | 150 | anbi2d 630 |
. . 3
β’ (π = (π β πΉ) β ((π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘))) β (π β β β§ ((π β πΉ):(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < (((π β πΉ)βπ)βπ‘))))) |
152 | 151 | spcegv 3559 |
. 2
β’ ((π β πΉ) β V β ((π β β β§ ((π β πΉ):(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < (((π β πΉ)βπ)βπ‘))) β βπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘))))) |
153 | 12, 143, 152 | sylc 65 |
1
β’ (π β βπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) |