Step | Hyp | Ref
| Expression |
1 | | cantnfs.s |
. . 3
CNF |
2 | | cantnfs.a |
. . 3
|
3 | | cantnfs.b |
. . 3
|
4 | | oemapval.t |
. . 3
|
5 | 1, 2, 3, 4 | oemapso 8579 |
. 2
|
6 | | oecl 7617 |
. . . . 5
|
7 | 2, 3, 6 | syl2anc 693 |
. . . 4
|
8 | | eloni 5733 |
. . . 4
|
9 | 7, 8 | syl 17 |
. . 3
|
10 | | ordwe 5736 |
. . 3
|
11 | | weso 5105 |
. . 3
|
12 | | sopo 5052 |
. . 3
|
13 | 9, 10, 11, 12 | 4syl 19 |
. 2
|
14 | 1, 2, 3 | cantnff 8571 |
. . 3
CNF |
15 | | frn 6053 |
. . . . 5
CNF
CNF |
16 | 14, 15 | syl 17 |
. . . 4
CNF
|
17 | | onss 6990 |
. . . . . . . 8
|
18 | 7, 17 | syl 17 |
. . . . . . 7
|
19 | 18 | sseld 3602 |
. . . . . 6
|
20 | | eleq1 2689 |
. . . . . . . . . 10
|
21 | | eleq1 2689 |
. . . . . . . . . 10
CNF
CNF |
22 | 20, 21 | imbi12d 334 |
. . . . . . . . 9
CNF
CNF |
23 | 22 | imbi2d 330 |
. . . . . . . 8
CNF
CNF |
24 | | r19.21v 2960 |
. . . . . . . . 9
CNF
CNF |
25 | | ordelss 5739 |
. . . . . . . . . . . . . . . . . . 19
|
26 | 9, 25 | sylan 488 |
. . . . . . . . . . . . . . . . . 18
|
27 | 26 | sselda 3603 |
. . . . . . . . . . . . . . . . 17
|
28 | | pm5.5 351 |
. . . . . . . . . . . . . . . . 17
CNF
CNF |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . 16
CNF
CNF |
30 | 29 | ralbidva 2985 |
. . . . . . . . . . . . . . 15
CNF
CNF |
31 | | dfss3 3592 |
. . . . . . . . . . . . . . 15
CNF CNF |
32 | 30, 31 | syl6bbr 278 |
. . . . . . . . . . . . . 14
CNF
CNF |
33 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
CNF
CNF |
34 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
CNF |
35 | 34 | adantr 481 |
. . . . . . . . . . . . . . . . 17
CNF
|
36 | 3 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
CNF |
37 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . 17
CNF
|
38 | | simplrl 800 |
. . . . . . . . . . . . . . . . 17
CNF |
39 | | simplrr 801 |
. . . . . . . . . . . . . . . . 17
CNF
CNF |
40 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
CNF |
41 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . 20
CNF |
42 | | onelon 5748 |
. . . . . . . . . . . . . . . . . . . 20
|
43 | 40, 41, 42 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
CNF |
44 | | on0eln0 5780 |
. . . . . . . . . . . . . . . . . . 19
|
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
CNF
|
46 | 45 | biimpar 502 |
. . . . . . . . . . . . . . . . 17
CNF |
47 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
48 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
49 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
50 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
51 | 1, 35, 37, 4, 38, 39, 46, 47, 48, 49, 50 | cantnflem4 8589 |
. . . . . . . . . . . . . . . 16
CNF CNF |
52 | | fczsupp0 7324 |
. . . . . . . . . . . . . . . . . . . . 21
supp |
53 | 52 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . . 20
supp |
54 | | oieq2 8418 |
. . . . . . . . . . . . . . . . . . . 20
supp
OrdIso OrdIso supp |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
OrdIso OrdIso supp |
56 | | ne0i 3921 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
57 | | ne0i 3921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
58 | 57 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
CNF |
59 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
60 | 59 | neeq1d 2853 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
61 | 58, 60 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
CNF
|
62 | 61 | necon2d 2817 |
. . . . . . . . . . . . . . . . . . . . . . . 24
CNF
|
63 | | on0eln0 5780 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
64 | | oe0m1 7601 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
65 | 63, 64 | bitr3d 270 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
66 | 36, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
CNF |
67 | | on0eln0 5780 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
68 | 34, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
CNF
|
69 | 62, 66, 68 | 3imtr4d 283 |
. . . . . . . . . . . . . . . . . . . . . . 23
CNF
|
70 | 56, 69 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . 22
CNF |
71 | 70 | imp 445 |
. . . . . . . . . . . . . . . . . . . . 21
CNF
|
72 | | fconstmpt 5163 |
. . . . . . . . . . . . . . . . . . . . 21
|
73 | 71, 72 | fmptd 6385 |
. . . . . . . . . . . . . . . . . . . 20
CNF |
74 | | 0ex 4790 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
76 | 3, 75 | fczfsuppd 8293 |
. . . . . . . . . . . . . . . . . . . . 21
finSupp
|
77 | 76 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
CNF finSupp |
78 | 1, 2, 3 | cantnfs 8563 |
. . . . . . . . . . . . . . . . . . . . 21
finSupp |
79 | 78 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
CNF finSupp |
80 | 73, 77, 79 | mpbir2and 957 |
. . . . . . . . . . . . . . . . . . 19
CNF |
81 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
seq𝜔 OrdIso OrdIso
seq𝜔 OrdIso OrdIso |
82 | 1, 34, 36, 55, 80, 81 | cantnfval 8565 |
. . . . . . . . . . . . . . . . . 18
CNF CNF seq𝜔 OrdIso OrdIso
OrdIso |
83 | | we0 5109 |
. . . . . . . . . . . . . . . . . . . . . 22
|
84 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
OrdIso OrdIso |
85 | 84 | oien 8443 |
. . . . . . . . . . . . . . . . . . . . . 22
OrdIso |
86 | 74, 83, 85 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . 21
OrdIso |
87 | | en0 8019 |
. . . . . . . . . . . . . . . . . . . . 21
OrdIso
OrdIso
|
88 | 86, 87 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . 20
OrdIso |
89 | 88 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . . 19
seq𝜔 OrdIso OrdIso OrdIso seq𝜔 OrdIso OrdIso
|
90 | 81 | seqom0g 7551 |
. . . . . . . . . . . . . . . . . . . 20
seq𝜔 OrdIso OrdIso
|
91 | 74, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
seq𝜔 OrdIso OrdIso |
92 | 89, 91 | eqtri 2644 |
. . . . . . . . . . . . . . . . . 18
seq𝜔 OrdIso OrdIso OrdIso |
93 | 82, 92 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
CNF CNF |
94 | 14 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
CNF CNF
|
95 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . 19
CNF CNF |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . 18
CNF CNF |
97 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . . 18
CNF CNF CNF |
98 | 96, 80, 97 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
CNF CNF CNF |
99 | 93, 98 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . 16
CNF
CNF |
100 | 33, 51, 99 | pm2.61ne 2879 |
. . . . . . . . . . . . . . 15
CNF CNF |
101 | 100 | expr 643 |
. . . . . . . . . . . . . 14
CNF
CNF |
102 | 32, 101 | sylbid 230 |
. . . . . . . . . . . . 13
CNF CNF |
103 | 102 | ex 450 |
. . . . . . . . . . . 12
CNF
CNF |
104 | 103 | com23 86 |
. . . . . . . . . . 11
CNF
CNF |
105 | 104 | a2i 14 |
. . . . . . . . . 10
CNF
CNF |
106 | 105 | a1i 11 |
. . . . . . . . 9
CNF
CNF |
107 | 24, 106 | syl5bi 232 |
. . . . . . . 8
CNF
CNF |
108 | 23, 107 | tfis2 7056 |
. . . . . . 7
CNF |
109 | 108 | com3l 89 |
. . . . . 6
CNF |
110 | 19, 109 | mpdd 43 |
. . . . 5
CNF |
111 | 110 | ssrdv 3609 |
. . . 4
CNF |
112 | 16, 111 | eqssd 3620 |
. . 3
CNF |
113 | | dffo2 6119 |
. . 3
CNF
CNF
CNF |
114 | 14, 112, 113 | sylanbrc 698 |
. 2
CNF |
115 | 2 | adantr 481 |
. . . . . 6
|
116 | 3 | adantr 481 |
. . . . . 6
|
117 | | fveq2 6191 |
. . . . . . . . . . . 12
|
118 | | fveq2 6191 |
. . . . . . . . . . . 12
|
119 | 117, 118 | eleq12d 2695 |
. . . . . . . . . . 11
|
120 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
121 | 120 | imbi1d 331 |
. . . . . . . . . . . 12
|
122 | 121 | ralbidv 2986 |
. . . . . . . . . . 11
|
123 | 119, 122 | anbi12d 747 |
. . . . . . . . . 10
|
124 | 123 | cbvrexv 3172 |
. . . . . . . . 9
|
125 | | fveq1 6190 |
. . . . . . . . . . . 12
|
126 | | fveq1 6190 |
. . . . . . . . . . . 12
|
127 | | eleq12 2691 |
. . . . . . . . . . . 12
|
128 | 125, 126,
127 | syl2an 494 |
. . . . . . . . . . 11
|
129 | | fveq1 6190 |
. . . . . . . . . . . . . 14
|
130 | | fveq1 6190 |
. . . . . . . . . . . . . 14
|
131 | 129, 130 | eqeqan12d 2638 |
. . . . . . . . . . . . 13
|
132 | 131 | imbi2d 330 |
. . . . . . . . . . . 12
|
133 | 132 | ralbidv 2986 |
. . . . . . . . . . 11
|
134 | 128, 133 | anbi12d 747 |
. . . . . . . . . 10
|
135 | 134 | rexbidv 3052 |
. . . . . . . . 9
|
136 | 124, 135 | syl5bb 272 |
. . . . . . . 8
|
137 | 136 | cbvopabv 4722 |
. . . . . . 7
|
138 | 4, 137 | eqtri 2644 |
. . . . . 6
|
139 | | simprll 802 |
. . . . . 6
|
140 | | simprlr 803 |
. . . . . 6
|
141 | | simprr 796 |
. . . . . 6
|
142 | | eqid 2622 |
. . . . . 6
|
143 | | eqid 2622 |
. . . . . 6
OrdIso supp OrdIso supp |
144 | | eqid 2622 |
. . . . . 6
seq𝜔 OrdIso supp OrdIso supp seq𝜔 OrdIso supp OrdIso
supp |
145 | 1, 115, 116, 138, 139, 140, 141, 142, 143, 144 | cantnflem1 8586 |
. . . . 5
CNF CNF |
146 | | fvex 6201 |
. . . . . 6
CNF |
147 | 146 | epelc 5031 |
. . . . 5
CNF CNF CNF CNF |
148 | 145, 147 | sylibr 224 |
. . . 4
CNF CNF |
149 | 148 | expr 643 |
. . 3
CNF CNF |
150 | 149 | ralrimivva 2971 |
. 2
CNF CNF |
151 | | soisoi 6578 |
. 2
CNF
CNF CNF CNF
|
152 | 5, 13, 114, 150, 151 | syl22anc 1327 |
1
CNF
|