Proof of Theorem frgra3vlem1
Step | Hyp | Ref
| Expression |
1 | | vex 3047 |
. . . . . 6
 |
2 | 1 | eltp 4016 |
. . . . 5
   
 
   |
3 | | vex 3047 |
. . . . . . . . 9
 |
4 | 3 | eltp 4016 |
. . . . . . . 8
   
 
   |
5 | | eqidd 2451 |
. . . . . . . . . . . . . . 15
           
USGrph 
  |
6 | 5 | a1i 11 |
. . . . . . . . . . . . . 14
     
   
           
USGrph 
   |
7 | 6 | 2a1i 12 |
. . . . . . . . . . . . 13
      
   
         
   
 
   
 
USGrph 
     |
8 | | preq1 4050 |
. . . . . . . . . . . . . . 15
         |
9 | | preq1 4050 |
. . . . . . . . . . . . . . 15
         |
10 | 8, 9 | preq12d 4058 |
. . . . . . . . . . . . . 14
         
           |
11 | 10 | sseq1d 3458 |
. . . . . . . . . . . . 13
      
                |
12 | | eqeq2 2461 |
. . . . . . . . . . . . . . 15
 
   |
13 | 12 | imbi2d 318 |
. . . . . . . . . . . . . 14
     
 
   
 
USGrph 
    
       
USGrph 
    |
14 | 13 | imbi2d 318 |
. . . . . . . . . . . . 13
         
     
 
   
 
USGrph 
     
     
   
 
   
 
USGrph 
     |
15 | 7, 11, 14 | 3imtr4d 272 |
. . . . . . . . . . . 12
      
   
         
   
 
   
 
USGrph 
     |
16 | | prex 4641 |
. . . . . . . . . . . . . . . . 17
    |
17 | | prex 4641 |
. . . . . . . . . . . . . . . . 17
    |
18 | 16, 17 | prss 4125 |
. . . . . . . . . . . . . . . 16
    
   
      
    |
19 | | usgraedgrn 25101 |
. . . . . . . . . . . . . . . . . . 19
      USGrph
      |
20 | | df-ne 2623 |
. . . . . . . . . . . . . . . . . . . 20

  |
21 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . 21
 |
22 | 21 | pm2.24i 137 |
. . . . . . . . . . . . . . . . . . . 20

  |
23 | 20, 22 | sylbi 199 |
. . . . . . . . . . . . . . . . . . 19
   |
24 | 19, 23 | syl 17 |
. . . . . . . . . . . . . . . . . 18
      USGrph
   
  |
25 | 24 | expcom 437 |
. . . . . . . . . . . . . . . . 17
        
USGrph    |
26 | 25 | adantr 467 |
. . . . . . . . . . . . . . . 16
    
       
 USGrph    |
27 | 18, 26 | sylbir 217 |
. . . . . . . . . . . . . . 15
     
   
  
 
USGrph    |
28 | 27 | adantld 469 |
. . . . . . . . . . . . . 14
     
   
           
USGrph 
   |
29 | 28 | 2a1i 12 |
. . . . . . . . . . . . 13
      
   
         
   
 
   
 
USGrph 
     |
30 | | preq1 4050 |
. . . . . . . . . . . . . . 15
         |
31 | | preq1 4050 |
. . . . . . . . . . . . . . 15
         |
32 | 30, 31 | preq12d 4058 |
. . . . . . . . . . . . . 14
         
           |
33 | 32 | sseq1d 3458 |
. . . . . . . . . . . . 13
      
                |
34 | | eqeq2 2461 |
. . . . . . . . . . . . . . 15
 
   |
35 | 34 | imbi2d 318 |
. . . . . . . . . . . . . 14
     
 
   
 
USGrph 
    
       
USGrph 
    |
36 | 35 | imbi2d 318 |
. . . . . . . . . . . . 13
         
     
 
   
 
USGrph 
     
     
   
 
   
 
USGrph 
     |
