Metamath Proof Explorer

Theorem isubgriedg

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

Ref Expression
Hypotheses isubgriedg.v ⊢ V = Vtx ⁡ G
isubgriedg.e ⊢ E = iEdg ⁡ G
Assertion isubgriedg ⊢ G ∈ W ∧ S ⊆ V → iEdg ⁡ G ISubGr S = E ↾ x ∈ dom ⁡ E | E ⁡ x ⊆ S

Proof

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