| Step | Hyp | Ref | Expression | 
						
							| 1 |  | f1oi |  | 
						
							| 2 |  | f1of1 |  | 
						
							| 3 | 1 2 | mp1i |  | 
						
							| 4 |  | simpllr |  | 
						
							| 5 |  | fveq2 |  | 
						
							| 6 |  | 0red |  | 
						
							| 7 |  | elfznn |  | 
						
							| 8 | 7 | nngt0d |  | 
						
							| 9 | 6 8 | ltned |  | 
						
							| 10 |  | c0ex |  | 
						
							| 11 |  | vex |  | 
						
							| 12 | 10 11 | pm3.2i |  | 
						
							| 13 |  | hashprg |  | 
						
							| 14 | 12 13 | mp1i |  | 
						
							| 15 | 9 14 | mpbid |  | 
						
							| 16 | 15 | adantl |  | 
						
							| 17 | 5 16 | sylan9eqr |  | 
						
							| 18 | 4 17 | jca |  | 
						
							| 19 | 18 | ex |  | 
						
							| 20 | 19 | rexlimdva |  | 
						
							| 21 | 20 | expimpd |  | 
						
							| 22 |  | eqeq1 |  | 
						
							| 23 | 22 | rexbidv |  | 
						
							| 24 | 23 | elrab |  | 
						
							| 25 |  | fveqeq2 |  | 
						
							| 26 | 25 | elrab |  | 
						
							| 27 | 21 24 26 | 3imtr4g |  | 
						
							| 28 | 27 | ssrdv |  | 
						
							| 29 |  | f1ss |  | 
						
							| 30 | 3 28 29 | syl2anc |  | 
						
							| 31 |  | stgriedg | Could not format  ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) : No typesetting found for |- ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) with typecode |- | 
						
							| 32 | 31 | dmeqd | Could not format  ( N e. NN0 -> dom ( iEdg ` ( StarGr ` N ) ) = dom ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) : No typesetting found for |- ( N e. NN0 -> dom ( iEdg ` ( StarGr ` N ) ) = dom ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) with typecode |- | 
						
							| 33 |  | dmresi |  | 
						
							| 34 | 32 33 | eqtrdi | Could not format  ( N e. NN0 -> dom ( iEdg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : No typesetting found for |- ( N e. NN0 -> dom ( iEdg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) with typecode |- | 
						
							| 35 |  | stgrvtx | Could not format  ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) ) : No typesetting found for |- ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) ) with typecode |- | 
						
							| 36 | 35 | pweqd | Could not format  ( N e. NN0 -> ~P ( Vtx ` ( StarGr ` N ) ) = ~P ( 0 ... N ) ) : No typesetting found for |- ( N e. NN0 -> ~P ( Vtx ` ( StarGr ` N ) ) = ~P ( 0 ... N ) ) with typecode |- | 
						
							| 37 | 36 | rabeqdv | Could not format  ( N e. NN0 -> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } = { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } ) : No typesetting found for |- ( N e. NN0 -> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } = { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } ) with typecode |- | 
						
							| 38 | 31 34 37 | f1eq123d | Could not format  ( N e. NN0 -> ( ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } <-> ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } -1-1-> { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } ) ) : No typesetting found for |- ( N e. NN0 -> ( ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } <-> ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } -1-1-> { e e. ~P ( 0 ... N ) | ( # ` e ) = 2 } ) ) with typecode |- | 
						
							| 39 | 30 38 | mpbird | Could not format  ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) : No typesetting found for |- ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) with typecode |- | 
						
							| 40 |  | fvex | Could not format  ( StarGr ` N ) e. _V : No typesetting found for |- ( StarGr ` N ) e. _V with typecode |- | 
						
							| 41 |  | eqid | Could not format  ( Vtx ` ( StarGr ` N ) ) = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for |- ( Vtx ` ( StarGr ` N ) ) = ( Vtx ` ( StarGr ` N ) ) with typecode |- | 
						
							| 42 |  | eqid | Could not format  ( iEdg ` ( StarGr ` N ) ) = ( iEdg ` ( StarGr ` N ) ) : No typesetting found for |- ( iEdg ` ( StarGr ` N ) ) = ( iEdg ` ( StarGr ` N ) ) with typecode |- | 
						
							| 43 | 41 42 | isusgrs | Could not format  ( ( StarGr ` N ) e. _V -> ( ( StarGr ` N ) e. USGraph <-> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) ) : No typesetting found for |- ( ( StarGr ` N ) e. _V -> ( ( StarGr ` N ) e. USGraph <-> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) ) with typecode |- | 
						
							| 44 | 40 43 | mp1i | Could not format  ( N e. NN0 -> ( ( StarGr ` N ) e. USGraph <-> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) ) : No typesetting found for |- ( N e. NN0 -> ( ( StarGr ` N ) e. USGraph <-> ( iEdg ` ( StarGr ` N ) ) : dom ( iEdg ` ( StarGr ` N ) ) -1-1-> { e e. ~P ( Vtx ` ( StarGr ` N ) ) | ( # ` e ) = 2 } ) ) with typecode |- | 
						
							| 45 | 39 44 | mpbird | Could not format  ( N e. NN0 -> ( StarGr ` N ) e. USGraph ) : No typesetting found for |- ( N e. NN0 -> ( StarGr ` N ) e. USGraph ) with typecode |- |