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

Metamath Proof Explorer

Theorem subgrprop

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

Ref Expression
Hypotheses issubgr.v ⊢ 𝑉 = ( Vtx ‘ 𝑆 )
issubgr.a ⊢ 𝐴 = ( Vtx ‘ 𝐺 )
issubgr.i ⊢ 𝐼 = ( iEdg ‘ 𝑆 )
issubgr.b ⊢ 𝐵 = ( iEdg ‘ 𝐺 )
issubgr.e ⊢ 𝐸 = ( Edg ‘ 𝑆 )
Assertion subgrprop ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) )

Proof

Step Hyp Ref Expression
1 issubgr.v ⊢ 𝑉 = ( Vtx ‘ 𝑆 )
2 issubgr.a ⊢ 𝐴 = ( Vtx ‘ 𝐺 )
3 issubgr.i ⊢ 𝐼 = ( iEdg ‘ 𝑆 )
4 issubgr.b ⊢ 𝐵 = ( iEdg ‘ 𝐺 )
5 issubgr.e ⊢ 𝐸 = ( Edg ‘ 𝑆 )
6 subgrv ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) )
7 1 2 3 4 5 issubgr ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑆 SubGraph 𝐺 ↔ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) ) )
8 7 biimpd ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) ) )
9 8 ancoms ⊢ ( ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) → ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) ) )
10 6 9 mpcom ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) )