Theorem usgrspanop

Description: A spanning subgraph of a simple graph represented by an ordered pair is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020)

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

Proof

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