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 )