Metamath Proof Explorer

Theorem subgruhgrfun

Description: The edge function of a subgraph of a hypergraph is a function. (Contributed by AV, 16-Nov-2020) (Proof shortened by AV, 20-Nov-2020)

Ref Expression
Assertion subgruhgrfun 
|- ( ( G e. UHGraph /\ S SubGraph G ) -> Fun ( iEdg ` S ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
2 1 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
3 subgrfun 
 |-  ( ( Fun ( iEdg ` G ) /\ S SubGraph G ) -> Fun ( iEdg ` S ) )
4 2 3 sylan 
 |-  ( ( G e. UHGraph /\ S SubGraph G ) -> Fun ( iEdg ` S ) )