Step | Hyp | Ref
| Expression |
1 | | stoweidlem35.8 |
. . . . . . . . . 10
β’ (π β π β Fin) |
2 | | stoweidlem35.6 |
. . . . . . . . . . 11
β’ πΊ = (π€ β π β¦ {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
3 | 2 | rnmptfi 43114 |
. . . . . . . . . 10
β’ (π β Fin β ran πΊ β Fin) |
4 | 1, 3 | syl 17 |
. . . . . . . . 9
β’ (π β ran πΊ β Fin) |
5 | | fnchoice 42967 |
. . . . . . . . . . 11
β’ (ran
πΊ β Fin β
βπ(π Fn ran πΊ β§ βπ β ran πΊ(π β β
β (πβπ) β π))) |
6 | 5 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ ran πΊ β Fin) β βπ(π Fn ran πΊ β§ βπ β ran πΊ(π β β
β (πβπ) β π))) |
7 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π Fn ran πΊ β§ βπ β ran πΊ(π β β
β (πβπ) β π))) β π Fn ran πΊ) |
8 | | stoweidlem35.2 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π€π |
9 | | nfmpt1 5212 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π€(π€ β π β¦ {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
10 | 2, 9 | nfcxfr 2904 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π€πΊ |
11 | 10 | nfrn 5904 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π€ran
πΊ |
12 | 11 | nfcri 2893 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π€ π β ran πΊ |
13 | 8, 12 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π€(π β§ π β ran πΊ) |
14 | | stoweidlem35.9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β π) |
15 | 14 | sselda 3943 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π€ β π) β π€ β π) |
16 | | stoweidlem35.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ π = {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} |
17 | 15, 16 | eleqtrdi 2849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π€ β π) β π€ β {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
18 | | rabid 3426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π€ β {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} β (π€ β π½ β§ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)})) |
19 | 17, 18 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π€ β π) β (π€ β π½ β§ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)})) |
20 | 19 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π€ β π) β ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}) |
21 | | df-rex 3073 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(ββ β
π π€ = {π‘ β π β£ 0 < (ββπ‘)} β ββ(β β π β§ π€ = {π‘ β π β£ 0 < (ββπ‘)})) |
22 | 20, 21 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π€ β π) β ββ(β β π β§ π€ = {π‘ β π β£ 0 < (ββπ‘)})) |
23 | | rabid 3426 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (β β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β (β β π β§ π€ = {π‘ β π β£ 0 < (ββπ‘)})) |
24 | 23 | exbii 1851 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(ββ β β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β ββ(β β π β§ π€ = {π‘ β π β£ 0 < (ββπ‘)})) |
25 | 22, 24 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π€ β π) β ββ β β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
26 | 25 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π€ β π) β§ π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) β ββ β β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
27 | | stoweidlem35.3 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²βπ |
28 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²β π€ β π |
29 | 27, 28 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²β(π β§ π€ β π) |
30 | | nfrab1 3425 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²β{β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} |
31 | 30 | nfeq2 2923 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²β π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} |
32 | 29, 31 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²β((π β§ π€ β π) β§ π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
33 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β (β β π β β β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}})) |
34 | 33 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β (β β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β β β π)) |
35 | 34 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π€ β π) β§ π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) β (β β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β β β π)) |
36 | 32, 35 | eximd 2210 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π€ β π) β§ π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) β (ββ β β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β ββ β β π)) |
37 | 26, 36 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π€ β π) β§ π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) β ββ β β π) |
38 | 37 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β ran πΊ) β§ π€ β π) β§ π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) β ββ β β π) |
39 | 2 | elrnmpt 5908 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ran πΊ β (π β ran πΊ β βπ€ β π π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}})) |
40 | 39 | ibi 267 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ran πΊ β βπ€ β π π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
41 | 40 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β ran πΊ) β βπ€ β π π = {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
42 | 13, 38, 41 | r19.29af 3250 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β ran πΊ) β ββ β β π) |
43 | | n0 4305 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β
β
ββ β β π) |
44 | 42, 43 | sylibr 233 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β ran πΊ) β π β β
) |
45 | 44 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π Fn ran πΊ β§ βπ β ran πΊ(π β β
β (πβπ) β π))) β§ π β ran πΊ) β π β β
) |
46 | | simplrr 777 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π Fn ran πΊ β§ βπ β ran πΊ(π β β
β (πβπ) β π))) β§ π β ran πΊ) β βπ β ran πΊ(π β β
β (πβπ) β π)) |
47 | | neeq1 3005 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (π β β
β π β β
)) |
48 | | fveq2 6838 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (πβπ) = (πβπ)) |
49 | 48 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((πβπ) β π β (πβπ) β π)) |
50 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((πβπ) β π β (πβπ) β π)) |
51 | 49, 50 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((πβπ) β π β (πβπ) β π)) |
52 | 47, 51 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((π β β
β (πβπ) β π) β (π β β
β (πβπ) β π))) |
53 | 52 | rspccva 3579 |
. . . . . . . . . . . . . . . . . 18
β’
((βπ β
ran πΊ(π β β
β (πβπ) β π) β§ π β ran πΊ) β (π β β
β (πβπ) β π)) |
54 | 46, 53 | sylancom 589 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π Fn ran πΊ β§ βπ β ran πΊ(π β β
β (πβπ) β π))) β§ π β ran πΊ) β (π β β
β (πβπ) β π)) |
55 | 45, 54 | mpd 15 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π Fn ran πΊ β§ βπ β ran πΊ(π β β
β (πβπ) β π))) β§ π β ran πΊ) β (πβπ) β π) |
56 | 55 | ralrimiva 3142 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π Fn ran πΊ β§ βπ β ran πΊ(π β β
β (πβπ) β π))) β βπ β ran πΊ(πβπ) β π) |
57 | | fveq2 6838 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (πβπ) = (πβπ)) |
58 | 57 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((πβπ) β π β (πβπ) β π)) |
59 | | eleq2 2827 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((πβπ) β π β (πβπ) β π)) |
60 | 58, 59 | bitrd 279 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((πβπ) β π β (πβπ) β π)) |
61 | 60 | cbvralvw 3224 |
. . . . . . . . . . . . . . 15
β’
(βπ β
ran πΊ(πβπ) β π β βπ β ran πΊ(πβπ) β π) |
62 | 56, 61 | sylib 217 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π Fn ran πΊ β§ βπ β ran πΊ(π β β
β (πβπ) β π))) β βπ β ran πΊ(πβπ) β π) |
63 | 7, 62 | jca 513 |
. . . . . . . . . . . . 13
β’ ((π β§ (π Fn ran πΊ β§ βπ β ran πΊ(π β β
β (πβπ) β π))) β (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π)) |
64 | 63 | ex 414 |
. . . . . . . . . . . 12
β’ (π β ((π Fn ran πΊ β§ βπ β ran πΊ(π β β
β (πβπ) β π)) β (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π))) |
65 | 64 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ ran πΊ β Fin) β ((π Fn ran πΊ β§ βπ β ran πΊ(π β β
β (πβπ) β π)) β (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π))) |
66 | 65 | eximdv 1921 |
. . . . . . . . . 10
β’ ((π β§ ran πΊ β Fin) β (βπ(π Fn ran πΊ β§ βπ β ran πΊ(π β β
β (πβπ) β π)) β βπ(π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π))) |
67 | 6, 66 | mpd 15 |
. . . . . . . . 9
β’ ((π β§ ran πΊ β Fin) β βπ(π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π)) |
68 | 4, 67 | mpdan 686 |
. . . . . . . 8
β’ (π β βπ(π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π)) |
69 | 68 | ralrimivw 3146 |
. . . . . . 7
β’ (π β βπ β β βπ(π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π)) |
70 | | stoweidlem35.10 |
. . . . . . . . . . . . 13
β’ (π β (π β π) β βͺ π) |
71 | | stoweidlem35.11 |
. . . . . . . . . . . . 13
β’ (π β (π β π) β β
) |
72 | | ssn0 4359 |
. . . . . . . . . . . . 13
β’ (((π β π) β βͺ π β§ (π β π) β β
) β βͺ π
β β
) |
73 | 70, 71, 72 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β βͺ π
β β
) |
74 | 73 | neneqd 2947 |
. . . . . . . . . . 11
β’ (π β Β¬ βͺ π =
β
) |
75 | | unieq 4875 |
. . . . . . . . . . . 12
β’ (π = β
β βͺ π =
βͺ β
) |
76 | | uni0 4895 |
. . . . . . . . . . . 12
β’ βͺ β
= β
|
77 | 75, 76 | eqtrdi 2794 |
. . . . . . . . . . 11
β’ (π = β
β βͺ π =
β
) |
78 | 74, 77 | nsyl 140 |
. . . . . . . . . 10
β’ (π β Β¬ π = β
) |
79 | | dm0rn0 5877 |
. . . . . . . . . . 11
β’ (dom
πΊ = β
β ran
πΊ =
β
) |
80 | | stoweidlem35.4 |
. . . . . . . . . . . . . . . . . 18
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} |
81 | | stoweidlem35.7 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΄ β V) |
82 | 80, 81 | rabexd 5289 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β V) |
83 | | nfrab1 3425 |
. . . . . . . . . . . . . . . . . . 19
β’
β²β{β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} |
84 | 80, 83 | nfcxfr 2904 |
. . . . . . . . . . . . . . . . . 18
β’
β²βπ |
85 | 84 | rabexgf 42962 |
. . . . . . . . . . . . . . . . 17
β’ (π β V β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β V) |
86 | 82, 85 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β V) |
87 | 86 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π€ β π) β {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} β V) |
88 | 8, 87, 2 | fmptdf 7060 |
. . . . . . . . . . . . . 14
β’ (π β πΊ:πβΆV) |
89 | | dffn2 6666 |
. . . . . . . . . . . . . 14
β’ (πΊ Fn π β πΊ:πβΆV) |
90 | 88, 89 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (π β πΊ Fn π) |
91 | 90 | fndmd 6603 |
. . . . . . . . . . . 12
β’ (π β dom πΊ = π) |
92 | 91 | eqeq1d 2740 |
. . . . . . . . . . 11
β’ (π β (dom πΊ = β
β π = β
)) |
93 | 79, 92 | bitr3id 285 |
. . . . . . . . . 10
β’ (π β (ran πΊ = β
β π = β
)) |
94 | 78, 93 | mtbird 325 |
. . . . . . . . 9
β’ (π β Β¬ ran πΊ = β
) |
95 | | fz1f1o 15530 |
. . . . . . . . . . 11
β’ (ran
πΊ β Fin β (ran
πΊ = β
β¨
((β―βran πΊ)
β β β§ βπ π:(1...(β―βran πΊ))β1-1-ontoβran
πΊ))) |
96 | 4, 95 | syl 17 |
. . . . . . . . . 10
β’ (π β (ran πΊ = β
β¨ ((β―βran πΊ) β β β§
βπ π:(1...(β―βran πΊ))β1-1-ontoβran
πΊ))) |
97 | 96 | ord 863 |
. . . . . . . . 9
β’ (π β (Β¬ ran πΊ = β
β
((β―βran πΊ)
β β β§ βπ π:(1...(β―βran πΊ))β1-1-ontoβran
πΊ))) |
98 | 94, 97 | mpd 15 |
. . . . . . . 8
β’ (π β ((β―βran πΊ) β β β§
βπ π:(1...(β―βran πΊ))β1-1-ontoβran
πΊ)) |
99 | | oveq2 7358 |
. . . . . . . . . . 11
β’ (π = (β―βran πΊ) β (1...π) = (1...(β―βran πΊ))) |
100 | 99 | f1oeq2d 6776 |
. . . . . . . . . 10
β’ (π = (β―βran πΊ) β (π:(1...π)β1-1-ontoβran
πΊ β π:(1...(β―βran πΊ))β1-1-ontoβran
πΊ)) |
101 | 100 | exbidv 1925 |
. . . . . . . . 9
β’ (π = (β―βran πΊ) β (βπ π:(1...π)β1-1-ontoβran
πΊ β βπ π:(1...(β―βran πΊ))β1-1-ontoβran
πΊ)) |
102 | 101 | rspcev 3580 |
. . . . . . . 8
β’
(((β―βran πΊ) β β β§ βπ π:(1...(β―βran πΊ))β1-1-ontoβran
πΊ) β βπ β β βπ π:(1...π)β1-1-ontoβran
πΊ) |
103 | 98, 102 | syl 17 |
. . . . . . 7
β’ (π β βπ β β βπ π:(1...π)β1-1-ontoβran
πΊ) |
104 | | r19.29 3116 |
. . . . . . 7
β’
((βπ β
β βπ(π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ βπ β β βπ π:(1...π)β1-1-ontoβran
πΊ) β βπ β β (βπ(π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ βπ π:(1...π)β1-1-ontoβran
πΊ)) |
105 | 69, 103, 104 | syl2anc 585 |
. . . . . 6
β’ (π β βπ β β (βπ(π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ βπ π:(1...π)β1-1-ontoβran
πΊ)) |
106 | | exdistrv 1960 |
. . . . . . . . 9
β’
(βπβπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ) β (βπ(π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ βπ π:(1...π)β1-1-ontoβran
πΊ)) |
107 | 106 | biimpri 227 |
. . . . . . . 8
β’
((βπ(π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ βπ π:(1...π)β1-1-ontoβran
πΊ) β βπβπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ)) |
108 | 107 | a1i 11 |
. . . . . . 7
β’ (π β ((βπ(π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ βπ π:(1...π)β1-1-ontoβran
πΊ) β βπβπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ))) |
109 | 108 | reximdv 3166 |
. . . . . 6
β’ (π β (βπ β β (βπ(π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ βπ π:(1...π)β1-1-ontoβran
πΊ) β βπ β β βπβπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ))) |
110 | 105, 109 | mpd 15 |
. . . . 5
β’ (π β βπ β β βπβπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ)) |
111 | | df-rex 3073 |
. . . . 5
β’
(βπ β
β βπβπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ) β βπ(π β β β§ βπβπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ))) |
112 | 110, 111 | sylib 217 |
. . . 4
β’ (π β βπ(π β β β§ βπβπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ))) |
113 | | ax-5 1914 |
. . . . . . . . 9
β’ (π β β β
βπ π β
β) |
114 | | 19.29 1877 |
. . . . . . . . 9
β’
((βπ π β β β§
βπβπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ)) β βπ(π β β β§ βπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ))) |
115 | 113, 114 | sylan 581 |
. . . . . . . 8
β’ ((π β β β§
βπβπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ)) β βπ(π β β β§ βπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ))) |
116 | | ax-5 1914 |
. . . . . . . . . 10
β’ (π β β β
βπ π β
β) |
117 | | 19.29 1877 |
. . . . . . . . . 10
β’
((βπ π β β β§
βπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ)) β βπ(π β β β§ ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ))) |
118 | 116, 117 | sylan 581 |
. . . . . . . . 9
β’ ((π β β β§
βπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ)) β βπ(π β β β§ ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ))) |
119 | 118 | eximi 1838 |
. . . . . . . 8
β’
(βπ(π β β β§
βπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ)) β βπβπ(π β β β§ ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ))) |
120 | 115, 119 | syl 17 |
. . . . . . 7
β’ ((π β β β§
βπβπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ)) β βπβπ(π β β β§ ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ))) |
121 | | df-3an 1090 |
. . . . . . . . 9
β’ ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ) β ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ)) |
122 | 121 | anbi2i 624 |
. . . . . . . 8
β’ ((π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ)) β (π β β β§ ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ))) |
123 | 122 | 2exbii 1852 |
. . . . . . 7
β’
(βπβπ(π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ)) β βπβπ(π β β β§ ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ))) |
124 | 120, 123 | sylibr 233 |
. . . . . 6
β’ ((π β β β§
βπβπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ)) β βπβπ(π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ))) |
125 | 124 | a1i 11 |
. . . . 5
β’ (π β ((π β β β§ βπβπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ)) β βπβπ(π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ)))) |
126 | 125 | eximdv 1921 |
. . . 4
β’ (π β (βπ(π β β β§ βπβπ((π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π) β§ π:(1...π)β1-1-ontoβran
πΊ)) β βπβπβπ(π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ)))) |
127 | 112, 126 | mpd 15 |
. . 3
β’ (π β βπβπβπ(π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ))) |
128 | 82 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ))) β π β V) |
129 | | simprl 770 |
. . . . . . 7
β’ ((π β§ (π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ))) β π β
β) |
130 | | simprr1 1222 |
. . . . . . 7
β’ ((π β§ (π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ))) β π Fn ran πΊ) |
131 | | elex 3462 |
. . . . . . . . 9
β’ (ran
πΊ β Fin β ran
πΊ β
V) |
132 | 4, 131 | syl 17 |
. . . . . . . 8
β’ (π β ran πΊ β V) |
133 | 132 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ))) β ran πΊ β V) |
134 | | simprr2 1223 |
. . . . . . . 8
β’ ((π β§ (π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ))) β βπ β ran πΊ(πβπ) β π) |
135 | 51 | rspccva 3579 |
. . . . . . . 8
β’
((βπ β
ran πΊ(πβπ) β π β§ π β ran πΊ) β (πβπ) β π) |
136 | 134, 135 | sylan 581 |
. . . . . . 7
β’ (((π β§ (π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ))) β§ π β ran πΊ) β (πβπ) β π) |
137 | | simprr3 1224 |
. . . . . . 7
β’ ((π β§ (π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ))) β π:(1...π)β1-1-ontoβran
πΊ) |
138 | 70 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ))) β (π β π) β βͺ π) |
139 | | stoweidlem35.1 |
. . . . . . . 8
β’
β²π‘π |
140 | | nfv 1918 |
. . . . . . . . 9
β’
β²π‘ π β β |
141 | | nfcv 2906 |
. . . . . . . . . . 11
β’
β²π‘π |
142 | | nfcv 2906 |
. . . . . . . . . . . . . 14
β’
β²π‘π |
143 | | nfrab1 3425 |
. . . . . . . . . . . . . . . 16
β’
β²π‘{π‘ β π β£ 0 < (ββπ‘)} |
144 | 143 | nfeq2 2923 |
. . . . . . . . . . . . . . 15
β’
β²π‘ π€ = {π‘ β π β£ 0 < (ββπ‘)} |
145 | | nfv 1918 |
. . . . . . . . . . . . . . . . . 18
β’
β²π‘(ββπ) = 0 |
146 | | nfra1 3266 |
. . . . . . . . . . . . . . . . . 18
β’
β²π‘βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) |
147 | 145, 146 | nfan 1903 |
. . . . . . . . . . . . . . . . 17
β’
β²π‘((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)) |
148 | | nfcv 2906 |
. . . . . . . . . . . . . . . . 17
β’
β²π‘π΄ |
149 | 147, 148 | nfrabw 3439 |
. . . . . . . . . . . . . . . 16
β’
β²π‘{β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} |
150 | 80, 149 | nfcxfr 2904 |
. . . . . . . . . . . . . . 15
β’
β²π‘π |
151 | 144, 150 | nfrabw 3439 |
. . . . . . . . . . . . . 14
β’
β²π‘{β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}} |
152 | 142, 151 | nfmpt 5211 |
. . . . . . . . . . . . 13
β’
β²π‘(π€ β π β¦ {β β π β£ π€ = {π‘ β π β£ 0 < (ββπ‘)}}) |
153 | 2, 152 | nfcxfr 2904 |
. . . . . . . . . . . 12
β’
β²π‘πΊ |
154 | 153 | nfrn 5904 |
. . . . . . . . . . 11
β’
β²π‘ran
πΊ |
155 | 141, 154 | nffn 6597 |
. . . . . . . . . 10
β’
β²π‘ π Fn ran πΊ |
156 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π‘(πβπ) β π |
157 | 154, 156 | nfralw 3293 |
. . . . . . . . . 10
β’
β²π‘βπ β ran πΊ(πβπ) β π |
158 | | nfcv 2906 |
. . . . . . . . . . 11
β’
β²π‘π |
159 | | nfcv 2906 |
. . . . . . . . . . 11
β’
β²π‘(1...π) |
160 | 158, 159,
154 | nff1o 6778 |
. . . . . . . . . 10
β’
β²π‘ π:(1...π)β1-1-ontoβran
πΊ |
161 | 155, 157,
160 | nf3an 1905 |
. . . . . . . . 9
β’
β²π‘(π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ) |
162 | 140, 161 | nfan 1903 |
. . . . . . . 8
β’
β²π‘(π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ)) |
163 | 139, 162 | nfan 1903 |
. . . . . . 7
β’
β²π‘(π β§ (π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ))) |
164 | | nfv 1918 |
. . . . . . . . 9
β’
β²π€ π β β |
165 | | nfcv 2906 |
. . . . . . . . . . 11
β’
β²π€π |
166 | 165, 11 | nffn 6597 |
. . . . . . . . . 10
β’
β²π€ π Fn ran πΊ |
167 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π€(πβπ) β π |
168 | 11, 167 | nfralw 3293 |
. . . . . . . . . 10
β’
β²π€βπ β ran πΊ(πβπ) β π |
169 | | nfcv 2906 |
. . . . . . . . . . 11
β’
β²π€π |
170 | | nfcv 2906 |
. . . . . . . . . . 11
β’
β²π€(1...π) |
171 | 169, 170,
11 | nff1o 6778 |
. . . . . . . . . 10
β’
β²π€ π:(1...π)β1-1-ontoβran
πΊ |
172 | 166, 168,
171 | nf3an 1905 |
. . . . . . . . 9
β’
β²π€(π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ) |
173 | 164, 172 | nfan 1903 |
. . . . . . . 8
β’
β²π€(π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ)) |
174 | 8, 173 | nfan 1903 |
. . . . . . 7
β’
β²π€(π β§ (π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ))) |
175 | 2, 128, 129, 130, 133, 136, 137, 138, 163, 174, 84 | stoweidlem27 43990 |
. . . . . 6
β’ ((π β§ (π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ))) β βπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) |
176 | 175 | ex 414 |
. . . . 5
β’ (π β ((π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ)) β βπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘))))) |
177 | 176 | 2eximdv 1923 |
. . . 4
β’ (π β (βπβπ(π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ)) β βπβπβπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘))))) |
178 | 177 | eximdv 1921 |
. . 3
β’ (π β (βπβπβπ(π β β β§ (π Fn ran πΊ β§ βπ β ran πΊ(πβπ) β π β§ π:(1...π)β1-1-ontoβran
πΊ)) β βπβπβπβπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘))))) |
179 | 127, 178 | mpd 15 |
. 2
β’ (π β βπβπβπβπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) |
180 | | id 22 |
. . . 4
β’
(βπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘))) β βπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) |
181 | 180 | exlimivv 1936 |
. . 3
β’
(βπβπβπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘))) β βπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) |
182 | 181 | eximi 1838 |
. 2
β’
(βπβπβπβπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘))) β βπβπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) |
183 | 179, 182 | syl 17 |
1
β’ (π β βπβπ(π β β β§ (π:(1...π)βΆπ β§ βπ‘ β (π β π)βπ β (1...π)0 < ((πβπ)βπ‘)))) |