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

Metamath Proof Explorer

Theorem umgrspanop

Description: A spanning subgraph of a multigraph represented by an ordered pair is a multigraph. (Contributed by AV, 27-Nov-2020)

Ref Expression
Hypotheses uhgrspanop.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
uhgrspanop.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion umgrspanop ( 𝐺 ∈ UMGraph → ⟨ 𝑉 , ( 𝐸 ↾ 𝐴 ) ⟩ ∈ UMGraph )

Proof

Step Hyp Ref Expression
1 uhgrspanop.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 uhgrspanop.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 vex ⊢ 𝑔 ∈ V
4 3 a1i ⊢ ( ( 𝐺 ∈ UMGraph ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = ( 𝐸 ↾ 𝐴 ) ) ) → 𝑔 ∈ V )
5 simprl ⊢ ( ( 𝐺 ∈ UMGraph ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = ( 𝐸 ↾ 𝐴 ) ) ) → ( Vtx ‘ 𝑔 ) = 𝑉 )
6 simprr ⊢ ( ( 𝐺 ∈ UMGraph ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = ( 𝐸 ↾ 𝐴 ) ) ) → ( iEdg ‘ 𝑔 ) = ( 𝐸 ↾ 𝐴 ) )
7 simpl ⊢ ( ( 𝐺 ∈ UMGraph ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = ( 𝐸 ↾ 𝐴 ) ) ) → 𝐺 ∈ UMGraph )
8 1 2 4 5 6 7 umgrspan ⊢ ( ( 𝐺 ∈ UMGraph ∧ ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = ( 𝐸 ↾ 𝐴 ) ) ) → 𝑔 ∈ UMGraph )
9 8 ex ⊢ ( 𝐺 ∈ UMGraph → ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = ( 𝐸 ↾ 𝐴 ) ) → 𝑔 ∈ UMGraph ) )
10 9 alrimiv ⊢ ( 𝐺 ∈ UMGraph → ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = ( 𝐸 ↾ 𝐴 ) ) → 𝑔 ∈ UMGraph ) )
11 1 fvexi ⊢ 𝑉 ∈ V
12 11 a1i ⊢ ( 𝐺 ∈ UMGraph → 𝑉 ∈ V )
13 2 fvexi ⊢ 𝐸 ∈ V
14 13 resex ⊢ ( 𝐸 ↾ 𝐴 ) ∈ V
15 14 a1i ⊢ ( 𝐺 ∈ UMGraph → ( 𝐸 ↾ 𝐴 ) ∈ V )
16 10 12 15 gropeld ⊢ ( 𝐺 ∈ UMGraph → ⟨ 𝑉 , ( 𝐸 ↾ 𝐴 ) ⟩ ∈ UMGraph )