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

Metamath Proof Explorer

Theorem isubgriedg

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

Ref Expression
Hypotheses isubgriedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isubgriedg.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion isubgriedg ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) )

Proof

Step Hyp Ref Expression
1 isubgriedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isubgriedg.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 1 2 isisubgr ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) = ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ )
4 3 fveq2d ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) = ( iEdg ‘ ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ ) )
5 1 fvexi ⊢ 𝑉 ∈ V
6 5 ssex ⊢ ( 𝑆 ⊆ 𝑉 → 𝑆 ∈ V )
7 2 fvexi ⊢ 𝐸 ∈ V
8 7 a1i ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → 𝐸 ∈ V )
9 8 resexd ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ∈ V )
10 opiedgfv ⊢ ( ( 𝑆 ∈ V ∧ ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ∈ V ) → ( iEdg ‘ ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) )
11 6 9 10 syl2an2 ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) )
12 4 11 eqtrd ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) )