This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Undirected graphs Subgraphs subgrprop2
Description: The properties of a subgraph: If S is a subgraph of G , its
vertices are also vertices of G , and its edges are also edges of
G , connecting vertices of the subgraph only. (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
subgrprop2 ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ 𝐸 ⊆ 𝒫 𝑉 ) )
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
1 2 3 4 5
subgrprop ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) )
7
resss ⊢ ( 𝐵 ↾ dom 𝐼 ) ⊆ 𝐵
8
sseq1 ⊢ ( 𝐼 = ( 𝐵 ↾ dom 𝐼 ) → ( 𝐼 ⊆ 𝐵 ↔ ( 𝐵 ↾ dom 𝐼 ) ⊆ 𝐵 ) )
9
7 8
mpbiri ⊢ ( 𝐼 = ( 𝐵 ↾ dom 𝐼 ) → 𝐼 ⊆ 𝐵 )
10
9
3anim2i ⊢ ( ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ 𝐸 ⊆ 𝒫 𝑉 ) )
11
6 10
syl ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ 𝐸 ⊆ 𝒫 𝑉 ) )