Step | Hyp | Ref
| Expression |
1 | | bnj1408.3 |
. . . 4
 
   |
2 | 1 | biimpri 198 |
. . 3
 
   |
3 | | bnj1408.1 |
. . . . 5
   
             |
4 | 3 | bnj1413 29110 |
. . . 4
 
   |
5 | | simplll 735 |
. . . . . . . . 9
    
    
 
  |
6 | | bnj213 28959 |
. . . . . . . . . . 11
  
   |
7 | 6 | sseli 3304 |
. . . . . . . . . 10
    
   |
8 | 7 | adantl 453 |
. . . . . . . . 9
    
    
 
  |
9 | | bnj906 29007 |
. . . . . . . . 9
 
             |
10 | 5, 8, 9 | syl2anc 643 |
. . . . . . . 8
    
    
 
    
       |
11 | | bnj1318 29100 |
. . . . . . . . . . 11
             |
12 | 11 | ssiun2s 4095 |
. . . . . . . . . 10
    
                  |
13 | | ssun4 3473 |
. . . . . . . . . . 11
        
                
            |
14 | 13, 3 | syl6sseqr 3355 |
. . . . . . . . . 10
        
             |
15 | 12, 14 | syl 16 |
. . . . . . . . 9
    
        |
16 | 15 | adantl 453 |
. . . . . . . 8
    
    
 
    
  |
17 | 10, 16 | sstrd 3318 |
. . . . . . 7
    
    
 
    
  |
18 | | simpr 448 |
. . . . . . . . . . 11
    
               
        |
19 | 18 | bnj1405 28914 |
. . . . . . . . . 10
    
            
            |
20 | | biid 228 |
. . . . . . . . . 10
    
            
    
     
    
           
    
        |
21 | | nfv 1626 |
. . . . . . . . . . . . 13
  
  |
22 | | nfcv 2540 |
. . . . . . . . . . . . . . . 16
       |
23 | | nfiu1 4081 |
. . . . . . . . . . . . . . . 16
  
          |
24 | 22, 23 | nfun 3463 |
. . . . . . . . . . . . . . 15
     
             |
25 | 3, 24 | nfcxfr 2537 |
. . . . . . . . . . . . . 14
   |
26 | 25 | nfcri 2534 |
. . . . . . . . . . . . 13
  |
27 | 21, 26 | nfan 1842 |
. . . . . . . . . . . 12
    
  |
28 | 23 | nfcri 2534 |
. . . . . . . . . . . 12
    
       |
29 | 27, 28 | nfan 1842 |
. . . . . . . . . . 11
    
              |
30 | 29 | nfri 1774 |
. . . . . . . . . 10
    
                


  
          |
31 | 19, 20, 30 | bnj1521 28928 |
. . . . . . . . 9
    
                 

           
    
        |
32 | | simplll 735 |
. . . . . . . . . . . . 13
    
              |
33 | 32 | 3ad2ant1 978 |
. . . . . . . . . . . 12
    
            
    
        |
34 | | bnj1147 29069 |
. . . . . . . . . . . . 13
      |
35 | | simp3 959 |
. . . . . . . . . . . . 13
    
            
    
             |
36 | 34, 35 | bnj1213 28876 |
. . . . . . . . . . . 12
    
            
    
        |
37 | 33, 36, 9 | syl2anc 643 |
. . . . . . . . . . 11
    
            
    
                  |
38 | | simp2 958 |
. . . . . . . . . . . . 13
    
            
    
        
    |
39 | 6, 38 | bnj1213 28876 |
. . . . . . . . . . . 12
    
            
    
        |
40 | | bnj1125 29067 |
. . . . . . . . . . . 12
 
                  |
41 | 33, 39, 35, 40 | syl3anc 1184 |
. . . . . . . . . . 11
    
            
    
                  |
42 | 37, 41 | sstrd 3318 |
. . . . . . . . . 10
    
            
    
                  |
43 | | ssiun2 4094 |
. . . . . . . . . . . 12
    
                  |
44 | 43 | 3ad2ant2 979 |
. . . . . . . . . . 11
    
            
    
              
        |
45 | | ssun4 3473 |
. . . . . . . . . . . 12
        
                
            |
46 | 45, 3 | syl6sseqr 3355 |
. . . . . . . . . . 11
        
             |
47 | 44, 46 | syl 16 |
. . . . . . . . . 10
    
            
    
             |
48 | 42, 47 | sstrd 3318 |
. . . . . . . . 9
    
            
    
             |
49 | 31, 48 | bnj593 28819 |
. . . . . . . 8
    
            
    
  |
50 | | nfcv 2540 |
. . . . . . . . . 10
       |
51 | 50, 25 | nfss 3301 |
. . . . . . . . 9
       |
52 | 51 | nfri 1774 |
. . . . . . . 8
             |
53 | 49, 52 | bnj1397 28912 |
. . . . . . 7
    
                   |
54 | | simpr 448 |
. . . . . . . 8
  

   |
55 | 3 | bnj1138 28865 |
. . . . . . . 8

    

   
         |
56 | 54, 55 | sylib 189 |
. . . . . . 7
  

    
               |
57 | 17, 53, 56 | mpjaodan 762 |
. . . . . 6
  

        |
58 | 57 | ralrimiva 2749 |
. . . . 5
 
         |
59 | | df-bnj19 28767 |
. . . . 5
    

    
  |
60 | 58, 59 | sylibr 204 |
. . . 4
 
    
   |
61 | 3 | bnj931 28847 |
. . . . 5
  
   |
62 | 61 | a1i 11 |
. . . 4
 
    
   |
63 | | bnj1408.4 |
. . . 4
               |
64 | 4, 60, 62, 63 | syl3anbrc 1138 |
. . 3
 
   |
65 | 1, 63 | bnj1124 29063 |
. . 3
      
   |
66 | 2, 64, 65 | syl2anc 643 |
. 2
 
    
   |
67 | | bnj906 29007 |
. . . . 5
 
    
    
   |
68 | | iunss1 4064 |
. . . . 5
       
     
         
        |
69 | | unss2 3478 |
. . . . 5
 
                        
         
     
            |
70 | 67, 68, 69 | 3syl 19 |
. . . 4
 
    
               
              |
71 | | bnj1408.2 |
. . . 4
   
             |
72 | 70, 3, 71 | 3sstr4g 3349 |
. . 3
 

  |
73 | | biid 228 |
. . . 4
 
 
   |
74 | | biid 228 |
. . . 4
             
    
    
   |
75 | 71, 73, 74 | bnj1136 29072 |
. . 3
 
    
   |
76 | 72, 75 | sseqtr4d 3345 |
. 2
 

       |
77 | 66, 76 | eqssd 3325 |
1
 
    
   |