Metamath Proof Explorer

Theorem isubgrvtx

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

Ref Expression
Hypothesis isubgrvtx.v ⊢ V = Vtx ⁡ G
Assertion isubgrvtx ⊢ G ∈ W ∧ S ⊆ V → Vtx ⁡ G ISubGr S = S

Proof

Step Hyp Ref Expression
1 isubgrvtx.v ⊢ V = Vtx ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 1 2 isisubgr ⊢ G ∈ W ∧ S ⊆ V → G ISubGr S = S iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ S
4 3 fveq2d ⊢ G ∈ W ∧ S ⊆ V → Vtx ⁡ G ISubGr S = Vtx ⁡ S iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ S
5 1 fvexi ⊢ V ∈ V
6 5 ssex ⊢ S ⊆ V → S ∈ V
7 fvexd ⊢ G ∈ W ∧ S ⊆ V → iEdg ⁡ G ∈ V
8 7 resexd ⊢ G ∈ W ∧ S ⊆ V → iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ S ∈ V
9 opvtxfv ⊢ S ∈ V ∧ iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ S ∈ V → Vtx ⁡ S iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ S = S
10 6 8 9 syl2an2 ⊢ G ∈ W ∧ S ⊆ V → Vtx ⁡ S iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ S = S
11 4 10 eqtrd ⊢ G ∈ W ∧ S ⊆ V → Vtx ⁡ G ISubGr S = S