This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑉 ∈ 𝑊 → ⟨ 𝑉 , ∅ ⟩ ∈ UPGraph )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑔 ∈ V
2 1 a1i ⊢ ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = ∅ ) → 𝑔 ∈ V )
3 simpr ⊢ ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = ∅ ) → ( iEdg ‘ 𝑔 ) = ∅ )
4 2 3 upgr0e ⊢ ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = ∅ ) → 𝑔 ∈ UPGraph )
5 4 ax-gen ⊢ ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = ∅ ) → 𝑔 ∈ UPGraph )
6 5 a1i ⊢ ( 𝑉 ∈ 𝑊 → ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = ∅ ) → 𝑔 ∈ UPGraph ) )
7 id ⊢ ( 𝑉 ∈ 𝑊 → 𝑉 ∈ 𝑊 )
8 0ex ⊢ ∅ ∈ V
9 8 a1i ⊢ ( 𝑉 ∈ 𝑊 → ∅ ∈ V )
10 6 7 9 gropeld ⊢ ( 𝑉 ∈ 𝑊 → ⟨ 𝑉 , ∅ ⟩ ∈ UPGraph )