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

Metamath Proof Explorer

Theorem uhgrspanop

Description: A spanning subgraph of a hypergraph represented by an ordered pair is a hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017) (Revised by AV, 11-Oct-2020)

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

Proof

Step	Hyp	Ref	Expression
1		uhgrspanop.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		uhgrspanop.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3		opex	⊢ ⟨ 𝑉 , ( 𝐸 ↾ 𝐴 ) ⟩ ∈ V
4	3	a1i	⊢ ( 𝐺 ∈ UHGraph → ⟨ 𝑉 , ( 𝐸 ↾ 𝐴 ) ⟩ ∈ V )
5	1	fvexi	⊢ 𝑉 ∈ V
6	2	fvexi	⊢ 𝐸 ∈ V
7	6	resex	⊢ ( 𝐸 ↾ 𝐴 ) ∈ V
8	5 7	opvtxfvi	⊢ ( Vtx ‘ ⟨ 𝑉 , ( 𝐸 ↾ 𝐴 ) ⟩ ) = 𝑉
9	8	a1i	⊢ ( 𝐺 ∈ UHGraph → ( Vtx ‘ ⟨ 𝑉 , ( 𝐸 ↾ 𝐴 ) ⟩ ) = 𝑉 )
10	5 7	opiedgfvi	⊢ ( iEdg ‘ ⟨ 𝑉 , ( 𝐸 ↾ 𝐴 ) ⟩ ) = ( 𝐸 ↾ 𝐴 )
11	10	a1i	⊢ ( 𝐺 ∈ UHGraph → ( iEdg ‘ ⟨ 𝑉 , ( 𝐸 ↾ 𝐴 ) ⟩ ) = ( 𝐸 ↾ 𝐴 ) )
12		id	⊢ ( 𝐺 ∈ UHGraph → 𝐺 ∈ UHGraph )
13	1 2 4 9 11 12	uhgrspan	⊢ ( 𝐺 ∈ UHGraph → ⟨ 𝑉 , ( 𝐸 ↾ 𝐴 ) ⟩ ∈ UHGraph )