Metamath Proof Explorer

Theorem isubgredgss

Description: The edges of an induced subgraph of a graph are edges of the graph. (Contributed by AV, 24-Sep-2025)

Ref Expression
Hypotheses isubgredg.v ⊢ V = Vtx ⁡ G
isubgredg.e ⊢ E = Edg ⁡ G
isubgredg.h ⊢ H = G ISubGr S
isubgredg.i ⊢ I = Edg ⁡ H
Assertion isubgredgss ⊢ G ∈ W ∧ S ⊆ V → I ⊆ E

Proof

Step Hyp Ref Expression
1 isubgredg.v ⊢ V = Vtx ⁡ G
2 isubgredg.e ⊢ E = Edg ⁡ G
3 isubgredg.h ⊢ H = G ISubGr S
4 isubgredg.i ⊢ I = Edg ⁡ H
5 3 fveq2i ⊢ iEdg ⁡ H = iEdg ⁡ G ISubGr S
6 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
7 1 6 isubgriedg ⊢ G ∈ W ∧ S ⊆ V → iEdg ⁡ G ISubGr S = iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ S
8 5 7 eqtrid ⊢ G ∈ W ∧ S ⊆ V → iEdg ⁡ H = iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ S
9 8 rneqd ⊢ G ∈ W ∧ S ⊆ V → ran ⁡ iEdg ⁡ H = ran ⁡ iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ S
10 resss ⊢ iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ S ⊆ iEdg ⁡ G
11 rnss ⊢ iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ S ⊆ iEdg ⁡ G → ran ⁡ iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ S ⊆ ran ⁡ iEdg ⁡ G
12 10 11 mp1i ⊢ G ∈ W ∧ S ⊆ V → ran ⁡ iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ S ⊆ ran ⁡ iEdg ⁡ G
13 9 12 eqsstrd ⊢ G ∈ W ∧ S ⊆ V → ran ⁡ iEdg ⁡ H ⊆ ran ⁡ iEdg ⁡ G
14 edgval ⊢ Edg ⁡ H = ran ⁡ iEdg ⁡ H
15 4 14 eqtri ⊢ I = ran ⁡ iEdg ⁡ H
16 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
17 2 16 eqtri ⊢ E = ran ⁡ iEdg ⁡ G
18 13 15 17 3sstr4g ⊢ G ∈ W ∧ S ⊆ V → I ⊆ E