Proof of Theorem cantnflem1b
Step | Hyp | Ref
| Expression |
1 | | simprr 774 |
. . . 4
 

              |
2 | | cantnflem1.o |
. . . . . . . 8
OrdIso  supp    |
3 | 2 | oicl 8062 |
. . . . . . 7
 |
4 | | cantnfs.b |
. . . . . . . . . . . 12
   |
5 | | suppssdm 6946 |
. . . . . . . . . . . . 13
 supp 
 |
6 | | oemapval.g |
. . . . . . . . . . . . . . . 16
   |
7 | | cantnfs.s |
. . . . . . . . . . . . . . . . 17
 CNF   |
8 | | cantnfs.a |
. . . . . . . . . . . . . . . . 17
   |
9 | 7, 8, 4 | cantnfs 8189 |
. . . . . . . . . . . . . . . 16
       finSupp     |
10 | 6, 9 | mpbid 215 |
. . . . . . . . . . . . . . 15
      finSupp
   |
11 | 10 | simpld 466 |
. . . . . . . . . . . . . 14
       |
12 | | fdm 5745 |
. . . . . . . . . . . . . 14
       |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . 13
   |
14 | 5, 13 | syl5sseq 3466 |
. . . . . . . . . . . 12
  supp    |
15 | 4, 14 | ssexd 4543 |
. . . . . . . . . . 11
  supp    |
16 | 7, 8, 4, 2, 6 | cantnfcl 8190 |
. . . . . . . . . . . 12
  supp     |
17 | 16 | simpld 466 |
. . . . . . . . . . 11
  supp    |
18 | 2 | oiiso 8070 |
. . . . . . . . . . 11
   supp 

supp      supp
    |
19 | 15, 17, 18 | syl2anc 673 |
. . . . . . . . . 10

   supp     |
20 | | isof1o 6234 |
. . . . . . . . . 10

   supp        supp    |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
      supp    |
22 | | f1ocnv 5840 |
. . . . . . . . 9
      supp 
    supp      |
23 | | f1of 5828 |
. . . . . . . . 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 8208 |
. . . . . . . 8
  supp    |
30 | 24, 29 | ffvelrnd 6038 |
. . . . . . 7
        |
31 | | ordelon 5454 |
. . . . . . 7
 
             |
32 | 3, 30, 31 | sylancr 676 |
. . . . . 6
        |
33 | 32 | adantr 472 |
. . . . 5
 

              |
34 | 3 | a1i 11 |
. . . . . . . 8

  |
35 | | ordelon 5454 |
. . . . . . . 8
 

  |
36 | 34, 35 | sylan 479 |
. . . . . . 7
 
   |
37 | | sucelon 6663 |
. . . . . . 7

  |
38 | 36, 37 | sylibr 217 |
. . . . . 6
 

  |
39 | 38 | adantrr 731 |
. . . . 5
 

         |
40 | | ontri1 5464 |
. . . . 5
             
        |
41 | 33, 39, 40 | syl2anc 673 |
. . . 4
 

            
        |
42 | 1, 41 | mpbid 215 |
. . 3
 

      
       |
43 | 19 | adantr 472 |
. . . . . 6
 

          supp
    |
44 | | ordtr 5444 |
. . . . . . . 8

  |
45 | 3, 44 | mp1i 13 |
. . . . . . 7
 

      
  |
46 | | simprl 772 |
. . . . . . 7
 

      
  |
47 | | trsuc 5514 |
. . . . . . 7
  
  |
48 | 45, 46, 47 | syl2anc 673 |
. . . . . 6
 

         |
49 | 30 | adantr 472 |
. . . . . 6
 

              |
50 | | isorel 6235 |
. . . . . 6
 
   supp   
                             |
51 | 43, 48, 49, 50 | syl12anc 1290 |
. . . . 5
 

            
                |
52 | | fvex 5889 |
. . . . . 6
      |
53 | 52 | epelc 4752 |
. . . . 5
     
       |
54 | | fvex 5889 |
. . . . . 6
          |
55 | 54 | epelc 4752 |
. . . . 5
                             |
56 | 51, 53, 55 | 3bitr3g 295 |
. . . 4
 

            
                |
57 | | f1ocnvfv2 6194 |
. . . . . . 7
       supp   supp              |
58 | 21, 29, 57 | syl2anc 673 |
. . . . . 6
            |
59 | 58 | adantr 472 |
. . . . 5
 

                  |
60 | 59 | eleq2d 2534 |
. . . 4
 

                            |
61 | 56, 60 | bitrd 261 |
. . 3
 

            
       |
62 | 42, 61 | mtbid 307 |
. 2
 

      
      |
63 | 7, 8, 4, 25, 26, 6, 27, 28 | oemapvali 8207 |
. . . . . 6
                        |
64 | 63 | simp1d 1042 |
. . . . 5
   |
65 | | onelon 5455 |
. . . . 5
 
   |
66 | 4, 64, 65 | syl2anc 673 |
. . . 4
   |
67 | 66 | adantr 472 |
. . 3
 

         |
68 | 4 | adantr 472 |
. . . 4
 

         |
69 | 14 | adantr 472 |
. . . . 5
 

        supp    |
70 | 2 | oif 8063 |
. . . . . . 7
     supp   |
71 | 70 | ffvelrni 6036 |
. . . . . 6
      supp    |
72 | 48, 71 | syl 17 |
. . . . 5
 

            supp    |
73 | 69, 72 | sseldd 3419 |
. . . 4
 

             |
74 | | onelon 5455 |
. . . 4
             |
75 | 68, 73, 74 | syl2anc 673 |
. . 3
 

             |
76 | | ontri1 5464 |
. . 3
                   |
77 | 67, 75, 76 | syl2anc 673 |
. 2
 

                   |
78 | 62, 77 | mpbird 240 |
1
 

             |