Proof of Theorem cantnflem1b
Step | Hyp | Ref
| Expression |
1 | | simprr 796 |
. . . 4
|
2 | | cantnflem1.o |
. . . . . . . 8
OrdIso supp |
3 | 2 | oicl 8434 |
. . . . . . 7
|
4 | | cantnfs.b |
. . . . . . . . . . . 12
|
5 | | suppssdm 7308 |
. . . . . . . . . . . . 13
supp
|
6 | | oemapval.g |
. . . . . . . . . . . . . . . 16
|
7 | | cantnfs.s |
. . . . . . . . . . . . . . . . 17
CNF |
8 | | cantnfs.a |
. . . . . . . . . . . . . . . . 17
|
9 | 7, 8, 4 | cantnfs 8563 |
. . . . . . . . . . . . . . . 16
finSupp |
10 | 6, 9 | mpbid 222 |
. . . . . . . . . . . . . . 15
finSupp
|
11 | 10 | simpld 475 |
. . . . . . . . . . . . . 14
|
12 | | fdm 6051 |
. . . . . . . . . . . . . 14
|
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . 13
|
14 | 5, 13 | syl5sseq 3653 |
. . . . . . . . . . . 12
supp |
15 | 4, 14 | ssexd 4805 |
. . . . . . . . . . 11
supp |
16 | 7, 8, 4, 2, 6 | cantnfcl 8564 |
. . . . . . . . . . . 12
supp |
17 | 16 | simpld 475 |
. . . . . . . . . . 11
supp |
18 | 2 | oiiso 8442 |
. . . . . . . . . . 11
supp
supp supp
|
19 | 15, 17, 18 | syl2anc 693 |
. . . . . . . . . 10
supp |
20 | | isof1o 6573 |
. . . . . . . . . 10
supp supp |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
supp |
22 | | f1ocnv 6149 |
. . . . . . . . 9
supp
supp |
23 | | f1of 6137 |
. . . . . . . . 9
supp supp |
24 | 21, 22, 23 | 3syl 18 |
. . . . . . . 8
supp
|
25 | | oemapval.t |
. . . . . . . . 9
|
26 | | oemapval.f |
. . . . . . . . 9
|
27 | | oemapvali.r |
. . . . . . . . 9
|
28 | | oemapvali.x |
. . . . . . . . 9
|
29 | 7, 8, 4, 25, 26, 6, 27, 28 | cantnflem1a 8582 |
. . . . . . . 8
supp |
30 | 24, 29 | ffvelrnd 6360 |
. . . . . . 7
|
31 | | ordelon 5747 |
. . . . . . 7
|
32 | 3, 30, 31 | sylancr 695 |
. . . . . 6
|
33 | 32 | adantr 481 |
. . . . 5
|
34 | 3 | a1i 11 |
. . . . . . . 8
|
35 | | ordelon 5747 |
. . . . . . . 8
|
36 | 34, 35 | sylan 488 |
. . . . . . 7
|
37 | | sucelon 7017 |
. . . . . . 7
|
38 | 36, 37 | sylibr 224 |
. . . . . 6
|
39 | 38 | adantrr 753 |
. . . . 5
|
40 | | ontri1 5757 |
. . . . 5
|
41 | 33, 39, 40 | syl2anc 693 |
. . . 4
|
42 | 1, 41 | mpbid 222 |
. . 3
|
43 | 19 | adantr 481 |
. . . . . 6
supp
|
44 | | ordtr 5737 |
. . . . . . . 8
|
45 | 3, 44 | mp1i 13 |
. . . . . . 7
|
46 | | simprl 794 |
. . . . . . 7
|
47 | | trsuc 5810 |
. . . . . . 7
|
48 | 45, 46, 47 | syl2anc 693 |
. . . . . 6
|
49 | 30 | adantr 481 |
. . . . . 6
|
50 | | isorel 6576 |
. . . . . 6
supp
|
51 | 43, 48, 49, 50 | syl12anc 1324 |
. . . . 5
|
52 | | fvex 6201 |
. . . . . 6
|
53 | 52 | epelc 5031 |
. . . . 5
|
54 | | fvex 6201 |
. . . . . 6
|
55 | 54 | epelc 5031 |
. . . . 5
|
56 | 51, 53, 55 | 3bitr3g 302 |
. . . 4
|
57 | | f1ocnvfv2 6533 |
. . . . . . 7
supp supp |
58 | 21, 29, 57 | syl2anc 693 |
. . . . . 6
|
59 | 58 | adantr 481 |
. . . . 5
|
60 | 59 | eleq2d 2687 |
. . . 4
|
61 | 56, 60 | bitrd 268 |
. . 3
|
62 | 42, 61 | mtbid 314 |
. 2
|
63 | 7, 8, 4, 25, 26, 6, 27, 28 | oemapvali 8581 |
. . . . . 6
|
64 | 63 | simp1d 1073 |
. . . . 5
|
65 | | onelon 5748 |
. . . . 5
|
66 | 4, 64, 65 | syl2anc 693 |
. . . 4
|
67 | 66 | adantr 481 |
. . 3
|
68 | 4 | adantr 481 |
. . . 4
|
69 | 14 | adantr 481 |
. . . . 5
supp |
70 | 2 | oif 8435 |
. . . . . . 7
supp |
71 | 70 | ffvelrni 6358 |
. . . . . 6
supp |
72 | 48, 71 | syl 17 |
. . . . 5
supp |
73 | 69, 72 | sseldd 3604 |
. . . 4
|
74 | | onelon 5748 |
. . . 4
|
75 | 68, 73, 74 | syl2anc 693 |
. . 3
|
76 | | ontri1 5757 |
. . 3
|
77 | 67, 75, 76 | syl2anc 693 |
. 2
|
78 | 62, 77 | mpbird 247 |
1
|