Theorem isubgrumgr

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

	Ref	Expression
Hypothesis	isubgrupgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	isubgrumgr	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) ∈ UMGraph )

Proof

Step	Hyp	Ref	Expression
1		isubgrupgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		umgruhgr	⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph )
3	1	isubgrsubgr	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) SubGraph 𝐺 )
4	2 3	sylan	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) SubGraph 𝐺 )
5		subumgr	⊢ ( ( 𝐺 ∈ UMGraph ∧ ( 𝐺 ISubGr 𝑆 ) SubGraph 𝐺 ) → ( 𝐺 ISubGr 𝑆 ) ∈ UMGraph )
6	4 5	syldan	⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) ∈ UMGraph )