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

Metamath Proof Explorer

Theorem isubgrvtx

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

Ref Expression
Hypothesis isubgrvtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion isubgrvtx ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) ) = 𝑆 )

Proof

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