Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 uhgrspanop.v ⊢ V = Vtx ⁡ G
2 uhgrspanop.e ⊢ E = iEdg ⁡ G
3 vex ⊢ g ∈ V
4 3 a1i ⊢ G ∈ UPGraph ∧ Vtx ⁡ g = V ∧ iEdg ⁡ g = E ↾ A → g ∈ V
5 simprl ⊢ G ∈ UPGraph ∧ Vtx ⁡ g = V ∧ iEdg ⁡ g = E ↾ A → Vtx ⁡ g = V
6 simprr ⊢ G ∈ UPGraph ∧ Vtx ⁡ g = V ∧ iEdg ⁡ g = E ↾ A → iEdg ⁡ g = E ↾ A
7 simpl ⊢ G ∈ UPGraph ∧ Vtx ⁡ g = V ∧ iEdg ⁡ g = E ↾ A → G ∈ UPGraph
8 1 2 4 5 6 7 upgrspan ⊢ G ∈ UPGraph ∧ Vtx ⁡ g = V ∧ iEdg ⁡ g = E ↾ A → g ∈ UPGraph
9 8 ex ⊢ G ∈ UPGraph → Vtx ⁡ g = V ∧ iEdg ⁡ g = E ↾ A → g ∈ UPGraph
10 9 alrimiv ⊢ G ∈ UPGraph → ∀ g Vtx ⁡ g = V ∧ iEdg ⁡ g = E ↾ A → g ∈ UPGraph
11 1 fvexi ⊢ V ∈ V
12 11 a1i ⊢ G ∈ UPGraph → V ∈ V
13 2 fvexi ⊢ E ∈ V
14 13 resex ⊢ E ↾ A ∈ V
15 14 a1i ⊢ G ∈ UPGraph → E ↾ A ∈ V
16 10 12 15 gropeld ⊢ G ∈ UPGraph → V E ↾ A ∈ UPGraph