subumgr

Description: A subgraph of a multigraph is a multigraph. (Contributed by AV, 26-Nov-2020)

		Ref	Expression
	Assertion	subumgr	$⊢ (G \in UMGraph \land S SubGraph G) \to S \in UMGraph$

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		umgruhgr	$⊢ G \in UMGraph \to G \in UHGraph$
8		subgruhgrfun	$⊢ (G \in UHGraph \land S SubGraph G) \to Fun iEdg (S)$
9	7 8	sylan	$⊢ (G \in UMGraph \land S SubGraph G) \to Fun iEdg (S)$
10	9	ancoms	$⊢ (S SubGraph G \land G \in UMGraph) \to Fun iEdg (S)$
11	10	funfnd	$⊢ (S SubGraph G \land G \in UMGraph) \to iEdg (S) Fn dom iEdg (S)$
12	11	adantl	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UMGraph)) \to iEdg (S) Fn dom iEdg (S)$
13		simplrl	$⊢ (((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UMGraph)) \land x \in dom iEdg (S)) \to S SubGraph G$
14		simplrr	$⊢ (((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UMGraph)) \land x \in dom iEdg (S)) \to G \in UMGraph$
15		simpr	$⊢ (((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UMGraph)) \land x \in dom iEdg (S)) \to x \in dom iEdg (S)$
16	1 3	subumgredg2	$⊢ (S SubGraph G \land G \in UMGraph \land x \in dom iEdg (S)) \to iEdg (S) (x) \in \{e \in 𝒫 Vtx (S) \| \|e\| = 2\}$
17	13 14 15 16	syl3anc	$⊢ (((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UMGraph)) \land x \in dom iEdg (S)) \to iEdg (S) (x) \in \{e \in 𝒫 Vtx (S) \| \|e\| = 2\}$
18	17	ralrimiva	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UMGraph)) \to \forall x \in dom iEdg (S) iEdg (S) (x) \in \{e \in 𝒫 Vtx (S) \| \|e\| = 2\}$
19		fnfvrnss	$⊢ (iEdg (S) Fn dom iEdg (S) \land \forall x \in dom iEdg (S) iEdg (S) (x) \in \{e \in 𝒫 Vtx (S) \| \|e\| = 2\}) \to ran iEdg (S) \subseteq \{e \in 𝒫 Vtx (S) \| \|e\| = 2\}$
20	12 18 19	syl2anc	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UMGraph)) \to ran iEdg (S) \subseteq \{e \in 𝒫 Vtx (S) \| \|e\| = 2\}$
21		df-f	$⊢ iEdg (S) : dom iEdg (S) ⟶ \{e \in 𝒫 Vtx (S) \| \|e\| = 2\} \leftrightarrow (iEdg (S) Fn dom iEdg (S) \land ran iEdg (S) \subseteq \{e \in 𝒫 Vtx (S) \| \|e\| = 2\})$
22	12 20 21	sylanbrc	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UMGraph)) \to iEdg (S) : dom iEdg (S) ⟶ \{e \in 𝒫 Vtx (S) \| \|e\| = 2\}$
23		subgrv	$⊢ S SubGraph G \to (S \in V \land G \in V)$
24	1 3	isumgrs	$⊢ S \in V \to (S \in UMGraph \leftrightarrow iEdg (S) : dom iEdg (S) ⟶ \{e \in 𝒫 Vtx (S) \| \|e\| = 2\})$
25	24	adantr	$⊢ (S \in V \land G \in V) \to (S \in UMGraph \leftrightarrow iEdg (S) : dom iEdg (S) ⟶ \{e \in 𝒫 Vtx (S) \| \|e\| = 2\})$
26	23 25	syl	$⊢ S SubGraph G \to (S \in UMGraph \leftrightarrow iEdg (S) : dom iEdg (S) ⟶ \{e \in 𝒫 Vtx (S) \| \|e\| = 2\})$
27	26	ad2antrl	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UMGraph)) \to (S \in UMGraph \leftrightarrow iEdg (S) : dom iEdg (S) ⟶ \{e \in 𝒫 Vtx (S) \| \|e\| = 2\})$
28	22 27	mpbird	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UMGraph)) \to S \in UMGraph$
29	28	ex	$⊢ (Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \to ((S SubGraph G \land G \in UMGraph) \to S \in UMGraph)$
30	6 29	syl	$⊢ S SubGraph G \to ((S SubGraph G \land G \in UMGraph) \to S \in UMGraph)$
31	30	anabsi8	$⊢ (G \in UMGraph \land S SubGraph G) \to S \in UMGraph$

Metamath Proof Explorer

Theorem subumgr

Proof