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