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→VE↾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→∀gVtx⁡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→VE↾A∈UPGraph