Metamath Proof Explorer

Theorem subgreldmiedg

Description: An element of the domain of the edge function of a subgraph is an element of the domain of the edge function of the supergraph. (Contributed by AV, 20-Nov-2020)

Ref Expression
Assertion subgreldmiedg 
|- ( ( S SubGraph G /\ X e. dom ( iEdg ` S ) ) -> X e. dom ( iEdg ` G ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` S ) = ( Vtx ` S )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 eqid 
 |-  ( iEdg ` S ) = ( iEdg ` S )
4 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
5 eqid 
 |-  ( Edg ` S ) = ( Edg ` S )
6 1 2 3 4 5 subgrprop2 
 |-  ( S SubGraph G -> ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) )
7 dmss 
 |-  ( ( iEdg ` S ) C_ ( iEdg ` G ) -> dom ( iEdg ` S ) C_ dom ( iEdg ` G ) )
8 7 3ad2ant2 
 |-  ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) -> dom ( iEdg ` S ) C_ dom ( iEdg ` G ) )
9 8 sseld 
 |-  ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) -> ( X e. dom ( iEdg ` S ) -> X e. dom ( iEdg ` G ) ) )
10 6 9 syl 
 |-  ( S SubGraph G -> ( X e. dom ( iEdg ` S ) -> X e. dom ( iEdg ` G ) ) )
11 10 imp 
 |-  ( ( S SubGraph G /\ X e. dom ( iEdg ` S ) ) -> X e. dom ( iEdg ` G ) )