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) \land S SubGraph G) \to 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 \to (Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S))$
7		funss	$⊢ iEdg (S) \subseteq iEdg (G) \to (Fun iEdg (G) \to Fun iEdg (S))$
8	7	3ad2ant2	$⊢ (Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \to (Fun iEdg (G) \to Fun iEdg (S))$
9	6 8	syl	$⊢ S SubGraph G \to (Fun iEdg (G) \to Fun iEdg (S))$
10	9	impcom	$⊢ (Fun iEdg (G) \land S SubGraph G) \to Fun iEdg (S)$