Metamath Proof Explorer


Theorem upgr0eopALT

Description: Alternate proof of upgr0eop , using the general theorem gropeld to transform a theorem for an arbitrary representation of a graph into a theorem for a graph represented as ordered pair. This general approach causes some overhead, which makes the proof longer than necessary (see proof of upgr0eop ). (Contributed by AV, 11-Oct-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion upgr0eopALT V W V UPGraph

Proof

Step Hyp Ref Expression
1 vex g V
2 1 a1i Vtx g = V iEdg g = g V
3 simpr Vtx g = V iEdg g = iEdg g =
4 2 3 upgr0e Vtx g = V iEdg g = g UPGraph
5 4 ax-gen g Vtx g = V iEdg g = g UPGraph
6 5 a1i V W g Vtx g = V iEdg g = g UPGraph
7 id V W V W
8 0ex V
9 8 a1i V W V
10 6 7 9 gropeld V W V UPGraph