Proof of Theorem cnfcom2lem
Step | Hyp | Ref
| Expression |
1 | | cnfcom2.1 |
. . . . . 6
|
2 | | n0i 3920 |
. . . . . 6
|
3 | 1, 2 | syl 17 |
. . . . 5
|
4 | | cnfcom.f |
. . . . . . . . . . . . . 14
CNF |
5 | | cnfcom.s |
. . . . . . . . . . . . . . . . 17
CNF |
6 | | omelon 8543 |
. . . . . . . . . . . . . . . . . 18
|
7 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
8 | | cnfcom.a |
. . . . . . . . . . . . . . . . 17
|
9 | 5, 7, 8 | cantnff1o 8593 |
. . . . . . . . . . . . . . . 16
CNF
|
10 | | f1ocnv 6149 |
. . . . . . . . . . . . . . . 16
CNF
CNF |
11 | | f1of 6137 |
. . . . . . . . . . . . . . . 16
CNF
CNF |
12 | 9, 10, 11 | 3syl 18 |
. . . . . . . . . . . . . . 15
CNF |
13 | | cnfcom.b |
. . . . . . . . . . . . . . 15
|
14 | 12, 13 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
CNF |
15 | 4, 14 | syl5eqel 2705 |
. . . . . . . . . . . . 13
|
16 | 5, 7, 8 | cantnfs 8563 |
. . . . . . . . . . . . 13
finSupp |
17 | 15, 16 | mpbid 222 |
. . . . . . . . . . . 12
finSupp
|
18 | 17 | simpld 475 |
. . . . . . . . . . 11
|
19 | 18 | adantr 481 |
. . . . . . . . . 10
|
20 | 19 | feqmptd 6249 |
. . . . . . . . 9
|
21 | | dif0 3950 |
. . . . . . . . . . . 12
|
22 | 21 | eleq2i 2693 |
. . . . . . . . . . 11
|
23 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
24 | | suppssdm 7308 |
. . . . . . . . . . . . . . . . . . . 20
supp
|
25 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . 21
|
26 | 18, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
27 | 24, 26 | syl5sseq 3653 |
. . . . . . . . . . . . . . . . . . 19
supp |
28 | 8, 27 | ssexd 4805 |
. . . . . . . . . . . . . . . . . 18
supp |
29 | | cnfcom.g |
. . . . . . . . . . . . . . . . . . . 20
OrdIso supp |
30 | 5, 7, 8, 29, 15 | cantnfcl 8564 |
. . . . . . . . . . . . . . . . . . 19
supp |
31 | 30 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
supp |
32 | 29 | oien 8443 |
. . . . . . . . . . . . . . . . . 18
supp
supp
supp |
33 | 28, 31, 32 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
supp |
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . . 16
supp |
35 | 23, 34 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . 15
supp |
36 | 35 | ensymd 8007 |
. . . . . . . . . . . . . 14
supp
|
37 | | en0 8019 |
. . . . . . . . . . . . . 14
supp
supp |
38 | 36, 37 | sylib 208 |
. . . . . . . . . . . . 13
supp
|
39 | | ss0b 3973 |
. . . . . . . . . . . . 13
supp
supp |
40 | 38, 39 | sylibr 224 |
. . . . . . . . . . . 12
supp
|
41 | 8 | adantr 481 |
. . . . . . . . . . . 12
|
42 | | 0ex 4790 |
. . . . . . . . . . . . 13
|
43 | 42 | a1i 11 |
. . . . . . . . . . . 12
|
44 | 19, 40, 41, 43 | suppssr 7326 |
. . . . . . . . . . 11
|
45 | 22, 44 | sylan2br 493 |
. . . . . . . . . 10
|
46 | 45 | mpteq2dva 4744 |
. . . . . . . . 9
|
47 | 20, 46 | eqtrd 2656 |
. . . . . . . 8
|
48 | | fconstmpt 5163 |
. . . . . . . 8
|
49 | 47, 48 | syl6eqr 2674 |
. . . . . . 7
|
50 | 49 | fveq2d 6195 |
. . . . . 6
CNF CNF
|
51 | 4 | fveq2i 6194 |
. . . . . . . 8
CNF CNF
CNF |
52 | | f1ocnvfv2 6533 |
. . . . . . . . 9
CNF
CNF CNF |
53 | 9, 13, 52 | syl2anc 693 |
. . . . . . . 8
CNF CNF |
54 | 51, 53 | syl5eq 2668 |
. . . . . . 7
CNF |
55 | 54 | adantr 481 |
. . . . . 6
CNF |
56 | | peano1 7085 |
. . . . . . . . 9
|
57 | 56 | a1i 11 |
. . . . . . . 8
|
58 | 5, 7, 8, 57 | cantnf0 8572 |
. . . . . . 7
CNF |
59 | 58 | adantr 481 |
. . . . . 6
CNF
|
60 | 50, 55, 59 | 3eqtr3d 2664 |
. . . . 5
|
61 | 3, 60 | mtand 691 |
. . . 4
|
62 | 30 | simprd 479 |
. . . . 5
|
63 | | nnlim 7078 |
. . . . 5
|
64 | 62, 63 | syl 17 |
. . . 4
|
65 | | ioran 511 |
. . . 4
|
66 | 61, 64, 65 | sylanbrc 698 |
. . 3
|
67 | 29 | oicl 8434 |
. . . 4
|
68 | | unizlim 5844 |
. . . 4
|
69 | 67, 68 | ax-mp 5 |
. . 3
|
70 | 66, 69 | sylnibr 319 |
. 2
|
71 | | orduniorsuc 7030 |
. . . 4
|
72 | 67, 71 | mp1i 13 |
. . 3
|
73 | 72 | ord 392 |
. 2
|
74 | 70, 73 | mpd 15 |
1
|