This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isubgredg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
isubgredg.h ⊢ 𝐻 = ( 𝐺 ISubGr 𝑆 )
isubgredg.i ⊢ 𝐼 = ( Edg ‘ 𝐻 )
Assertion isubgredgss ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → 𝐼 ⊆ 𝐸 )

Proof

Step Hyp Ref Expression
1 isubgredg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isubgredg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 isubgredg.h ⊢ 𝐻 = ( 𝐺 ISubGr 𝑆 )
4 isubgredg.i ⊢ 𝐼 = ( Edg ‘ 𝐻 )
5 3 fveq2i ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) )
6 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
7 1 6 isubgriedg ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) = ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) )
8 5 7 eqtrid ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ 𝐻 ) = ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) )
9 8 rneqd ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ran ( iEdg ‘ 𝐻 ) = ran ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) )
10 resss ⊢ ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ⊆ ( iEdg ‘ 𝐺 )
11 rnss ⊢ ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ⊆ ( iEdg ‘ 𝐺 ) → ran ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ⊆ ran ( iEdg ‘ 𝐺 ) )
12 10 11 mp1i ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ran ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ⊆ ran ( iEdg ‘ 𝐺 ) )
13 9 12 eqsstrd ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ran ( iEdg ‘ 𝐻 ) ⊆ ran ( iEdg ‘ 𝐺 ) )
14 edgval ⊢ ( Edg ‘ 𝐻 ) = ran ( iEdg ‘ 𝐻 )
15 4 14 eqtri ⊢ 𝐼 = ran ( iEdg ‘ 𝐻 )
16 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
17 2 16 eqtri ⊢ 𝐸 = ran ( iEdg ‘ 𝐺 )
18 13 15 17 3sstr4g ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → 𝐼 ⊆ 𝐸 )