Step | Hyp | Ref
| Expression |
1 | | nfcv 2904 |
. . . . . . . 8
β’
β²π πΉ |
2 | | rfcnnnub.1 |
. . . . . . . 8
β’
β²π‘πΉ |
3 | | nfcv 2904 |
. . . . . . . 8
β’
β²π π |
4 | | nfcv 2904 |
. . . . . . . 8
β’
β²π‘π |
5 | | nfv 1918 |
. . . . . . . 8
β’
β²π π |
6 | | rfcnnnub.2 |
. . . . . . . 8
β’
β²π‘π |
7 | | rfcnnnub.5 |
. . . . . . . 8
β’ π = βͺ
π½ |
8 | | rfcnnnub.3 |
. . . . . . . 8
β’ πΎ = (topGenβran
(,)) |
9 | | rfcnnnub.4 |
. . . . . . . 8
β’ (π β π½ β Comp) |
10 | | rfcnnnub.8 |
. . . . . . . . 9
β’ (π β πΉ β πΆ) |
11 | | rfcnnnub.7 |
. . . . . . . . 9
β’ πΆ = (π½ Cn πΎ) |
12 | 10, 11 | eleqtrdi 2844 |
. . . . . . . 8
β’ (π β πΉ β (π½ Cn πΎ)) |
13 | | rfcnnnub.6 |
. . . . . . . 8
β’ (π β π β β
) |
14 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 12,
13 | evthf 43711 |
. . . . . . 7
β’ (π β βπ β π βπ‘ β π (πΉβπ‘) β€ (πΉβπ )) |
15 | | df-rex 3072 |
. . . . . . 7
β’
(βπ β
π βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β βπ (π β π β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ ))) |
16 | 14, 15 | sylib 217 |
. . . . . 6
β’ (π β βπ (π β π β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ ))) |
17 | 8, 7, 11, 10 | fcnre 43709 |
. . . . . . . . . 10
β’ (π β πΉ:πβΆβ) |
18 | 17 | ffvelcdmda 7087 |
. . . . . . . . 9
β’ ((π β§ π β π) β (πΉβπ ) β β) |
19 | 18 | ex 414 |
. . . . . . . 8
β’ (π β (π β π β (πΉβπ ) β β)) |
20 | 19 | anim1d 612 |
. . . . . . 7
β’ (π β ((π β π β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ )) β ((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ )))) |
21 | 20 | eximdv 1921 |
. . . . . 6
β’ (π β (βπ (π β π β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ )) β βπ ((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ )))) |
22 | 16, 21 | mpd 15 |
. . . . 5
β’ (π β βπ ((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ ))) |
23 | 17 | ffvelcdmda 7087 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (πΉβπ‘) β β) |
24 | 23 | ex 414 |
. . . . . 6
β’ (π β (π‘ β π β (πΉβπ‘) β β)) |
25 | 6, 24 | ralrimi 3255 |
. . . . 5
β’ (π β βπ‘ β π (πΉβπ‘) β β) |
26 | | 19.41v 1954 |
. . . . 5
β’
(βπ (((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ )) β§ βπ‘ β π (πΉβπ‘) β β) β (βπ ((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ )) β§ βπ‘ β π (πΉβπ‘) β β)) |
27 | 22, 25, 26 | sylanbrc 584 |
. . . 4
β’ (π β βπ (((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ )) β§ βπ‘ β π (πΉβπ‘) β β)) |
28 | | df-3an 1090 |
. . . . 5
β’ (((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β (((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ )) β§ βπ‘ β π (πΉβπ‘) β β)) |
29 | 28 | exbii 1851 |
. . . 4
β’
(βπ ((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β βπ (((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ )) β§ βπ‘ β π (πΉβπ‘) β β)) |
30 | 27, 29 | sylibr 233 |
. . 3
β’ (π β βπ ((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β)) |
31 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π‘π |
32 | 2, 31 | nffv 6902 |
. . . . . . . . 9
β’
β²π‘(πΉβπ ) |
33 | 32 | nfel1 2920 |
. . . . . . . 8
β’
β²π‘(πΉβπ ) β β |
34 | | nfra1 3282 |
. . . . . . . 8
β’
β²π‘βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) |
35 | | nfra1 3282 |
. . . . . . . 8
β’
β²π‘βπ‘ β π (πΉβπ‘) β β |
36 | 33, 34, 35 | nf3an 1905 |
. . . . . . 7
β’
β²π‘((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) |
37 | | nfv 1918 |
. . . . . . . 8
β’
β²π‘ π β β |
38 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π‘
< |
39 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π‘π |
40 | 32, 38, 39 | nfbr 5196 |
. . . . . . . 8
β’
β²π‘(πΉβπ ) < π |
41 | 37, 40 | nfan 1903 |
. . . . . . 7
β’
β²π‘(π β β β§ (πΉβπ ) < π) |
42 | 36, 41 | nfan 1903 |
. . . . . 6
β’
β²π‘(((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β§ (π β β β§ (πΉβπ ) < π)) |
43 | | simpll3 1215 |
. . . . . . . . 9
β’
(((((πΉβπ ) β β β§
βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β§ (π β β β§ (πΉβπ ) < π)) β§ π‘ β π) β βπ‘ β π (πΉβπ‘) β β) |
44 | | simpr 486 |
. . . . . . . . 9
β’
(((((πΉβπ ) β β β§
βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β§ (π β β β§ (πΉβπ ) < π)) β§ π‘ β π) β π‘ β π) |
45 | | rsp 3245 |
. . . . . . . . 9
β’
(βπ‘ β
π (πΉβπ‘) β β β (π‘ β π β (πΉβπ‘) β β)) |
46 | 43, 44, 45 | sylc 65 |
. . . . . . . 8
β’
(((((πΉβπ ) β β β§
βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β§ (π β β β§ (πΉβπ ) < π)) β§ π‘ β π) β (πΉβπ‘) β β) |
47 | | simpll1 1213 |
. . . . . . . 8
β’
(((((πΉβπ ) β β β§
βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β§ (π β β β§ (πΉβπ ) < π)) β§ π‘ β π) β (πΉβπ ) β β) |
48 | | simplrl 776 |
. . . . . . . . 9
β’
(((((πΉβπ ) β β β§
βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β§ (π β β β§ (πΉβπ ) < π)) β§ π‘ β π) β π β β) |
49 | 48 | nnred 12227 |
. . . . . . . 8
β’
(((((πΉβπ ) β β β§
βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β§ (π β β β§ (πΉβπ ) < π)) β§ π‘ β π) β π β β) |
50 | | simpl2 1193 |
. . . . . . . . 9
β’ ((((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β§ (π β β β§ (πΉβπ ) < π)) β βπ‘ β π (πΉβπ‘) β€ (πΉβπ )) |
51 | 50 | r19.21bi 3249 |
. . . . . . . 8
β’
(((((πΉβπ ) β β β§
βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β§ (π β β β§ (πΉβπ ) < π)) β§ π‘ β π) β (πΉβπ‘) β€ (πΉβπ )) |
52 | | simplrr 777 |
. . . . . . . 8
β’
(((((πΉβπ ) β β β§
βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β§ (π β β β§ (πΉβπ ) < π)) β§ π‘ β π) β (πΉβπ ) < π) |
53 | 46, 47, 49, 51, 52 | lelttrd 11372 |
. . . . . . 7
β’
(((((πΉβπ ) β β β§
βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β§ (π β β β§ (πΉβπ ) < π)) β§ π‘ β π) β (πΉβπ‘) < π) |
54 | 53 | ex 414 |
. . . . . 6
β’ ((((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β§ (π β β β§ (πΉβπ ) < π)) β (π‘ β π β (πΉβπ‘) < π)) |
55 | 42, 54 | ralrimi 3255 |
. . . . 5
β’ ((((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β§ (π β β β§ (πΉβπ ) < π)) β βπ‘ β π (πΉβπ‘) < π) |
56 | | arch 12469 |
. . . . . 6
β’ ((πΉβπ ) β β β βπ β β (πΉβπ ) < π) |
57 | 56 | 3ad2ant1 1134 |
. . . . 5
β’ (((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β βπ β β (πΉβπ ) < π) |
58 | 55, 57 | reximddv 3172 |
. . . 4
β’ (((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β βπ β β βπ‘ β π (πΉβπ‘) < π) |
59 | 58 | eximi 1838 |
. . 3
β’
(βπ ((πΉβπ ) β β β§ βπ‘ β π (πΉβπ‘) β€ (πΉβπ ) β§ βπ‘ β π (πΉβπ‘) β β) β βπ βπ β β βπ‘ β π (πΉβπ‘) < π) |
60 | 30, 59 | syl 17 |
. 2
β’ (π β βπ βπ β β βπ‘ β π (πΉβπ‘) < π) |
61 | | 19.9v 1988 |
. 2
β’
(βπ βπ β β βπ‘ β π (πΉβπ‘) < π β βπ β β βπ‘ β π (πΉβπ‘) < π) |
62 | 60, 61 | sylib 217 |
1
β’ (π β βπ β β βπ‘ β π (πΉβπ‘) < π) |