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 𝑆 ) ) = 𝑆 )