Step | Hyp | Ref
| Expression |
1 | | stoweidlem29.4 |
. . . . . 6
β’ πΎ = (topGenβran
(,)) |
2 | | stoweidlem29.3 |
. . . . . 6
β’ π = βͺ
π½ |
3 | | eqid 2737 |
. . . . . 6
β’ (π½ Cn πΎ) = (π½ Cn πΎ) |
4 | | stoweidlem29.6 |
. . . . . 6
β’ (π β πΉ β (π½ Cn πΎ)) |
5 | 1, 2, 3, 4 | fcnre 43237 |
. . . . 5
β’ (π β πΉ:πβΆβ) |
6 | | df-f 6501 |
. . . . 5
β’ (πΉ:πβΆβ β (πΉ Fn π β§ ran πΉ β β)) |
7 | 5, 6 | sylib 217 |
. . . 4
β’ (π β (πΉ Fn π β§ ran πΉ β β)) |
8 | 7 | simprd 497 |
. . 3
β’ (π β ran πΉ β β) |
9 | 7 | simpld 496 |
. . . . . . . . 9
β’ (π β πΉ Fn π) |
10 | | fnfun 6603 |
. . . . . . . . 9
β’ (πΉ Fn π β Fun πΉ) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
β’ (π β Fun πΉ) |
12 | 11 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π) β Fun πΉ) |
13 | 5 | fdmd 6680 |
. . . . . . . . . 10
β’ (π β dom πΉ = π) |
14 | 13 | eqcomd 2743 |
. . . . . . . . 9
β’ (π β π = dom πΉ) |
15 | 14 | eleq2d 2824 |
. . . . . . . 8
β’ (π β (π β π β π β dom πΉ)) |
16 | 15 | biimpa 478 |
. . . . . . 7
β’ ((π β§ π β π) β π β dom πΉ) |
17 | | fvelrn 7028 |
. . . . . . 7
β’ ((Fun
πΉ β§ π β dom πΉ) β (πΉβπ ) β ran πΉ) |
18 | 12, 16, 17 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ ) β ran πΉ) |
19 | | stoweidlem29.1 |
. . . . . . . . . 10
β’
β²π‘πΉ |
20 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π‘π |
21 | 19, 20 | nffv 6853 |
. . . . . . . . 9
β’
β²π‘(πΉβπ ) |
22 | 21 | nfeq2 2925 |
. . . . . . . 8
β’
β²π‘ π₯ = (πΉβπ ) |
23 | | breq1 5109 |
. . . . . . . 8
β’ (π₯ = (πΉβπ ) β (π₯ β€ (πΉβπ‘) β (πΉβπ ) β€ (πΉβπ‘))) |
24 | 22, 23 | ralbid 3257 |
. . . . . . 7
β’ (π₯ = (πΉβπ ) β (βπ‘ β π π₯ β€ (πΉβπ‘) β βπ‘ β π (πΉβπ ) β€ (πΉβπ‘))) |
25 | 24 | rspcev 3582 |
. . . . . 6
β’ (((πΉβπ ) β ran πΉ β§ βπ‘ β π (πΉβπ ) β€ (πΉβπ‘)) β βπ₯ β ran πΉβπ‘ β π π₯ β€ (πΉβπ‘)) |
26 | 18, 25 | sylan 581 |
. . . . 5
β’ (((π β§ π β π) β§ βπ‘ β π (πΉβπ ) β€ (πΉβπ‘)) β βπ₯ β ran πΉβπ‘ β π π₯ β€ (πΉβπ‘)) |
27 | | nfcv 2908 |
. . . . . 6
β’
β²π πΉ |
28 | | nfcv 2908 |
. . . . . 6
β’
β²π π |
29 | | nfcv 2908 |
. . . . . 6
β’
β²π‘π |
30 | | stoweidlem29.5 |
. . . . . 6
β’ (π β π½ β Comp) |
31 | | stoweidlem29.7 |
. . . . . 6
β’ (π β π β β
) |
32 | 27, 19, 28, 29, 2, 1, 30, 4, 31 | evth2f 43227 |
. . . . 5
β’ (π β βπ β π βπ‘ β π (πΉβπ ) β€ (πΉβπ‘)) |
33 | 26, 32 | r19.29a 3160 |
. . . 4
β’ (π β βπ₯ β ran πΉβπ‘ β π π₯ β€ (πΉβπ‘)) |
34 | | nfv 1918 |
. . . . . . 7
β’
β²π¦(π β§ βπ‘ β π π₯ β€ (πΉβπ‘)) |
35 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ βπ‘ β π π₯ β€ (πΉβπ‘)) β§ π¦ β ran πΉ) β π¦ β ran πΉ) |
36 | 9 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ βπ‘ β π π₯ β€ (πΉβπ‘)) β§ π¦ β ran πΉ) β πΉ Fn π) |
37 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π‘π¦ |
38 | 29, 37, 19 | fvelrnbf 43230 |
. . . . . . . . . . 11
β’ (πΉ Fn π β (π¦ β ran πΉ β βπ‘ β π (πΉβπ‘) = π¦)) |
39 | 36, 38 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ βπ‘ β π π₯ β€ (πΉβπ‘)) β§ π¦ β ran πΉ) β (π¦ β ran πΉ β βπ‘ β π (πΉβπ‘) = π¦)) |
40 | 35, 39 | mpbid 231 |
. . . . . . . . 9
β’ (((π β§ βπ‘ β π π₯ β€ (πΉβπ‘)) β§ π¦ β ran πΉ) β βπ‘ β π (πΉβπ‘) = π¦) |
41 | | stoweidlem29.2 |
. . . . . . . . . . . 12
β’
β²π‘π |
42 | | nfra1 3268 |
. . . . . . . . . . . 12
β’
β²π‘βπ‘ β π π₯ β€ (πΉβπ‘) |
43 | 41, 42 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π‘(π β§ βπ‘ β π π₯ β€ (πΉβπ‘)) |
44 | 19 | nfrn 5908 |
. . . . . . . . . . . 12
β’
β²π‘ran
πΉ |
45 | 44 | nfcri 2895 |
. . . . . . . . . . 11
β’
β²π‘ π¦ β ran πΉ |
46 | 43, 45 | nfan 1903 |
. . . . . . . . . 10
β’
β²π‘((π β§ βπ‘ β π π₯ β€ (πΉβπ‘)) β§ π¦ β ran πΉ) |
47 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π‘ π₯ β€ π¦ |
48 | | rspa 3232 |
. . . . . . . . . . . . 13
β’
((βπ‘ β
π π₯ β€ (πΉβπ‘) β§ π‘ β π) β π₯ β€ (πΉβπ‘)) |
49 | | breq2 5110 |
. . . . . . . . . . . . 13
β’ ((πΉβπ‘) = π¦ β (π₯ β€ (πΉβπ‘) β π₯ β€ π¦)) |
50 | 48, 49 | syl5ibcom 244 |
. . . . . . . . . . . 12
β’
((βπ‘ β
π π₯ β€ (πΉβπ‘) β§ π‘ β π) β ((πΉβπ‘) = π¦ β π₯ β€ π¦)) |
51 | 50 | ex 414 |
. . . . . . . . . . 11
β’
(βπ‘ β
π π₯ β€ (πΉβπ‘) β (π‘ β π β ((πΉβπ‘) = π¦ β π₯ β€ π¦))) |
52 | 51 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ βπ‘ β π π₯ β€ (πΉβπ‘)) β§ π¦ β ran πΉ) β (π‘ β π β ((πΉβπ‘) = π¦ β π₯ β€ π¦))) |
53 | 46, 47, 52 | rexlimd 3250 |
. . . . . . . . 9
β’ (((π β§ βπ‘ β π π₯ β€ (πΉβπ‘)) β§ π¦ β ran πΉ) β (βπ‘ β π (πΉβπ‘) = π¦ β π₯ β€ π¦)) |
54 | 40, 53 | mpd 15 |
. . . . . . . 8
β’ (((π β§ βπ‘ β π π₯ β€ (πΉβπ‘)) β§ π¦ β ran πΉ) β π₯ β€ π¦) |
55 | 54 | ex 414 |
. . . . . . 7
β’ ((π β§ βπ‘ β π π₯ β€ (πΉβπ‘)) β (π¦ β ran πΉ β π₯ β€ π¦)) |
56 | 34, 55 | ralrimi 3241 |
. . . . . 6
β’ ((π β§ βπ‘ β π π₯ β€ (πΉβπ‘)) β βπ¦ β ran πΉ π₯ β€ π¦) |
57 | 56 | ex 414 |
. . . . 5
β’ (π β (βπ‘ β π π₯ β€ (πΉβπ‘) β βπ¦ β ran πΉ π₯ β€ π¦)) |
58 | 57 | reximdv 3168 |
. . . 4
β’ (π β (βπ₯ β ran πΉβπ‘ β π π₯ β€ (πΉβπ‘) β βπ₯ β ran πΉβπ¦ β ran πΉ π₯ β€ π¦)) |
59 | 33, 58 | mpd 15 |
. . 3
β’ (π β βπ₯ β ran πΉβπ¦ β ran πΉ π₯ β€ π¦) |
60 | | lbinfcl 12110 |
. . 3
β’ ((ran
πΉ β β β§
βπ₯ β ran πΉβπ¦ β ran πΉ π₯ β€ π¦) β inf(ran πΉ, β, < ) β ran πΉ) |
61 | 8, 59, 60 | syl2anc 585 |
. 2
β’ (π β inf(ran πΉ, β, < ) β ran πΉ) |
62 | 8, 61 | sseldd 3946 |
. 2
β’ (π β inf(ran πΉ, β, < ) β
β) |
63 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ π‘ β π) β ran πΉ β β) |
64 | 59 | adantr 482 |
. . . . 5
β’ ((π β§ π‘ β π) β βπ₯ β ran πΉβπ¦ β ran πΉ π₯ β€ π¦) |
65 | | dffn3 6682 |
. . . . . . 7
β’ (πΉ Fn π β πΉ:πβΆran πΉ) |
66 | 9, 65 | sylib 217 |
. . . . . 6
β’ (π β πΉ:πβΆran πΉ) |
67 | 66 | ffvelcdmda 7036 |
. . . . 5
β’ ((π β§ π‘ β π) β (πΉβπ‘) β ran πΉ) |
68 | | lbinfle 12111 |
. . . . 5
β’ ((ran
πΉ β β β§
βπ₯ β ran πΉβπ¦ β ran πΉ π₯ β€ π¦ β§ (πΉβπ‘) β ran πΉ) β inf(ran πΉ, β, < ) β€ (πΉβπ‘)) |
69 | 63, 64, 67, 68 | syl3anc 1372 |
. . . 4
β’ ((π β§ π‘ β π) β inf(ran πΉ, β, < ) β€ (πΉβπ‘)) |
70 | 69 | ex 414 |
. . 3
β’ (π β (π‘ β π β inf(ran πΉ, β, < ) β€ (πΉβπ‘))) |
71 | 41, 70 | ralrimi 3241 |
. 2
β’ (π β βπ‘ β π inf(ran πΉ, β, < ) β€ (πΉβπ‘)) |
72 | 61, 62, 71 | 3jca 1129 |
1
β’ (π β (inf(ran πΉ, β, < ) β ran πΉ β§ inf(ran πΉ, β, < ) β β β§
βπ‘ β π inf(ran πΉ, β, < ) β€ (πΉβπ‘))) |