Theorem upgrspanop

Description: A spanning subgraph of a pseudograph represented by an ordered pair is a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 13-Oct-2020)

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

Proof

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