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 → V A B C ∈ 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 = A B C → A ∈ X
3 simplrl ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V ∧ Vtx ⁡ g = V ∧ iEdg ⁡ g = A B C → 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 = A B C → B ∈ Vtx ⁡ g ↔ B ∈ V
6 3 5 mpbird ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V ∧ Vtx ⁡ g = V ∧ iEdg ⁡ g = A B C → B ∈ Vtx ⁡ g
7 simplrr ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V ∧ Vtx ⁡ g = V ∧ iEdg ⁡ g = A B C → 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 = A B C → C ∈ Vtx ⁡ g ↔ C ∈ V
10 7 9 mpbird ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V ∧ Vtx ⁡ g = V ∧ iEdg ⁡ g = A B C → C ∈ Vtx ⁡ g
11 simprr ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V ∧ Vtx ⁡ g = V ∧ iEdg ⁡ g = A B C → iEdg ⁡ g = A B C
12 1 2 6 10 11 upgr1e ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V ∧ Vtx ⁡ g = V ∧ iEdg ⁡ g = A B C → g ∈ UPGraph
13 12 ex ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → Vtx ⁡ g = V ∧ iEdg ⁡ g = A B C → g ∈ UPGraph
14 13 alrimiv ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → ∀ g Vtx ⁡ g = V ∧ iEdg ⁡ g = A B C → g ∈ UPGraph
15 simpll ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → V ∈ W
16 snex ⊢ A B C ∈ V
17 16 a1i ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → A B C ∈ V
18 14 15 17 gropeld ⊢ V ∈ W ∧ A ∈ X ∧ B ∈ V ∧ C ∈ V → V A B C ∈ UPGraph