Metamath Proof Explorer

Theorem isubgrupgr

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

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

Step	Hyp	Ref	Expression
1		isubgrupgr.v	$⊢ V = Vtx (G)$
2		upgruhgr	$⊢ G \in UPGraph \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 UPGraph \land S \subseteq V) \to (G ISubGr S) SubGraph G$
5		subupgr	$⊢ (G \in UPGraph \land (G ISubGr S) SubGraph G) \to G ISubGr S \in UPGraph$
6	4 5	syldan	$⊢ (G \in UPGraph \land S \subseteq V) \to G ISubGr S \in UPGraph$