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 e. W -> <. V , (/) >. e. UPGraph )

Proof

Step	Hyp	Ref	Expression
1		vex	|- g e. _V
2	1	a1i	|- ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = (/) ) -> g e. _V )
3		simpr	|- ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = (/) ) -> ( iEdg ` g ) = (/) )
4	2 3	upgr0e	|- ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = (/) ) -> g e. UPGraph )
5	4	ax-gen	|- A. g ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = (/) ) -> g e. UPGraph )
6	5	a1i	|- ( V e. W -> A. g ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = (/) ) -> g e. UPGraph ) )
7		id	|- ( V e. W -> V e. W )
8		0ex	|- (/) e. _V
9	8	a1i	|- ( V e. W -> (/) e. _V )
10	6 7 9	gropeld	|- ( V e. W -> <. V , (/) >. e. UPGraph )