| Step | Hyp | Ref | Expression | 
						
							| 0 |  | cstgr | Could not format  StarGr : No typesetting found for class StarGr with typecode class | 
						
							| 1 |  | vn |  | 
						
							| 2 |  | cn0 |  | 
						
							| 3 |  | cbs |  | 
						
							| 4 |  | cnx |  | 
						
							| 5 | 4 3 | cfv |  | 
						
							| 6 |  | cc0 |  | 
						
							| 7 |  | cfz |  | 
						
							| 8 | 1 | cv |  | 
						
							| 9 | 6 8 7 | co |  | 
						
							| 10 | 5 9 | cop |  | 
						
							| 11 |  | cedgf |  | 
						
							| 12 | 4 11 | cfv |  | 
						
							| 13 |  | cid |  | 
						
							| 14 |  | ve |  | 
						
							| 15 | 9 | cpw |  | 
						
							| 16 |  | vx |  | 
						
							| 17 |  | c1 |  | 
						
							| 18 | 17 8 7 | co |  | 
						
							| 19 | 14 | cv |  | 
						
							| 20 | 16 | cv |  | 
						
							| 21 | 6 20 | cpr |  | 
						
							| 22 | 19 21 | wceq |  | 
						
							| 23 | 22 16 18 | wrex |  | 
						
							| 24 | 23 14 15 | crab |  | 
						
							| 25 | 13 24 | cres |  | 
						
							| 26 | 12 25 | cop |  | 
						
							| 27 | 10 26 | cpr |  | 
						
							| 28 | 1 2 27 | cmpt |  | 
						
							| 29 | 0 28 | wceq | Could not format  StarGr = ( n e. NN0 |-> { <. ( Base ` ndx ) , ( 0 ... n ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) >. } ) : No typesetting found for wff StarGr = ( n e. NN0 |-> { <. ( Base ` ndx ) , ( 0 ... n ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) >. } ) with typecode wff |