37 | 29, 33, 36 | 3imtr4d 272 |
. . . . . . . . . . . 12
      
   
         
   
 
   
 
USGrph 
     |
38 | 21 | pm2.24i 137 |
. . . . . . . . . . . . . . . . . . . 20

  |
39 | 20, 38 | sylbi 199 |
. . . . . . . . . . . . . . . . . . 19
   |
40 | 19, 39 | syl 17 |
. . . . . . . . . . . . . . . . . 18
      USGrph
   
  |
41 | 40 | expcom 437 |
. . . . . . . . . . . . . . . . 17
        
USGrph    |
42 | 41 | adantr 467 |
. . . . . . . . . . . . . . . 16
    
       
 USGrph    |
43 | 18, 42 | sylbir 217 |
. . . . . . . . . . . . . . 15
     
   
  
 
USGrph    |
44 | 43 | adantld 469 |
. . . . . . . . . . . . . 14
     
   
           
USGrph 
   |
45 | 44 | 2a1i 12 |
. . . . . . . . . . . . 13
      
   
         
   
 
   
 
USGrph 
     |
46 | | preq1 4050 |
. . . . . . . . . . . . . . 15
         |
47 | | preq1 4050 |
. . . . . . . . . . . . . . 15
         |
48 | 46, 47 | preq12d 4058 |
. . . . . . . . . . . . . 14
         
           |
49 | 48 | sseq1d 3458 |
. . . . . . . . . . . . 13
      
                |
50 | | eqeq2 2461 |
. . . . . . . . . . . . . . 15
 
   |
51 | 50 | imbi2d 318 |
. . . . . . . . . . . . . 14
     
 
   
 
USGrph 
    
       
USGrph 
    |
52 | 51 | imbi2d 318 |
. . . . . . . . . . . . 13
         
     
 
   
 
USGrph 
     
     
   
 
   
 
USGrph 
     |
53 | 45, 49, 52 | 3imtr4d 272 |
. . . . . . . . . . . 12
      
   
         
   
 
   
 
USGrph 
     |
54 | 15, 37, 53 | 3jaoi 1330 |
. . . . . . . . . . 11
 
          
       
     
 
   
 
USGrph 
     |
55 | | preq1 4050 |
. . . . . . . . . . . . . . 15
     
   |
56 | | preq1 4050 |
. . . . . . . . . . . . . . 15
     
   |
57 | 55, 56 | preq12d 4058 |
. . . . . . . . . . . . . 14
         
           |
58 | 57 | sseq1d 3458 |
. . . . . . . . . . . . 13
      
                |
59 | | eqeq1 2454 |
. . . . . . . . . . . . . 14
 
   |
60 | 59 | imbi2d 318 |
. . . . . . . . . . . . 13
     
 
   
 
USGrph 
    
       
USGrph 
    |
61 | 58, 60 | imbi12d 322 |
. . . . . . . . . . . 12
               
 
   
 
USGrph 
     
     
   
 
   
 
USGrph 
     |
62 | 61 | imbi2d 318 |
. . . . . . . . . . 11
           
             
 
   
 
USGrph 
  
     
   
         
   
 
   
 
USGrph 
      |
63 | 54, 62 | syl5ibr 225 |
. . . . . . . . . 10
   
     
   
     
   
           
USGrph 
      |
64 | | prex 4641 |
. . . . . . . . . . . . . . . . 17
    |
65 | | prex 4641 |
. . . . . . . . . . . . . . . . 17
    |
66 | 64, 65 | prss 4125 |
. . . . . . . . . . . . . . . 16
    
   
      
    |
67 | | usgraedgrn 25101 |
. . . . . . . . . . . . . . . . . . 19
      USGrph
      |
68 | | df-ne 2623 |
. . . . . . . . . . . . . . . . . . . 20

  |
69 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . 21
 |
70 | 69 | pm2.24i 137 |
. . . . . . . . . . . . . . . . . . . 20

  |
