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 ∧ X ∈ dom ⁡ iEdg ⁡ S → X ∈ 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 → Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S
7 dmss ⊢ iEdg ⁡ S ⊆ iEdg ⁡ G → dom ⁡ iEdg ⁡ S ⊆ dom ⁡ iEdg ⁡ G
8 7 3ad2ant2 ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S → dom ⁡ iEdg ⁡ S ⊆ dom ⁡ iEdg ⁡ G
9 8 sseld ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S → X ∈ dom ⁡ iEdg ⁡ S → X ∈ dom ⁡ iEdg ⁡ G
10 6 9 syl ⊢ S SubGraph G → X ∈ dom ⁡ iEdg ⁡ S → X ∈ dom ⁡ iEdg ⁡ G
11 10 imp ⊢ S SubGraph G ∧ X ∈ dom ⁡ iEdg ⁡ S → X ∈ dom ⁡ iEdg ⁡ G