Step | Hyp | Ref
| Expression |
1 | | pm3.24 892 |
. 2
   |
2 | | df-ne 2623 |
. . . . 5

  |
3 | 2 | ralbii 2818 |
. . . 4
 

  |
4 | | df-ral 2741 |
. . . 4
 
      |
5 | | ralnex 2833 |
. . . 4
 
   |
6 | 3, 4, 5 | 3bitr3i 279 |
. . 3
   

   |
7 | | weso 4824 |
. . . . . . . . 9
   |
8 | 7 | adantr 467 |
. . . . . . . 8
    
    |
9 | | vex 3047 |
. . . . . . . 8
 |
10 | | soex 6733 |
. . . . . . . 8
 
   |
11 | 8, 9, 10 | sylancl 667 |
. . . . . . 7
    
    |
12 | | zorn2lem.3 |
. . . . . . . . . . 11
recs           |
13 | 12 | tfr1 7112 |
. . . . . . . . . 10
 |
14 | | fvelrnb 5910 |
. . . . . . . . . 10
          |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . 9

       |
16 | | nfv 1760 |
. . . . . . . . . . 11

 |
17 | | nfa1 1978 |
. . . . . . . . . . 11
    
  |
18 | 16, 17 | nfan 2010 |
. . . . . . . . . 10
         |
19 | | nfv 1760 |
. . . . . . . . . 10

 |
20 | | zorn2lem.5 |
. . . . . . . . . . . . . . . . . 18
           |
21 | | ssrab2 3513 |
. . . . . . . . . . . . . . . . . 18
 
         |
22 | 20, 21 | eqsstri 3461 |
. . . . . . . . . . . . . . . . 17
 |
23 | | zorn2lem.4 |
. . . . . . . . . . . . . . . . . 18
      |
24 | 12, 23, 20 | zorn2lem1 8923 |
. . . . . . . . . . . . . . . . 17
  
        |
25 | 22, 24 | sseldi 3429 |
. . . . . . . . . . . . . . . 16
  
        |
26 | | eleq1 2516 |
. . . . . . . . . . . . . . . 16
         
   |
27 | 25, 26 | syl5ibcom 224 |
. . . . . . . . . . . . . . 15
  
      
   |
28 | 27 | exp32 609 |
. . . . . . . . . . . . . 14
             |
29 | 28 | com12 32 |
. . . . . . . . . . . . 13
             |
30 | 29 | a2d 29 |
. . . . . . . . . . . 12
               |
31 | 30 | spsd 1944 |
. . . . . . . . . . 11
    


    
     |
32 | 31 | imp 431 |
. . . . . . . . . 10
    
            |
33 | 18, 19, 32 | rexlimd 2870 |
. . . . . . . . 9
    
   
       |
34 | 15, 33 | syl5bi 221 |
. . . . . . . 8
    
      |
35 | 34 | ssrdv 3437 |
. . . . . . 7
    
    |
36 | 11, 35 | ssexd 4549 |
. . . . . 6
    
    |
37 | 36 | ex 436 |
. . . . 5
    

   |
38 | 37 | adantl 468 |
. . . 4
 
         |
39 | 12, 23, 20 | zorn2lem3 8925 |
. . . . . . . . . . . . . 14
  

  

           |
40 | 39 | exp45 618 |
. . . . . . . . . . . . 13
                   |
41 | 40 | com23 81 |
. . . . . . . . . . . 12
                   |
42 | 41 | imp 431 |
. . . . . . . . . . 11
 
                 |
43 | 42 | a2d 29 |
. . . . . . . . . 10
 
  



             |
44 | 43 | imp4a 593 |
. . . . . . . . 9
 
  

 
             |
45 | 44 | alrimdv 1774 |
. . . . . . . 8
 
  

                 |
46 | 45 | alimdv 1762 |
. . . . . . 7
 
                         |
47 | | r2al 2765 |
. . . . . . 7
 

       
                  |
48 | 46, 47 | syl6ibr 231 |
. . . . . 6
 
                   |
49 | | ssid 3450 |
. . . . . . . 8
 |
50 | 13 | tz7.48lem 7155 |
. . . . . . . 8
 


              |
51 | 49, 50 | mpan 675 |
. . . . . . 7
 

             |
52 | | fnrel 5672 |
. . . . . . . . . . 11
   |
53 | 13, 52 | ax-mp 5 |
. . . . . . . . . 10
 |
54 | | fndm 5673 |
. . . . . . . . . . . 12
   |
55 | 13, 54 | ax-mp 5 |
. . . . . . . . . . 11
 |
56 | 55 | eqimssi 3485 |
. . . . . . . . . 10
 |
57 | | relssres 5141 |
. . . . . . . . . 10
       |
58 | 53, 56, 57 | mp2an 677 |
. . . . . . . . 9
   |
59 | 58 | cnveqi 5008 |
. . . . . . . 8
 
   |
60 | 59 | funeqi 5601 |
. . . . . . 7
   
   |
61 | 51, 60 | sylib 200 |
. . . . . 6
 

           |
62 | 48, 61 | syl6 34 |
. . . . 5
 
          |
63 | | onprc 6608 |
. . . . . 6
 |
64 | | funrnex 6757 |
. . . . . . . 8
 
      |
65 | 64 | com12 32 |
. . . . . . 7
 
 
    |
66 | | df-rn 4844 |
. . . . . . . 8
  |
67 | 66 | eleq1i 2519 |
. . . . . . 7

   |
68 | | dfdm4 5026 |
. . . . . . . . 9
  |
69 | 55, 68 | eqtr3i 2474 |
. . . . . . . 8
  |
70 | 69 | eleq1i 2519 |
. . . . . . 7

   |
71 | 65, 67, 70 | 3imtr4g 274 |
. . . . . 6
 
    |
72 | 63, 71 | mtoi 182 |
. . . . 5
 
  |
73 | 62, 72 | syl6 34 |
. . . 4
 
         |
74 | 38, 73 | jcad 536 |
. . 3
 
           |
75 | 6, 74 | syl5bir 222 |
. 2
 
   
    |
76 | 1, 75 | mt3i 130 |
1
 
 
  |