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	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → 𝐼 ⊆ 𝐸 )