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 ⊢ V = Vtx ⁡ G
uhgrspanop.e ⊢ E = iEdg ⁡ G
Assertion uhgrspanop ⊢ G ∈ UHGraph → V E ↾ A ∈ UHGraph

Proof

Step Hyp Ref Expression
1 uhgrspanop.v ⊢ V = Vtx ⁡ G
2 uhgrspanop.e ⊢ E = iEdg ⁡ G
3 opex ⊢ V E ↾ A ∈ V
4 3 a1i ⊢ G ∈ UHGraph → V E ↾ A ∈ V
5 1 fvexi ⊢ V ∈ V
6 2 fvexi ⊢ E ∈ V
7 6 resex ⊢ E ↾ A ∈ V
8 5 7 opvtxfvi ⊢ Vtx ⁡ V E ↾ A = V
9 8 a1i ⊢ G ∈ UHGraph → Vtx ⁡ V E ↾ A = V
10 5 7 opiedgfvi ⊢ iEdg ⁡ V E ↾ A = E ↾ A
11 10 a1i ⊢ G ∈ UHGraph → iEdg ⁡ V E ↾ A = E ↾ A
12 id ⊢ G ∈ UHGraph → G ∈ UHGraph
13 1 2 4 9 11 12 uhgrspan ⊢ G ∈ UHGraph → V E ↾ A ∈ UHGraph