Proof of Theorem konigthlem
Step | Hyp | Ref
| Expression |
1 | | fvex 5873 |
. . . . . . . . 9
     |
2 | | fvex 5873 |
. . . . . . . . . . 11
         |
3 | | eqid 2450 |
. . . . . . . . . . 11
                             |
4 | 2, 3 | fnmpti 5704 |
. . . . . . . . . 10
                   |
5 | 1 | mptex 6134 |
. . . . . . . . . . . 12
               |
6 | | konigth.4 |
. . . . . . . . . . . . 13
                 |
7 | 6 | fvmpt2 5955 |
. . . . . . . . . . . 12
                                     |
8 | 5, 7 | mpan2 676 |
. . . . . . . . . . 11
                     |
9 | 8 | fneq1d 5664 |
. . . . . . . . . 10
         
                     |
10 | 4, 9 | mpbiri 237 |
. . . . . . . . 9
           |
11 | | fnrndomg 8960 |
. . . . . . . . 9
                         |
12 | 1, 10, 11 | mpsyl 65 |
. . . . . . . 8
           |
13 | | domsdomtr 7704 |
. . . . . . . 8
                             |
14 | 12, 13 | sylan 474 |
. . . . . . 7
                     |
15 | | sdomdif 7717 |
. . . . . . 7
             
       |
16 | 14, 15 | syl 17 |
. . . . . 6
               
       |
17 | 16 | ralimiaa 2779 |
. . . . 5
 
       

            |
18 | | konigth.1 |
. . . . . 6
 |
19 | | fvex 5873 |
. . . . . . 7
     |
20 | | difss 3559 |
. . . . . . 7
    
          |
21 | 19, 20 | ssexi 4547 |
. . . . . 6
    
      |
22 | 18, 21 | ac6c5 8909 |
. . . . 5
 
    
    
  
        
       |
23 | | equid 1854 |
. . . . . . 7
 |
24 | | eldifi 3554 |
. . . . . . . . . . . . 13
                         |
25 | | fvex 5873 |
. . . . . . . . . . . . . . 15
     |
26 | | konigth.5 |
. . . . . . . . . . . . . . . 16
       |
27 | 26 | fvmpt2 5955 |
. . . . . . . . . . . . . . 15
                 |
28 | 25, 27 | mpan2 676 |
. . . . . . . . . . . . . 14
           |
29 | 28 | eleq1d 2512 |
. . . . . . . . . . . . 13
         
           |
30 | 24, 29 | syl5ibr 225 |
. . . . . . . . . . . 12
          
                |
31 | 30 | ralimia 2778 |
. . . . . . . . . . 11
 
             

          |
32 | 25, 26 | fnmpti 5704 |
. . . . . . . . . . 11
 |
33 | 31, 32 | jctil 540 |
. . . . . . . . . 10
 
             


           |
34 | 18 | mptex 6134 |
. . . . . . . . . . . 12
       |
35 | 26, 34 | eqeltri 2524 |
. . . . . . . . . . 11
 |
36 | 35 | elixp 7526 |
. . . . . . . . . 10
                   |
37 | 33, 36 | sylibr 216 |
. . . . . . . . 9
 
             
       |
38 | | konigth.3 |
. . . . . . . . 9
      |
39 | 37, 38 | syl6eleqr 2539 |
. . . . . . . 8
 
             
  |
40 | | foelrn 6039 |
. . . . . . . . . 10
     


      |
41 | 40 | expcom 437 |
. . . . . . . . 9
      
       |
42 | | konigth.2 |
. . . . . . . . . . . . . . 15
      |
43 | 42 | eleq2i 2520 |
. . . . . . . . . . . . . 14

       |
44 | | eliun 4282 |
. . . . . . . . . . . . . 14
     

      |
45 | 43, 44 | bitri 253 |
. . . . . . . . . . . . 13


      |
46 | | nfra1 2768 |
. . . . . . . . . . . . . . 15
           
      |
47 | | nfv 1760 |
. . . . . . . . . . . . . . 15
      |
48 | 46, 47 | nfan 2010 |
. . . . . . . . . . . . . 14
            
           |
49 | | nfv 1760 |
. . . . . . . . . . . . . 14
  |
50 | 28 | ad2antrl 733 |
. . . . . . . . . . . . . . . . . . . 20
      
                |
51 | | fveq1 5862 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
52 | 8 | fveq1d 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
                             |
53 | 3 | fvmpt2 5955 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                           |
54 | 2, 53 | mpan2 676 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                 |
55 | 52, 54 | sylan9eq 2504 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                       |
56 | 55 | eqcomd 2456 |
. . . . . . . . . . . . . . . . . . . . 21
 
                       |
