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 \in UHGraph \land S SubGraph G) \to Fun iEdg (S)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ iEdg (G) = iEdg (G)$
2	1	uhgrfun	$⊢ G \in UHGraph \to Fun iEdg (G)$
3		subgrfun	$⊢ (Fun iEdg (G) \land S SubGraph G) \to Fun iEdg (S)$
4	2 3	sylan	$⊢ (G \in UHGraph \land S SubGraph G) \to Fun iEdg (S)$