This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Undirected graphs Subgraphs usgrspan
Description: A spanning subgraph S of a simple graph G is a simple graph.
(Contributed by AV , 15-Oct-2020) (Revised by AV , 16-Oct-2020) (Proof
shortened by AV , 18-Nov-2020)
Ref
Expression
Hypotheses
uhgrspan.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
uhgrspan.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
uhgrspan.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
uhgrspan.q ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
uhgrspan.r ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐸 ↾ 𝐴 ) )
usgrspan.g ⊢ ( 𝜑 → 𝐺 ∈ USGraph )
Assertion
usgrspan ⊢ ( 𝜑 → 𝑆 ∈ USGraph )
Proof
Step
Hyp
Ref
Expression
1
uhgrspan.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2
uhgrspan.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3
uhgrspan.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
4
uhgrspan.q ⊢ ( 𝜑 → ( Vtx ‘ 𝑆 ) = 𝑉 )
5
uhgrspan.r ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐸 ↾ 𝐴 ) )
6
usgrspan.g ⊢ ( 𝜑 → 𝐺 ∈ USGraph )
7
usgruhgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
8
6 7
syl ⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
9
1 2 3 4 5 8
uhgrspansubgr ⊢ ( 𝜑 → 𝑆 SubGraph 𝐺 )
10
subusgr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑆 SubGraph 𝐺 ) → 𝑆 ∈ USGraph )
11
6 9 10
syl2anc ⊢ ( 𝜑 → 𝑆 ∈ USGraph )