57 | 51, 56 | sylan9eq 2504 |
. . . . . . . . . . . . . . . . . . . 20
      
                    |
58 | 50, 57 | eqtr3d 2486 |
. . . . . . . . . . . . . . . . . . 19
      
                    |
59 | | fnfvelrn 6017 |
. . . . . . . . . . . . . . . . . . . . 21
         
                   |
60 | 10, 59 | sylan 474 |
. . . . . . . . . . . . . . . . . . . 20
 
                   |
61 | 60 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
      
                    |
62 | 58, 61 | eqeltrd 2528 |
. . . . . . . . . . . . . . . . . 18
      
                |
63 | 62 | 3adant1 1025 |
. . . . . . . . . . . . . . . . 17
           
    
    
                |
64 | | simp1 1007 |
. . . . . . . . . . . . . . . . . 18
           
    
    
               
       |
65 | | simp3l 1035 |
. . . . . . . . . . . . . . . . . 18
           
    
    
        |
66 | | rsp 2753 |
. . . . . . . . . . . . . . . . . . 19
 
             

                 |
67 | | eldifn 3555 |
. . . . . . . . . . . . . . . . . . 19
                         |
68 | 66, 67 | syl6 34 |
. . . . . . . . . . . . . . . . . 18
 
             

           |
69 | 64, 65, 68 | sylc 62 |
. . . . . . . . . . . . . . . . 17
           
    
    
     
          |
70 | 63, 69 | pm2.21dd 178 |
. . . . . . . . . . . . . . . 16
           
    
    
     
  |
71 | 70 | 3expia 1209 |
. . . . . . . . . . . . . . 15
           
    
           
   |
72 | 71 | expd 438 |
. . . . . . . . . . . . . 14
           
    
          
    |
73 | 48, 49, 72 | rexlimd 2870 |
. . . . . . . . . . . . 13
           
    
          
   |
74 | 45, 73 | syl5bi 221 |
. . . . . . . . . . . 12
           
    
         |
75 | 74 | ex 436 |
. . . . . . . . . . 11
 
             
     
    |
76 | 75 | com23 81 |
. . . . . . . . . 10
 
             

    
    |
77 | 76 | rexlimdv 2876 |
. . . . . . . . 9
 
             
 
   
   |
78 | 41, 77 | syl9r 74 |
. . . . . . . 8
 
             

    
    |
79 | 39, 78 | mpd 15 |
. . . . . . 7
 
             
    
   |
80 | 23, 79 | mt2i 122 |
. . . . . 6
 
             
      |
81 | 80 | exlimiv 1775 |
. . . . 5
            
    
      |
82 | 17, 22, 81 | 3syl 18 |
. . . 4
 
       
      |
83 | 82 | nexdv 1781 |
. . 3
 
       
       |
84 | 1 | 0dom 7699 |
. . . . . . . 8
     |
85 | | domsdomtr 7704 |
. . . . . . . 8
                     |
86 | 84, 85 | mpan 675 |
. . . . . . 7
        
      |
87 | 19 | 0sdom 7700 |
. . . . . . 7
           |
88 | 86, 87 | sylib 200 |
. . . . . 6
        
      |
89 | 88 | ralimi 2780 |
. . . . 5
 
       

      |
90 | 38 | neeq1i 2687 |
. . . . . 6
        |
91 | 19 | rgenw 2748 |
. . . . . . . . 9

     |
92 | | ixpexg 7543 |
. . . . . . . . 9
 
   
       |
93 | 91, 92 | ax-mp 5 |
. . . . . . . 8

     |
94 | 38, 93 | eqeltri 2524 |
. . . . . . 7
 |
95 | 94 | 0sdom 7700 |
. . . . . 6
   |
96 | 18, 19 | ac9 8910 |
. . . . . 6
 
           |
97 | 90, 95, 96 | 3bitr4i 281 |
. . . . 5
        |
98 | 89, 97 | sylibr 216 |
. . . 4
 
       
  |
99 | 18, 1 | iunex 6770 |
. . . . . . 7

     |
100 | 42, 99 | eqeltri 2524 |
. . . . . 6
 |
101 | | domtri 8978 |
. . . . . 6
 
 
   |
102 | 94, 100, 101 | mp2an 677 |
. . . . 5

  |
103 | 102 | biimpri 210 |
. . . 4

  |
104 | | fodomr 7720 |
. . . 4
          |
105 | 98, 103, 104 | syl2an 480 |
. . 3
          
        |
106 | 83, 105 | mtand 664 |
. 2
 
       
  |
107 | 106 | notnotrd 117 |
1
 
       
  |