Metamath Proof Explorer

Theorem subgrprop

Description: The properties of a subgraph. (Contributed by AV, 19-Nov-2020)

Ref Expression
Hypotheses issubgr.v ⊢ V = Vtx ⁡ S
issubgr.a ⊢ A = Vtx ⁡ G
issubgr.i ⊢ I = iEdg ⁡ S
issubgr.b ⊢ B = iEdg ⁡ G
issubgr.e ⊢ E = Edg ⁡ S
Assertion subgrprop ⊢ S SubGraph G → V ⊆ A ∧ I = B ↾ dom ⁡ I ∧ E ⊆ 𝒫 V

Proof

Step Hyp Ref Expression
1 issubgr.v ⊢ V = Vtx ⁡ S
2 issubgr.a ⊢ A = Vtx ⁡ G
3 issubgr.i ⊢ I = iEdg ⁡ S
4 issubgr.b ⊢ B = iEdg ⁡ G
5 issubgr.e ⊢ E = Edg ⁡ S
6 subgrv ⊢ S SubGraph G → S ∈ V ∧ G ∈ V
7 1 2 3 4 5 issubgr ⊢ G ∈ V ∧ S ∈ V → S SubGraph G ↔ V ⊆ A ∧ I = B ↾ dom ⁡ I ∧ E ⊆ 𝒫 V
8 7 biimpd ⊢ G ∈ V ∧ S ∈ V → S SubGraph G → V ⊆ A ∧ I = B ↾ dom ⁡ I ∧ E ⊆ 𝒫 V
9 8 ancoms ⊢ S ∈ V ∧ G ∈ V → S SubGraph G → V ⊆ A ∧ I = B ↾ dom ⁡ I ∧ E ⊆ 𝒫 V
10 6 9 mpcom ⊢ S SubGraph G → V ⊆ A ∧ I = B ↾ dom ⁡ I ∧ E ⊆ 𝒫 V