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 e. W /\ S C_ V ) -> I C_ 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 e. W /\ S C_ V ) -> ( iEdg ` ( G ISubGr S ) ) = ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) )
8	5 7	eqtrid	|- ( ( G e. W /\ S C_ V ) -> ( iEdg ` H ) = ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) )
9	8	rneqd	|- ( ( G e. W /\ S C_ V ) -> ran ( iEdg ` H ) = ran ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) )
10		resss	|- ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) C_ ( iEdg ` G )
11		rnss	|- ( ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) C_ ( iEdg ` G ) -> ran ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) C_ ran ( iEdg ` G ) )
12	10 11	mp1i	|- ( ( G e. W /\ S C_ V ) -> ran ( ( iEdg ` G ) |` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) C_ S } ) C_ ran ( iEdg ` G ) )
13	9 12	eqsstrd	|- ( ( G e. W /\ S C_ V ) -> ran ( iEdg ` H ) C_ 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 e. W /\ S C_ V ) -> I C_ E )