71 | 68, 70 | sylbi 199 |
. . . . . . . . . . . . . . . . . . 19
   |
72 | 67, 71 | syl 17 |
. . . . . . . . . . . . . . . . . 18
      USGrph
   
  |
73 | 72 | expcom 437 |
. . . . . . . . . . . . . . . . 17
        
USGrph    |
74 | 73 | adantl 468 |
. . . . . . . . . . . . . . . 16
    
       
 USGrph    |
75 | 66, 74 | sylbir 217 |
. . . . . . . . . . . . . . 15
     
   
  
 
USGrph    |
76 | 75 | adantld 469 |
. . . . . . . . . . . . . 14
     
   
           
USGrph 
   |
77 | 76 | 2a1i 12 |
. . . . . . . . . . . . 13
      
   
         
   
 
   
 
USGrph 
     |
78 | | eqeq2 2461 |
. . . . . . . . . . . . . . 15
 
   |
79 | 78 | imbi2d 318 |
. . . . . . . . . . . . . 14
     
 
   
 
USGrph 
    
       
USGrph 
    |
80 | 79 | imbi2d 318 |
. . . . . . . . . . . . 13
         
     
 
   
 
USGrph 
     
     
   
 
   
 
USGrph 
     |
81 | 77, 11, 80 | 3imtr4d 272 |
. . . . . . . . . . . 12
      
   
         
   
 
   
 
USGrph 
     |
82 | | eqidd 2451 |
. . . . . . . . . . . . . . 15
           
USGrph 
  |
83 | 82 | a1i 11 |
. . . . . . . . . . . . . 14
     
   
           
USGrph 
   |
84 | 83 | 2a1i 12 |
. . . . . . . . . . . . 13
      
   
         
   
 
   
 
USGrph 
     |
85 | | eqeq2 2461 |
. . . . . . . . . . . . . . 15
 
   |
86 | 85 | imbi2d 318 |
. . . . . . . . . . . . . 14
     
 
   
 
USGrph 
    
       
USGrph 
    |
87 | 86 | imbi2d 318 |
. . . . . . . . . . . . 13
         
     
 
   
 
USGrph 
     
     
   
 
   
 
USGrph 
     |
88 | 84, 33, 87 | 3imtr4d 272 |
. . . . . . . . . . . 12
      
   
         
   
 
   
 
USGrph 
     |
89 | 69 | pm2.24i 137 |
. . . . . . . . . . . . . . . . . . . 20

  |
90 | 68, 89 | sylbi 199 |
. . . . . . . . . . . . . . . . . . 19
   |
91 | 67, 90 | syl 17 |
. . . . . . . . . . . . . . . . . 18
      USGrph
   
  |
92 | 91 | expcom 437 |
. . . . . . . . . . . . . . . . 17
        
USGrph    |
93 | 92 | adantl 468 |
. . . . . . . . . . . . . . . 16
    
       
 USGrph    |
94 | 66, 93 | sylbir 217 |
. . . . . . . . . . . . . . 15
     
   
  
 
USGrph    |
95 | 94 | adantld 469 |
. . . . . . . . . . . . . 14
     
   
           
USGrph 
   |
96 | 95 | 2a1i 12 |
. . . . . . . . . . . . 13
      
   
         
   
 
   
 
USGrph 
     |
97 | | eqeq2 2461 |
. . . . . . . . . . . . . . 15
 
   |
98 | 97 | imbi2d 318 |
. . . . . . . . . . . . . 14
     
 
   
 
USGrph 
    
       
USGrph 
    |
99 | 98 | imbi2d 318 |
. . . . . . . . . . . . 13
         
     
 
   
 
USGrph 
     
     
   
 
   
 
USGrph 
     |
100 | 96, 49, 99 | 3imtr4d 272 |
. . . . . . . . . . . 12
      
   
         
   
 
   
 
USGrph 
     |
