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 )