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	$$⊢\left(G\in \mathrm{UHGraph}\wedge S\mathrm{SubGraph}G\right)\to \mathrm{Fun}\mathrm{iEdg}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{iEdg}\left(G\right)=\mathrm{iEdg}\left(G\right)$$
2	1	uhgrfun	$$⊢G\in \mathrm{UHGraph}\to \mathrm{Fun}\mathrm{iEdg}\left(G\right)$$
3		subgrfun	$$⊢\left(\mathrm{Fun}\mathrm{iEdg}\left(G\right)\wedge S\mathrm{SubGraph}G\right)\to \mathrm{Fun}\mathrm{iEdg}\left(S\right)$$
4	2 3	sylan	$$⊢\left(G\in \mathrm{UHGraph}\wedge S\mathrm{SubGraph}G\right)\to \mathrm{Fun}\mathrm{iEdg}\left(S\right)$$