101 | 81, 88, 100 | 3jaoi 1330 |
. . . . . . . . . . 11
 
          
       
     
 
   
 
USGrph 
     |
102 | | preq1 4050 |
. . . . . . . . . . . . . . 15
     
   |
103 | | preq1 4050 |
. . . . . . . . . . . . . . 15
     
   |
104 | 102, 103 | preq12d 4058 |
. . . . . . . . . . . . . 14
         
           |
105 | 104 | sseq1d 3458 |
. . . . . . . . . . . . 13
      
                |
106 | | eqeq1 2454 |
. . . . . . . . . . . . . 14
 
   |
107 | 106 | imbi2d 318 |
. . . . . . . . . . . . 13
     
 
   
 
USGrph 
    
       
USGrph 
    |
108 | 105, 107 | imbi12d 322 |
. . . . . . . . . . . 12
               
 
   
 
USGrph 
     
     
   
 
   
 
USGrph 
     |
109 | 108 | imbi2d 318 |
. . . . . . . . . . 11
           
             
 
   
 
USGrph 
  
     
   
         
   
 
   
 
USGrph 
      |
110 | 101, 109 | syl5ibr 225 |
. . . . . . . . . 10
   
     
   
     
   
           
USGrph 
      |
111 | 21 | pm2.24i 137 |
. . . . . . . . . . . . . . . . . . . . 21

  |
112 | 20, 111 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . 20
   |
113 | 19, 112 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
      USGrph
   
  |
114 | 113 | expcom 437 |
. . . . . . . . . . . . . . . . . 18
        
USGrph    |
115 | 114 | adantr 467 |
. . . . . . . . . . . . . . . . 17
    
       
 USGrph    |
116 | 18, 115 | sylbir 217 |
. . . . . . . . . . . . . . . 16
     
   
  
 
USGrph    |
117 | 116 | adantld 469 |
. . . . . . . . . . . . . . 15
     
   
           
USGrph 
   |
118 | 117 | a1d 26 |
. . . . . . . . . . . . . 14
     
   
         
   
 
   
 
USGrph 
    |
119 | 118 | a1i 11 |
. . . . . . . . . . . . 13
      
   
         
   
 
   
 
USGrph 
     |
120 | | eqeq2 2461 |
. . . . . . . . . . . . . . 15
 
   |
121 | 120 | imbi2d 318 |
. . . . . . . . . . . . . 14
     
 
   
 
USGrph 
    
       
USGrph 
    |
122 | 121 | imbi2d 318 |
. . . . . . . . . . . . 13
         
     
 
   
 
USGrph 
     
     
   
 
   
 
USGrph 
     |
123 | 119, 11, 122 | 3imtr4d 272 |
. . . . . . . . . . . 12
      
   
         
   
 
   
 
USGrph 
     |
124 | | pm2.21 112 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
     |
125 | 68, 124 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 

    |
126 | 67, 69, 125 | mpisyl 21 |
. . . . . . . . . . . . . . . . . . . . . 22
      USGrph
          |
127 | 126 | expcom 437 |
. . . . . . . . . . . . . . . . . . . . 21
        
USGrph  

    |
128 | 127 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
    
       
 USGrph  
     |
129 | 66, 128 | sylbir 217 |
. . . . . . . . . . . . . . . . . . 19
     
   
  
 
USGrph  

    |
130 | 129 | com13 83 |
. . . . . . . . . . . . . . . . . 18
 
    
 USGrph    
     
    |
131 | 130 | adantr 467 |
. . . . . . . . . . . . . . . . 17
  


      
USGrph      
   
    |
132 | 131 | imp 431 |
. . . . . . . . . . . . . . . 16
           
USGrph         
 
   |
133 | 132 | com12 32 |
. . . . . . . . . . . . . . 15
     
   
           
USGrph 
   |
134 | 133 | a1d 26 |
. . . . . . . . . . . . . 14
     
   
         
   
 
   
 
