This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isisubgr.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion isisubgr ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) = ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ )

Proof

Step Hyp Ref Expression
1 isisubgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isisubgr.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 elex ⊢ ( 𝐺 ∈ 𝑊 → 𝐺 ∈ V )
4 3 adantr ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → 𝐺 ∈ V )
5 1 fvexi ⊢ 𝑉 ∈ V
6 5 a1i ⊢ ( 𝑆 ⊆ 𝑉 → 𝑉 ∈ V )
7 id ⊢ ( 𝑆 ⊆ 𝑉 → 𝑆 ⊆ 𝑉 )
8 6 7 sselpwd ⊢ ( 𝑆 ⊆ 𝑉 → 𝑆 ∈ 𝒫 𝑉 )
9 8 adantl ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ∈ 𝒫 𝑉 )
10 opex ⊢ ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ ∈ V
11 10 a1i ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ ∈ V )
12 simpr ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) → 𝑣 = 𝑆 )
13 fvexd ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) → ( iEdg ‘ 𝑔 ) ∈ V )
14 fveq2 ⊢ ( 𝑔 = 𝐺 → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) )
15 14 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( iEdg ‘ 𝑔 ) = 𝐸 )
16 15 eqeq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑒 = ( iEdg ‘ 𝑔 ) ↔ 𝑒 = 𝐸 ) )
17 16 adantr ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) → ( 𝑒 = ( iEdg ‘ 𝑔 ) ↔ 𝑒 = 𝐸 ) )
18 simpr ⊢ ( ( 𝑣 = 𝑆 ∧ 𝑒 = 𝐸 ) → 𝑒 = 𝐸 )
19 dmeq ⊢ ( 𝑒 = 𝐸 → dom 𝑒 = dom 𝐸 )
20 19 adantl ⊢ ( ( 𝑣 = 𝑆 ∧ 𝑒 = 𝐸 ) → dom 𝑒 = dom 𝐸 )
21 fveq1 ⊢ ( 𝑒 = 𝐸 → ( 𝑒 ‘ 𝑥 ) = ( 𝐸 ‘ 𝑥 ) )
22 21 adantl ⊢ ( ( 𝑣 = 𝑆 ∧ 𝑒 = 𝐸 ) → ( 𝑒 ‘ 𝑥 ) = ( 𝐸 ‘ 𝑥 ) )
23 simpl ⊢ ( ( 𝑣 = 𝑆 ∧ 𝑒 = 𝐸 ) → 𝑣 = 𝑆 )
24 22 23 sseq12d ⊢ ( ( 𝑣 = 𝑆 ∧ 𝑒 = 𝐸 ) → ( ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 ↔ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 ) )
25 20 24 rabeqbidv ⊢ ( ( 𝑣 = 𝑆 ∧ 𝑒 = 𝐸 ) → { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } = { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } )
26 18 25 reseq12d ⊢ ( ( 𝑣 = 𝑆 ∧ 𝑒 = 𝐸 ) → ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) )
27 26 ex ⊢ ( 𝑣 = 𝑆 → ( 𝑒 = 𝐸 → ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ) )
28 27 adantl ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) → ( 𝑒 = 𝐸 → ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ) )
29 17 28 sylbid ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) → ( 𝑒 = ( iEdg ‘ 𝑔 ) → ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ) )
30 29 imp ⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) ∧ 𝑒 = ( iEdg ‘ 𝑔 ) ) → ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) )
31 13 30 csbied ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) → ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) )
32 12 31 opeq12d ⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) → ⟨ 𝑣 , ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) ⟩ = ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ )
33 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
34 33 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 )
35 34 pweqd ⊢ ( 𝑔 = 𝐺 → 𝒫 ( Vtx ‘ 𝑔 ) = 𝒫 𝑉 )
36 df-isubgr ⊢ ISubGr = ( 𝑔 ∈ V , 𝑣 ∈ 𝒫 ( Vtx ‘ 𝑔 ) ↦ ⟨ 𝑣 , ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) ⟩ )
37 32 35 36 ovmpox ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ 𝒫 𝑉 ∧ ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ ∈ V ) → ( 𝐺 ISubGr 𝑆 ) = ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ )
38 4 9 11 37 syl3anc ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) = ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ )