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 
|- 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 )