Metamath Proof Explorer

Theorem isisubgr

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

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

Proof

Step Hyp Ref Expression
1 isisubgr.v 
 |-  V = ( Vtx ` G )
2 isisubgr.e 
 |-  E = ( iEdg ` G )
3 elex 
 |-  ( G e. W -> G e. _V )
4 3 adantr 
 |-  ( ( G e. W /\ S C_ V ) -> G e. _V )
5 1 fvexi 
 |-  V e. _V
6 5 a1i 
 |-  ( S C_ V -> V e. _V )
7 id 
 |-  ( S C_ V -> S C_ V )
8 6 7 sselpwd 
 |-  ( S C_ V -> S e. ~P V )
9 8 adantl 
 |-  ( ( G e. W /\ S C_ V ) -> S e. ~P V )
10 opex 
 |-  <. S , ( E |` { x e. dom E | ( E ` x ) C_ S } ) >. e. _V
11 10 a1i 
 |-  ( ( G e. W /\ S C_ V ) -> <. S , ( E |` { x e. dom E | ( E ` x ) C_ S } ) >. e. _V )
12 simpr 
 |-  ( ( g = G /\ v = S ) -> v = S )
13 fvexd 
 |-  ( ( g = G /\ v = S ) -> ( iEdg ` g ) e. _V )
14 fveq2 
 |-  ( g = G -> ( iEdg ` g ) = ( iEdg ` G ) )
15 14 2 eqtr4di 
 |-  ( g = G -> ( iEdg ` g ) = E )
16 15 eqeq2d 
 |-  ( g = G -> ( e = ( iEdg ` g ) <-> e = E ) )
17 16 adantr 
 |-  ( ( g = G /\ v = S ) -> ( e = ( iEdg ` g ) <-> e = E ) )
18 simpr 
 |-  ( ( v = S /\ e = E ) -> e = E )
19 dmeq 
 |-  ( e = E -> dom e = dom E )
20 19 adantl 
 |-  ( ( v = S /\ e = E ) -> dom e = dom E )
21 fveq1 
 |-  ( e = E -> ( e ` x ) = ( E ` x ) )
22 21 adantl 
 |-  ( ( v = S /\ e = E ) -> ( e ` x ) = ( E ` x ) )
23 simpl 
 |-  ( ( v = S /\ e = E ) -> v = S )
24 22 23 sseq12d 
 |-  ( ( v = S /\ e = E ) -> ( ( e ` x ) C_ v <-> ( E ` x ) C_ S ) )
25 20 24 rabeqbidv 
 |-  ( ( v = S /\ e = E ) -> { x e. dom e | ( e ` x ) C_ v } = { x e. dom E | ( E ` x ) C_ S } )
26 18 25 reseq12d 
 |-  ( ( v = S /\ e = E ) -> ( e |` { x e. dom e | ( e ` x ) C_ v } ) = ( E |` { x e. dom E | ( E ` x ) C_ S } ) )
27 26 ex 
 |-  ( v = S -> ( e = E -> ( e |` { x e. dom e | ( e ` x ) C_ v } ) = ( E |` { x e. dom E | ( E ` x ) C_ S } ) ) )
28 27 adantl 
 |-  ( ( g = G /\ v = S ) -> ( e = E -> ( e |` { x e. dom e | ( e ` x ) C_ v } ) = ( E |` { x e. dom E | ( E ` x ) C_ S } ) ) )
29 17 28 sylbid 
 |-  ( ( g = G /\ v = S ) -> ( e = ( iEdg ` g ) -> ( e |` { x e. dom e | ( e ` x ) C_ v } ) = ( E |` { x e. dom E | ( E ` x ) C_ S } ) ) )
30 29 imp 
 |-  ( ( ( g = G /\ v = S ) /\ e = ( iEdg ` g ) ) -> ( e |` { x e. dom e | ( e ` x ) C_ v } ) = ( E |` { x e. dom E | ( E ` x ) C_ S } ) )
31 13 30 csbied 
 |-  ( ( g = G /\ v = S ) -> [_ ( iEdg ` g ) / e ]_ ( e |` { x e. dom e | ( e ` x ) C_ v } ) = ( E |` { x e. dom E | ( E ` x ) C_ S } ) )
32 12 31 opeq12d 
 |-  ( ( g = G /\ v = S ) -> <. v , [_ ( iEdg ` g ) / e ]_ ( e |` { x e. dom e | ( e ` x ) C_ v } ) >. = <. S , ( E |` { x e. dom E | ( E ` x ) C_ S } ) >. )
33 fveq2 
 |-  ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) )
34 33 1 eqtr4di 
 |-  ( g = G -> ( Vtx ` g ) = V )
35 34 pweqd 
 |-  ( g = G -> ~P ( Vtx ` g ) = ~P V )
36 df-isubgr 
 |-  ISubGr = ( g e. _V , v e. ~P ( Vtx ` g ) |-> <. v , [_ ( iEdg ` g ) / e ]_ ( e |` { x e. dom e | ( e ` x ) C_ v } ) >. )
37 32 35 36 ovmpox 
 |-  ( ( G e. _V /\ S e. ~P V /\ <. S , ( E |` { x e. dom E | ( E ` x ) C_ S } ) >. e. _V ) -> ( G ISubGr S ) = <. S , ( E |` { x e. dom E | ( E ` x ) C_ S } ) >. )
38 4 9 11 37 syl3anc 
 |-  ( ( G e. W /\ S C_ V ) -> ( G ISubGr S ) = <. S , ( E |` { x e. dom E | ( E ` x ) C_ S } ) >. )