Metamath Proof Explorer

Theorem isubgrvtx

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

Ref Expression
Hypothesis isubgrvtx.v 
|- V = ( Vtx ` G )
Assertion isubgrvtx 
|- ( ( G e. W /\ S C_ V ) -> ( Vtx ` ( G ISubGr S ) ) = S )

Proof

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