Step | Hyp | Ref
| Expression |
1 | | fvex 6201 |
. . . 4
seq𝜔 |
2 | 1 | csbex 4793 |
. . 3
OrdIso supp seq𝜔
|
3 | 2 | a1i 11 |
. 2
OrdIso supp seq𝜔
|
4 | | eqid 2622 |
. . . 4
finSupp finSupp |
5 | | cantnfs.a |
. . . 4
|
6 | | cantnfs.b |
. . . 4
|
7 | 4, 5, 6 | cantnffval 8560 |
. . 3
CNF finSupp OrdIso supp seq𝜔 |
8 | | cantnfs.s |
. . . . 5
CNF |
9 | 4, 5, 6 | cantnfdm 8561 |
. . . . 5
CNF finSupp |
10 | 8, 9 | syl5eq 2668 |
. . . 4
finSupp |
11 | 10 | mpteq1d 4738 |
. . 3
OrdIso
supp seq𝜔 finSupp OrdIso supp seq𝜔
|
12 | 7, 11 | eqtr4d 2659 |
. 2
CNF OrdIso supp seq𝜔
|
13 | 5 | adantr 481 |
. . . . . . . 8
|
14 | 6 | adantr 481 |
. . . . . . . 8
|
15 | | eqid 2622 |
. . . . . . . 8
OrdIso supp OrdIso supp |
16 | | simpr 477 |
. . . . . . . 8
|
17 | | eqid 2622 |
. . . . . . . 8
seq𝜔 OrdIso supp OrdIso supp seq𝜔 OrdIso supp OrdIso
supp |
18 | 8, 13, 14, 15, 16, 17 | cantnfval 8565 |
. . . . . . 7
CNF seq𝜔 OrdIso supp OrdIso supp OrdIso supp |
19 | 18 | adantr 481 |
. . . . . 6
CNF seq𝜔 OrdIso supp OrdIso supp OrdIso supp |
20 | | ovex 6678 |
. . . . . . . . . . 11
supp
|
21 | 8, 13, 14, 15, 16 | cantnfcl 8564 |
. . . . . . . . . . . 12
supp OrdIso supp |
22 | 21 | simpld 475 |
. . . . . . . . . . 11
supp |
23 | 15 | oien 8443 |
. . . . . . . . . . 11
supp
supp
OrdIso supp supp |
24 | 20, 22, 23 | sylancr 695 |
. . . . . . . . . 10
OrdIso supp supp |
25 | 24 | adantr 481 |
. . . . . . . . 9
OrdIso supp supp |
26 | | suppssdm 7308 |
. . . . . . . . . . 11
supp
|
27 | 8, 5, 6 | cantnfs 8563 |
. . . . . . . . . . . . 13
finSupp |
28 | 27 | simprbda 653 |
. . . . . . . . . . . 12
|
29 | | fdm 6051 |
. . . . . . . . . . . 12
|
30 | 28, 29 | syl 17 |
. . . . . . . . . . 11
|
31 | 26, 30 | syl5sseq 3653 |
. . . . . . . . . 10
supp |
32 | | feq3 6028 |
. . . . . . . . . . . . . 14
|
33 | 28, 32 | syl5ibcom 235 |
. . . . . . . . . . . . 13
|
34 | 33 | imp 445 |
. . . . . . . . . . . 12
|
35 | | f00 6087 |
. . . . . . . . . . . 12
|
36 | 34, 35 | sylib 208 |
. . . . . . . . . . 11
|
37 | 36 | simprd 479 |
. . . . . . . . . 10
|
38 | | sseq0 3975 |
. . . . . . . . . 10
supp supp |
39 | 31, 37, 38 | syl2an2r 876 |
. . . . . . . . 9
supp |
40 | 25, 39 | breqtrd 4679 |
. . . . . . . 8
OrdIso supp |
41 | | en0 8019 |
. . . . . . . 8
OrdIso
supp OrdIso
supp |
42 | 40, 41 | sylib 208 |
. . . . . . 7
OrdIso supp |
43 | 42 | fveq2d 6195 |
. . . . . 6
seq𝜔
OrdIso supp OrdIso supp OrdIso supp seq𝜔 OrdIso supp OrdIso supp |
44 | | 0ex 4790 |
. . . . . . 7
|
45 | 17 | seqom0g 7551 |
. . . . . . 7
seq𝜔 OrdIso supp OrdIso supp |
46 | 44, 45 | mp1i 13 |
. . . . . 6
seq𝜔
OrdIso supp OrdIso supp |
47 | 19, 43, 46 | 3eqtrd 2660 |
. . . . 5
CNF |
48 | | el1o 7579 |
. . . . 5
CNF CNF |
49 | 47, 48 | sylibr 224 |
. . . 4
CNF |
50 | 37 | oveq2d 6666 |
. . . . 5
|
51 | 13 | adantr 481 |
. . . . . 6
|
52 | | oe0 7602 |
. . . . . 6
|
53 | 51, 52 | syl 17 |
. . . . 5
|
54 | 50, 53 | eqtrd 2656 |
. . . 4
|
55 | 49, 54 | eleqtrrd 2704 |
. . 3
CNF |
56 | 13 | adantr 481 |
. . . 4
|
57 | 14 | adantr 481 |
. . . 4
|
58 | 16 | adantr 481 |
. . . 4
|
59 | | on0eln0 5780 |
. . . . . 6
|
60 | 13, 59 | syl 17 |
. . . . 5
|
61 | 60 | biimpar 502 |
. . . 4
|
62 | 31 | adantr 481 |
. . . 4
supp |
63 | 8, 56, 57, 58, 61, 57, 62 | cantnflt2 8570 |
. . 3
CNF |
64 | 55, 63 | pm2.61dane 2881 |
. 2
CNF |
65 | 3, 12, 64 | fmpt2d 6393 |
1
CNF |