Metamath Proof Explorer

Theorem isubgriedg

Description: The edges of an induced subgraph. (Contributed by AV, 12-May-2025)

Ref Expression
Hypotheses isubgriedg.v 
|- V = ( Vtx ` G )
isubgriedg.e 
|- E = ( iEdg ` G )
Assertion isubgriedg 
|- ( ( G e. W /\ S C_ V ) -> ( iEdg ` ( G ISubGr S ) ) = ( E |` { x e. dom E | ( E ` x ) C_ S } ) )

Proof

Step Hyp Ref Expression
1 isubgriedg.v 
 |-  V = ( Vtx ` G )
2 isubgriedg.e 
 |-  E = ( iEdg ` G )
3 1 2 isisubgr 
 |-  ( ( G e. W /\ S C_ V ) -> ( G ISubGr S ) = <. S , ( E |` { x e. dom E | ( E ` x ) C_ S } ) >. )
4 3 fveq2d 
 |-  ( ( G e. W /\ S C_ V ) -> ( iEdg ` ( G ISubGr S ) ) = ( iEdg ` <. S , ( E |` { x e. dom E | ( E ` x ) C_ S } ) >. ) )
5 1 fvexi 
 |-  V e. _V
6 5 ssex 
 |-  ( S C_ V -> S e. _V )
7 2 fvexi 
 |-  E e. _V
8 7 a1i 
 |-  ( ( G e. W /\ S C_ V ) -> E e. _V )
9 8 resexd 
 |-  ( ( G e. W /\ S C_ V ) -> ( E |` { x e. dom E | ( E ` x ) C_ S } ) e. _V )
10 opiedgfv 
 |-  ( ( S e. _V /\ ( E |` { x e. dom E | ( E ` x ) C_ S } ) e. _V ) -> ( iEdg ` <. S , ( E |` { x e. dom E | ( E ` x ) C_ S } ) >. ) = ( E |` { x e. dom E | ( E ` x ) C_ S } ) )
11 6 9 10 syl2an2 
 |-  ( ( G e. W /\ S C_ V ) -> ( iEdg ` <. S , ( E |` { x e. dom E | ( E ` x ) C_ S } ) >. ) = ( E |` { x e. dom E | ( E ` x ) C_ S } ) )
12 4 11 eqtrd 
 |-  ( ( G e. W /\ S C_ V ) -> ( iEdg ` ( G ISubGr S ) ) = ( E |` { x e. dom E | ( E ` x ) C_ S } ) )