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

Metamath Proof Explorer

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 )