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

Metamath Proof Explorer

Theorem upgr1e

Description: A pseudograph with one edge. Such a graph is actually a simple pseudograph, see uspgr1e . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 16-Oct-2020) (Revised by AV, 21-Mar-2021) (Proof shortened by AV, 17-Apr-2021)

Ref Expression
Hypotheses upgr1e.v 
|- V = ( Vtx ` G )
upgr1e.a 
|- ( ph -> A e. X )
upgr1e.b 
|- ( ph -> B e. V )
upgr1e.c 
|- ( ph -> C e. V )
upgr1e.e 
|- ( ph -> ( iEdg ` G ) = { <. A , { B , C } >. } )
Assertion upgr1e 
|- ( ph -> G e. UPGraph )

Proof

Step Hyp Ref Expression
1 upgr1e.v 
 |-  V = ( Vtx ` G )
2 upgr1e.a 
 |-  ( ph -> A e. X )
3 upgr1e.b 
 |-  ( ph -> B e. V )
4 upgr1e.c 
 |-  ( ph -> C e. V )
5 upgr1e.e 
 |-  ( ph -> ( iEdg ` G ) = { <. A , { B , C } >. } )
6 prex 
 |-  { B , C } e. _V
7 6 snid 
 |-  { B , C } e. { { B , C } }
8 7 a1i 
 |-  ( ph -> { B , C } e. { { B , C } } )
9 2 8 fsnd 
 |-  ( ph -> { <. A , { B , C } >. } : { A } --> { { B , C } } )
10 3 4 prssd 
 |-  ( ph -> { B , C } C_ V )
11 10 1 sseqtrdi 
 |-  ( ph -> { B , C } C_ ( Vtx ` G ) )
12 6 elpw 
 |-  ( { B , C } e. ~P ( Vtx ` G ) <-> { B , C } C_ ( Vtx ` G ) )
13 11 12 sylibr 
 |-  ( ph -> { B , C } e. ~P ( Vtx ` G ) )
14 13 3 upgr1elem 
 |-  ( ph -> { { B , C } } C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
15 9 14 fssd 
 |-  ( ph -> { <. A , { B , C } >. } : { A } --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
16 15 ffdmd 
 |-  ( ph -> { <. A , { B , C } >. } : dom { <. A , { B , C } >. } --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
17 5 dmeqd 
 |-  ( ph -> dom ( iEdg ` G ) = dom { <. A , { B , C } >. } )
18 5 17 feq12d 
 |-  ( ph -> ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } <-> { <. A , { B , C } >. } : dom { <. A , { B , C } >. } --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
19 16 18 mpbird 
 |-  ( ph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
20 1 1vgrex 
 |-  ( B e. V -> G e. _V )
21 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
22 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
23 21 22 isupgr 
 |-  ( G e. _V -> ( G e. UPGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
24 3 20 23 3syl 
 |-  ( ph -> ( G e. UPGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
25 19 24 mpbird 
 |-  ( ph -> G e. UPGraph )