Metamath Proof Explorer

Theorem subgreldmiedg

Description: An element of the domain of the edge function of a subgraph is an element of the domain of the edge function of the supergraph. (Contributed by AV, 20-Nov-2020)

		Ref	Expression
	Assertion	subgreldmiedg	$⊢ (S SubGraph G \land X \in dom iEdg (S)) \to X \in dom iEdg (G)$

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		dmss	$⊢ iEdg (S) \subseteq iEdg (G) \to dom iEdg (S) \subseteq dom iEdg (G)$
8	7	3ad2ant2	$⊢ (Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \to dom iEdg (S) \subseteq dom iEdg (G)$
9	8	sseld	$⊢ (Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \to (X \in dom iEdg (S) \to X \in dom iEdg (G))$
10	6 9	syl	$⊢ S SubGraph G \to (X \in dom iEdg (S) \to X \in dom iEdg (G))$
11	10	imp	$⊢ (S SubGraph G \land X \in dom iEdg (S)) \to X \in dom iEdg (G)$