Metamath Proof Explorer

Theorem upgrspan

Description: A spanning subgraph S of a pseudograph G is a pseudograph. (Contributed by AV, 11-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 ‘ 𝑆 ) = ( 𝐸 ↾ 𝐴 ) )
upgrspan.g ⊢ ( 𝜑 → 𝐺 ∈ UPGraph )
Assertion upgrspan ( 𝜑 → 𝑆 ∈ UPGraph )

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 upgrspan.g ⊢ ( 𝜑 → 𝐺 ∈ UPGraph )
7 upgruhgr ⊢ ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph )
8 6 7 syl ⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
9 1 2 3 4 5 8 uhgrspansubgr ⊢ ( 𝜑 → 𝑆 SubGraph 𝐺 )
10 subupgr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑆 SubGraph 𝐺 ) → 𝑆 ∈ UPGraph )
11 6 9 10 syl2anc ⊢ ( 𝜑 → 𝑆 ∈ UPGraph )