Step | Hyp | Ref
| Expression |
1 | | cantnf.s |
. . . 4

 CNF    |
2 | | cantnfs.a |
. . . . . . . . 9
   |
3 | | cantnfs.s |
. . . . . . . . . . . . 13
 CNF   |
4 | | cantnfs.b |
. . . . . . . . . . . . 13
   |
5 | | oemapval.t |
. . . . . . . . . . . . 13
   

        


            |
6 | | cantnf.c |
. . . . . . . . . . . . 13
     |
7 | | cantnf.e |
. . . . . . . . . . . . 13

  |
8 | 3, 2, 4, 5, 6, 1, 7 | cantnflem2 8195 |
. . . . . . . . . . . 12
         |
9 | | eqid 2451 |
. . . . . . . . . . . . . 14
 |
10 | | eqid 2451 |
. . . . . . . . . . . . . 14
 |
11 | | eqid 2451 |
. . . . . . . . . . . . . 14
 |
12 | 9, 10, 11 | 3pm3.2i 1186 |
. . . . . . . . . . . . 13

  |
13 | | cantnf.x |
. . . . . . . . . . . . . 14
       |
14 | | cantnf.p |
. . . . . . . . . . . . . 14
    
                |
15 | | cantnf.y |
. . . . . . . . . . . . . 14
     |
16 | | cantnf.z |
. . . . . . . . . . . . . 14
     |
17 | 13, 14, 15, 16 | oeeui 7303 |
. . . . . . . . . . . . 13
   
                 

    |
18 | 12, 17 | mpbiri 237 |
. . . . . . . . . . . 12
   
                   |
19 | 8, 18 | syl 17 |
. . . . . . . . . . 11
                 |
20 | 19 | simpld 461 |
. . . . . . . . . 10
   
     |
21 | 20 | simp1d 1020 |
. . . . . . . . 9
   |
22 | | oecl 7239 |
. . . . . . . . 9
 
     |
23 | 2, 21, 22 | syl2anc 667 |
. . . . . . . 8
     |
24 | 20 | simp2d 1021 |
. . . . . . . . . 10
     |
25 | 24 | eldifad 3416 |
. . . . . . . . 9
   |
26 | | onelon 5448 |
. . . . . . . . 9
 
   |
27 | 2, 25, 26 | syl2anc 667 |
. . . . . . . 8
   |
28 | | omcl 7238 |
. . . . . . . 8
   
       |
29 | 23, 27, 28 | syl2anc 667 |
. . . . . . 7
       |
30 | 20 | simp3d 1022 |
. . . . . . . 8
     |
31 | | onelon 5448 |
. . . . . . . 8
   
  
  |
32 | 23, 30, 31 | syl2anc 667 |
. . . . . . 7
   |
33 | | oaword1 7253 |
. . . . . . 7
     
    
        |
34 | 29, 32, 33 | syl2anc 667 |
. . . . . 6
    
        |
35 | | dif1o 7202 |
. . . . . . . . . . 11
  
    |
36 | 35 | simprbi 466 |
. . . . . . . . . 10
  
  |
37 | 24, 36 | syl 17 |
. . . . . . . . 9
   |
38 | | on0eln0 5478 |
. . . . . . . . . 10
 
   |
39 | 27, 38 | syl 17 |
. . . . . . . . 9
 
   |
40 | 37, 39 | mpbird 236 |
. . . . . . . 8

  |
41 | | omword1 7274 |
. . . . . . . 8
               |
42 | 23, 27, 40, 41 | syl21anc 1267 |
. . . . . . 7
  
      |
43 | 42, 30 | sseldd 3433 |
. . . . . 6
       |
44 | 34, 43 | sseldd 3433 |
. . . . 5
         |
45 | 19 | simprd 465 |
. . . . 5
         |
46 | 44, 45 | eleqtrd 2531 |
. . . 4
   |
47 | 1, 46 | sseldd 3433 |
. . 3
  CNF    |
48 | 3, 2, 4 | cantnff 8179 |
. . . 4
  CNF          |
49 | | ffn 5728 |
. . . 4
  CNF         CNF    |
50 | | fvelrnb 5912 |
. . . 4
  CNF 
  CNF     CNF        |
51 | 48, 49, 50 | 3syl 18 |
. . 3
  
CNF     CNF        |
52 | 47, 51 | mpbid 214 |
. 2
    CNF       |
53 | 2 | adantr 467 |
. . 3
 

  CNF      
  |
54 | 4 | adantr 467 |
. . 3
 

  CNF      
  |
55 | 6 | adantr 467 |
. . 3
 

  CNF      
    |
56 | 1 | adantr 467 |
. . 3
 

  CNF        CNF    |
57 | 7 | adantr 467 |
. . 3
 

  CNF         |
58 | | simprl 764 |
. . 3
 

  CNF         |
59 | | simprr 766 |
. . 3
 

  CNF         CNF       |
60 | | eqid 2451 |
. . 3
    
                  |
61 | 3, 53, 54, 5, 55, 56, 57, 13, 14, 15, 16, 58, 59, 60 | cantnflem3 8196 |
. 2
 

  CNF      
 CNF    |
62 | 52, 61 | rexlimddv 2883 |
1
  CNF    |