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 )