Step | Hyp | Ref
| Expression |
1 | | ordom 7074 |
. . . 4
|
2 | | ordwe 5736 |
. . . 4
|
3 | | weso 5105 |
. . . 4
|
4 | 1, 2, 3 | mp2b 10 |
. . 3
|
5 | 4 | a1i 11 |
. 2
|
6 | | sopo 5052 |
. . . . 5
|
7 | 4, 6 | ax-mp 5 |
. . . 4
|
8 | | poss 5037 |
. . . 4
|
9 | 7, 8 | mpi 20 |
. . 3
|
10 | 9 | adantr 481 |
. 2
|
11 | | fin23lem22.b |
. . . 4
|
12 | 11 | fin23lem22 9149 |
. . 3
|
13 | | f1ofo 6144 |
. . 3
|
14 | 12, 13 | syl 17 |
. 2
|
15 | | nnsdomel 8816 |
. . . . . . . 8
|
16 | 15 | adantl 482 |
. . . . . . 7
|
17 | 16 | biimpd 219 |
. . . . . 6
|
18 | | fin23lem23 9148 |
. . . . . . . . . . . . 13
|
19 | 18 | adantrr 753 |
. . . . . . . . . . . 12
|
20 | | ineq1 3807 |
. . . . . . . . . . . . . 14
|
21 | 20 | breq1d 4663 |
. . . . . . . . . . . . 13
|
22 | 21 | cbvreuv 3173 |
. . . . . . . . . . . 12
|
23 | 19, 22 | sylib 208 |
. . . . . . . . . . 11
|
24 | | nfv 1843 |
. . . . . . . . . . . 12
|
25 | 21 | cbvriotav 6622 |
. . . . . . . . . . . 12
|
26 | | ineq1 3807 |
. . . . . . . . . . . . 13
|
27 | 26 | breq1d 4663 |
. . . . . . . . . . . 12
|
28 | 24, 25, 27 | riotaprop 6635 |
. . . . . . . . . . 11
|
29 | 23, 28 | syl 17 |
. . . . . . . . . 10
|
30 | 29 | simprd 479 |
. . . . . . . . 9
|
31 | 30 | adantrr 753 |
. . . . . . . 8
|
32 | | simprr 796 |
. . . . . . . . 9
|
33 | | fin23lem23 9148 |
. . . . . . . . . . . . . . 15
|
34 | 33 | adantrl 752 |
. . . . . . . . . . . . . 14
|
35 | 20 | breq1d 4663 |
. . . . . . . . . . . . . . 15
|
36 | 35 | cbvreuv 3173 |
. . . . . . . . . . . . . 14
|
37 | 34, 36 | sylib 208 |
. . . . . . . . . . . . 13
|
38 | | nfv 1843 |
. . . . . . . . . . . . . 14
|
39 | 35 | cbvriotav 6622 |
. . . . . . . . . . . . . 14
|
40 | | ineq1 3807 |
. . . . . . . . . . . . . . 15
|
41 | 40 | breq1d 4663 |
. . . . . . . . . . . . . 14
|
42 | 38, 39, 41 | riotaprop 6635 |
. . . . . . . . . . . . 13
|
43 | 37, 42 | syl 17 |
. . . . . . . . . . . 12
|
44 | 43 | simprd 479 |
. . . . . . . . . . 11
|
45 | 44 | ensymd 8007 |
. . . . . . . . . 10
|
46 | 45 | adantrr 753 |
. . . . . . . . 9
|
47 | | sdomentr 8094 |
. . . . . . . . 9
|
48 | 32, 46, 47 | syl2anc 693 |
. . . . . . . 8
|
49 | | ensdomtr 8096 |
. . . . . . . 8
|
50 | 31, 48, 49 | syl2anc 693 |
. . . . . . 7
|
51 | 50 | expr 643 |
. . . . . 6
|
52 | | simpll 790 |
. . . . . . . . 9
|
53 | | omsson 7069 |
. . . . . . . . 9
|
54 | 52, 53 | syl6ss 3615 |
. . . . . . . 8
|
55 | 29 | simpld 475 |
. . . . . . . 8
|
56 | 54, 55 | sseldd 3604 |
. . . . . . 7
|
57 | 43 | simpld 475 |
. . . . . . . 8
|
58 | 54, 57 | sseldd 3604 |
. . . . . . 7
|
59 | | onsdominel 8109 |
. . . . . . . 8
|
60 | 59 | 3expia 1267 |
. . . . . . 7
|
61 | 56, 58, 60 | syl2anc 693 |
. . . . . 6
|
62 | 17, 51, 61 | 3syld 60 |
. . . . 5
|
63 | | simprl 794 |
. . . . . . 7
|
64 | | breq2 4657 |
. . . . . . . . 9
|
65 | 64 | riotabidv 6613 |
. . . . . . . 8
|
66 | 65, 11 | fvmptg 6280 |
. . . . . . 7
|
67 | 63, 55, 66 | syl2anc 693 |
. . . . . 6
|
68 | | simprr 796 |
. . . . . . 7
|
69 | | breq2 4657 |
. . . . . . . . 9
|
70 | 69 | riotabidv 6613 |
. . . . . . . 8
|
71 | 70, 11 | fvmptg 6280 |
. . . . . . 7
|
72 | 68, 57, 71 | syl2anc 693 |
. . . . . 6
|
73 | 67, 72 | eleq12d 2695 |
. . . . 5
|
74 | 62, 73 | sylibrd 249 |
. . . 4
|
75 | | epel 5032 |
. . . 4
|
76 | | fvex 6201 |
. . . . 5
|
77 | 76 | epelc 5031 |
. . . 4
|
78 | 74, 75, 77 | 3imtr4g 285 |
. . 3
|
79 | 78 | ralrimivva 2971 |
. 2
|
80 | | soisoi 6578 |
. 2
|
81 | 5, 10, 14, 79, 80 | syl22anc 1327 |
1
|