Step | Hyp | Ref
| Expression |
1 | | fvex 5880 |
. . . 4
seq𝜔                            |
2 | 1 | csbex 4541 |
. . 3
OrdIso  supp    ![]_ ]_](_urbrack.gif) seq𝜔  
                         |
3 | 2 | a1i 11 |
. 2
 
 OrdIso  supp    ![]_ ]_](_urbrack.gif) seq𝜔  
                          |
4 | | eqid 2453 |
. . . 4
   finSupp     finSupp   |
5 | | cantnfs.a |
. . . 4
   |
6 | | cantnfs.b |
. . . 4
   |
7 | 4, 5, 6 | cantnffval 8173 |
. . 3
  CNF      finSupp  OrdIso  supp    ![]_ ]_](_urbrack.gif) seq𝜔                              |
8 | | cantnfs.s |
. . . . 5
 CNF   |
9 | 4, 5, 6 | cantnfdm 8174 |
. . . . 5
  CNF     finSupp    |
10 | 8, 9 | syl5eq 2499 |
. . . 4
    finSupp    |
11 | 10 | mpteq1d 4487 |
. . 3
  OrdIso
 supp    ![]_ ]_](_urbrack.gif) seq𝜔                                finSupp  OrdIso  supp    ![]_ ]_](_urbrack.gif) seq𝜔  
                           |
12 | 7, 11 | eqtr4d 2490 |
. 2
  CNF   OrdIso  supp    ![]_ ]_](_urbrack.gif) seq𝜔  
                           |
13 | 5 | adantr 467 |
. . . . . . . 8
 
   |
14 | 6 | adantr 467 |
. . . . . . . 8
 
   |
15 | | eqid 2453 |
. . . . . . . 8
OrdIso  supp   OrdIso  supp    |
16 | | simpr 463 |
. . . . . . . 8
 
   |
17 | | eqid 2453 |
. . . . . . . 8
seq𝜔      OrdIso  supp          OrdIso  supp            seq𝜔      OrdIso  supp          OrdIso
 supp             |
18 | 8, 13, 14, 15, 16, 17 | cantnfval 8178 |
. . . . . . 7
 
   CNF     seq𝜔      OrdIso  supp          OrdIso  supp              OrdIso  supp      |
19 | 18 | adantr 467 |
. . . . . 6
       CNF     seq𝜔      OrdIso  supp          OrdIso  supp              OrdIso  supp      |
20 | | ovex 6323 |
. . . . . . . . . . 11
 supp 
 |
21 | 8, 13, 14, 15, 16 | cantnfcl 8177 |
. . . . . . . . . . . 12
 
  supp  OrdIso  supp      |
22 | 21 | simpld 461 |
. . . . . . . . . . 11
 
  supp    |
23 | 15 | oien 8058 |
. . . . . . . . . . 11
   supp 

supp  
OrdIso  supp    supp    |
24 | 20, 22, 23 | sylancr 670 |
. . . . . . . . . 10
 
 OrdIso  supp    supp    |
25 | 24 | adantr 467 |
. . . . . . . . 9
     OrdIso  supp    supp    |
26 | | suppssdm 6932 |
. . . . . . . . . . . 12
 supp 
 |
27 | 8, 5, 6 | cantnfs 8176 |
. . . . . . . . . . . . . 14
       finSupp     |
28 | 27 | simprbda 629 |
. . . . . . . . . . . . 13
 
       |
29 | | fdm 5738 |
. . . . . . . . . . . . 13
       |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
 

  |
31 | 26, 30 | syl5sseq 3482 |
. . . . . . . . . . 11
 
  supp    |
32 | 31 | adantr 467 |
. . . . . . . . . 10
      supp    |
33 | | feq3 5717 |
. . . . . . . . . . . . . 14

    
       |
34 | 28, 33 | syl5ibcom 224 |
. . . . . . . . . . . . 13
 
 
       |
35 | 34 | imp 431 |
. . . . . . . . . . . 12
           |
36 | | f00 5770 |
. . . . . . . . . . . 12
    
    |
37 | 35, 36 | sylib 200 |
. . . . . . . . . . 11
         |
38 | 37 | simprd 465 |
. . . . . . . . . 10
       |
39 | | sseq0 3768 |
. . . . . . . . . 10
   supp    supp    |
40 | 32, 38, 39 | syl2anc 667 |
. . . . . . . . 9
      supp    |
41 | 25, 40 | breqtrd 4430 |
. . . . . . . 8
     OrdIso  supp     |
42 | | en0 7637 |
. . . . . . . 8
 OrdIso
 supp   OrdIso
 supp     |
43 | 41, 42 | sylib 200 |
. . . . . . 7
     OrdIso  supp     |
44 | 43 | fveq2d 5874 |
. . . . . 6
     seq𝜔  
   OrdIso  supp          OrdIso  supp              OrdIso  supp    seq𝜔      OrdIso  supp          OrdIso  supp                 |
45 | | 0ex 4538 |
. . . . . . 7
 |
46 | 17 | seqom0g 7178 |
. . . . . . 7

seq𝜔      OrdIso  supp          OrdIso  supp                 |
47 | 45, 46 | mp1i 13 |
. . . . . 6
     seq𝜔  
   OrdIso  supp          OrdIso  supp                 |
48 | 19, 44, 47 | 3eqtrd 2491 |
. . . . 5
       CNF       |
49 | | el1o 7206 |
. . . . 5
   CNF       CNF       |
50 | 48, 49 | sylibr 216 |
. . . 4
       CNF       |
51 | 38 | oveq2d 6311 |
. . . . 5
           |
52 | 13 | adantr 467 |
. . . . . 6
       |
53 | | oe0 7229 |
. . . . . 6
     |
54 | 52, 53 | syl 17 |
. . . . 5
         |
55 | 51, 54 | eqtrd 2487 |
. . . 4
         |
56 | 50, 55 | eleqtrrd 2534 |
. . 3
       CNF         |
57 | 13 | adantr 467 |
. . . 4
       |
58 | 14 | adantr 467 |
. . . 4
       |
59 | 16 | adantr 467 |
. . . 4
       |
60 | | on0eln0 5481 |
. . . . . 6
 
   |
61 | 13, 60 | syl 17 |
. . . . 5
 
 
   |
62 | 61 | biimpar 488 |
. . . 4
       |
63 | 31 | adantr 467 |
. . . 4
      supp    |
64 | 8, 57, 58, 59, 62, 58, 63 | cantnflt2 8183 |
. . 3
       CNF         |
65 | 56, 64 | pm2.61dane 2713 |
. 2
 
   CNF         |
66 | 3, 12, 65 | fmpt2d 6058 |
1
  CNF          |