USGrph 
    |
135 | 134 | a1i 11 |
. . . . . . . . . . . . 13
      
   
         
   
 
   
 
USGrph 
     |
136 | | eqeq2 2461 |
. . . . . . . . . . . . . . 15
 
   |
137 | 136 | imbi2d 318 |
. . . . . . . . . . . . . 14
     
 
   
 
USGrph 
    
       
USGrph 
    |
138 | 137 | imbi2d 318 |
. . . . . . . . . . . . 13
         
     
 
   
 
USGrph 
     
     
   
 
   
 
USGrph 
     |
139 | 135, 33, 138 | 3imtr4d 272 |
. . . . . . . . . . . 12
      
   
         
   
 
   
 
USGrph 
     |
140 | | eqidd 2451 |
. . . . . . . . . . . . . . 15
           
USGrph 
  |
141 | 140 | a1i 11 |
. . . . . . . . . . . . . 14
     
   
           
USGrph 
   |
142 | 141 | 2a1i 12 |
. . . . . . . . . . . . 13
      
   
         
   
 
   
 
USGrph 
     |
143 | | eqeq2 2461 |
. . . . . . . . . . . . . . 15
 
   |
144 | 143 | imbi2d 318 |
. . . . . . . . . . . . . 14
     
 
   
 
USGrph 
    
       
USGrph 
    |
145 | 144 | imbi2d 318 |
. . . . . . . . . . . . 13
         
     
 
   
 
USGrph 
     
     
   
 
   
 
USGrph 
     |
146 | 142, 49, 145 | 3imtr4d 272 |
. . . . . . . . . . . 12
      
   
         
   
 
   
 
USGrph 
     |
147 | 123, 139,
146 | 3jaoi 1330 |
. . . . . . . . . . 11
 
          
       
     
 
   
 
USGrph 
     |
148 | | preq1 4050 |
. . . . . . . . . . . . . . 15
     
   |
149 | | preq1 4050 |
. . . . . . . . . . . . . . 15
     
   |
150 | 148, 149 | preq12d 4058 |
. . . . . . . . . . . . . 14
         
           |
151 | 150 | sseq1d 3458 |
. . . . . . . . . . . . 13
      
                |
152 | | eqeq1 2454 |
. . . . . . . . . . . . . 14
 
   |
153 | 152 | imbi2d 318 |
. . . . . . . . . . . . 13
     
 
   
 
USGrph 
    
       
USGrph 
    |
154 | 151, 153 | imbi12d 322 |
. . . . . . . . . . . 12
               
 
   
 
USGrph 
     
     
   
 
   
 
USGrph 
     |
155 | 154 | imbi2d 318 |
. . . . . . . . . . 11
           
             
 
   
 
USGrph 
  
     
   
         
   
 
   
 
USGrph 
      |
156 | 147, 155 | syl5ibr 225 |
. . . . . . . . . 10
   
     
   
     
   
           
USGrph 
      |
157 | 63, 110, 156 | 3jaoi 1330 |
. . . . . . . . 9
 
         
   
     
   
           
USGrph 
      |
158 | 157 | com3l 84 |
. . . . . . . 8
 
          
        
   
           
USGrph 
      |
159 | 4, 158 | sylbi 199 |
. . . . . . 7
   
          
        
   
           
USGrph 
      |
160 | 159 | imp 431 |
. . . . . 6
                 
      
   
           
USGrph 
     |
161 | 160 | com3l 84 |
. . . . 5
 
                     
        
       
USGrph 
     |
162 | 2, 161 | sylbi 199 |
. . . 4
   
                     
        
       
USGrph 
     |
163 | 162 | imp31 434 |
. . 3
    
 
        

         
         
 
   
 
USGrph 
   |
164 | 163 | com12 32 |
. 2
           
USGrph       
                    
     
   |
165 | 164 | alrimivv 1773 |
1
           
USGrph                 
                    
   |