Metamath Proof Explorer

Theorem isubgrumgr

Description: An induced subgraph of a multigraph is a multigraph. (Contributed by AV, 15-May-2025)

		Ref	Expression
	Hypothesis	isubgrupgr.v	$⊢ V = Vtx (G)$
	Assertion	isubgrumgr	$⊢ (G \in UMGraph \land S \subseteq V) \to G ISubGr S \in UMGraph$

Step	Hyp	Ref	Expression
1		isubgrupgr.v	$⊢ V = Vtx (G)$
2		umgruhgr	$⊢ G \in UMGraph \to G \in UHGraph$
3	1	isubgrsubgr	$⊢ (G \in UHGraph \land S \subseteq V) \to (G ISubGr S) SubGraph G$
4	2 3	sylan	$⊢ (G \in UMGraph \land S \subseteq V) \to (G ISubGr S) SubGraph G$
5		subumgr	$⊢ (G \in UMGraph \land (G ISubGr S) SubGraph G) \to G ISubGr S \in UMGraph$
6	4 5	syldan	$⊢ (G \in UMGraph \land S \subseteq V) \to G ISubGr S \in UMGraph$