Metamath Proof Explorer

Theorem usgrss

Description: An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017) (Revised by AV, 15-Oct-2020)

Ref Expression
Hypotheses usgrf1o.e 
|- E = ( iEdg ` G )
usgrss.v 
|- V = ( Vtx ` G )
Assertion usgrss 
|- ( ( G e. USGraph /\ X e. dom E ) -> ( E ` X ) C_ V )

Proof

Step Hyp Ref Expression
1 usgrf1o.e 
 |-  E = ( iEdg ` G )
2 usgrss.v 
 |-  V = ( Vtx ` G )
3 ssrab2 
 |-  { x e. ~P V | ( # ` x ) = 2 } C_ ~P V
4 2 1 usgrfs 
 |-  ( G e. USGraph -> E : dom E -1-1-> { x e. ~P V | ( # ` x ) = 2 } )
5 f1f 
 |-  ( E : dom E -1-1-> { x e. ~P V | ( # ` x ) = 2 } -> E : dom E --> { x e. ~P V | ( # ` x ) = 2 } )
6 4 5 syl 
 |-  ( G e. USGraph -> E : dom E --> { x e. ~P V | ( # ` x ) = 2 } )
7 6 ffvelcdmda 
 |-  ( ( G e. USGraph /\ X e. dom E ) -> ( E ` X ) e. { x e. ~P V | ( # ` x ) = 2 } )
8 3 7 sselid 
 |-  ( ( G e. USGraph /\ X e. dom E ) -> ( E ` X ) e. ~P V )
9 8 elpwid 
 |-  ( ( G e. USGraph /\ X e. dom E ) -> ( E ` X ) C_ V )