Metamath Proof Explorer

Theorem subgrfun

Description: The edge function of a subgraph of a graph whose edge function is actually a function is a function. (Contributed by AV, 20-Nov-2020)

Ref Expression
Assertion subgrfun 
|- ( ( Fun ( iEdg ` G ) /\ S SubGraph G ) -> Fun ( iEdg ` S ) )

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 funss 
 |-  ( ( iEdg ` S ) C_ ( iEdg ` G ) -> ( Fun ( iEdg ` G ) -> Fun ( iEdg ` S ) ) )
8 7 3ad2ant2 
 |-  ( ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) -> ( Fun ( iEdg ` G ) -> Fun ( iEdg ` S ) ) )
9 6 8 syl 
 |-  ( S SubGraph G -> ( Fun ( iEdg ` G ) -> Fun ( iEdg ` S ) ) )
10 9 impcom 
 |-  ( ( Fun ( iEdg ` G ) /\ S SubGraph G ) -> Fun ( iEdg ` S ) )