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 e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> <. V , { <. A , { B , C } >. } >. e. UPGraph )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Vtx ` g ) = ( Vtx ` g )
2		simpllr	|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = { <. A , { B , C } >. } ) ) -> A e. X )
3		simplrl	|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = { <. A , { B , C } >. } ) ) -> B e. V )
4		eleq2	|- ( ( Vtx ` g ) = V -> ( B e. ( Vtx ` g ) <-> B e. V ) )
5	4	ad2antrl	|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = { <. A , { B , C } >. } ) ) -> ( B e. ( Vtx ` g ) <-> B e. V ) )
6	3 5	mpbird	|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = { <. A , { B , C } >. } ) ) -> B e. ( Vtx ` g ) )
7		simplrr	|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = { <. A , { B , C } >. } ) ) -> C e. V )
8		eleq2	|- ( ( Vtx ` g ) = V -> ( C e. ( Vtx ` g ) <-> C e. V ) )
9	8	ad2antrl	|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = { <. A , { B , C } >. } ) ) -> ( C e. ( Vtx ` g ) <-> C e. V ) )
10	7 9	mpbird	|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = { <. A , { B , C } >. } ) ) -> C e. ( Vtx ` g ) )
11		simprr	|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = { <. A , { B , C } >. } ) ) -> ( iEdg ` g ) = { <. A , { B , C } >. } )
12	1 2 6 10 11	upgr1e	|- ( ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) /\ ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = { <. A , { B , C } >. } ) ) -> g e. UPGraph )
13	12	ex	|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = { <. A , { B , C } >. } ) -> g e. UPGraph ) )
14	13	alrimiv	|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> A. g ( ( ( Vtx ` g ) = V /\ ( iEdg ` g ) = { <. A , { B , C } >. } ) -> g e. UPGraph ) )
15		simpll	|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> V e. W )
16		snex	|- { <. A , { B , C } >. } e. _V
17	16	a1i	|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> { <. A , { B , C } >. } e. _V )
18	14 15 17	gropeld	|- ( ( ( V e. W /\ A e. X ) /\ ( B e. V /\ C e. V ) ) -> <. V , { <. A , { B , C } >. } >. e. UPGraph )