Metamath Proof Explorer

Theorem upgr1eopALT

Description: Alternate proof of upgr1eop , 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 upgr1eop ). (Contributed by AV, 11-Oct-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion upgr1eopALT ⊢V∈W∧A∈X∧B∈V∧C∈V→VABC∈UPGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡g=Vtx⁡g
2 simpllr ⊢V∈W∧A∈X∧B∈V∧C∈V∧Vtx⁡g=V∧iEdg⁡g=ABC→A∈X
3 simplrl ⊢V∈W∧A∈X∧B∈V∧C∈V∧Vtx⁡g=V∧iEdg⁡g=ABC→B∈V
4 eleq2 ⊢Vtx⁡g=V→B∈Vtx⁡g↔B∈V
5 4 ad2antrl ⊢V∈W∧A∈X∧B∈V∧C∈V∧Vtx⁡g=V∧iEdg⁡g=ABC→B∈Vtx⁡g↔B∈V
6 3 5 mpbird ⊢V∈W∧A∈X∧B∈V∧C∈V∧Vtx⁡g=V∧iEdg⁡g=ABC→B∈Vtx⁡g
7 simplrr ⊢V∈W∧A∈X∧B∈V∧C∈V∧Vtx⁡g=V∧iEdg⁡g=ABC→C∈V
8 eleq2 ⊢Vtx⁡g=V→C∈Vtx⁡g↔C∈V
9 8 ad2antrl ⊢V∈W∧A∈X∧B∈V∧C∈V∧Vtx⁡g=V∧iEdg⁡g=ABC→C∈Vtx⁡g↔C∈V
10 7 9 mpbird ⊢V∈W∧A∈X∧B∈V∧C∈V∧Vtx⁡g=V∧iEdg⁡g=ABC→C∈Vtx⁡g
11 simprr ⊢V∈W∧A∈X∧B∈V∧C∈V∧Vtx⁡g=V∧iEdg⁡g=ABC→iEdg⁡g=ABC
12 1 2 6 10 11 upgr1e ⊢V∈W∧A∈X∧B∈V∧C∈V∧Vtx⁡g=V∧iEdg⁡g=ABC→g∈UPGraph
13 12 ex ⊢V∈W∧A∈X∧B∈V∧C∈V→Vtx⁡g=V∧iEdg⁡g=ABC→g∈UPGraph
14 13 alrimiv ⊢V∈W∧A∈X∧B∈V∧C∈V→∀gVtx⁡g=V∧iEdg⁡g=ABC→g∈UPGraph
15 simpll ⊢V∈W∧A∈X∧B∈V∧C∈V→V∈W
16 snex ⊢ABC∈V
17 16 a1i ⊢V∈W∧A∈X∧B∈V∧C∈V→ABC∈V
18 14 15 17 gropeld ⊢V∈W∧A∈X∧B∈V∧C∈V→VABC∈UPGraph