Metamath Proof Explorer

Theorem uspgr1e

Description: A simple pseudograph with one edge. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020) (Revised by AV, 21-Mar-2021) (Proof shortened by AV, 17-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 uspgr1e.v 
 |-  V = ( Vtx ` G )
2 uspgr1e.a 
 |-  ( ph -> A e. X )
3 uspgr1e.b 
 |-  ( ph -> B e. V )
4 uspgr1e.c 
 |-  ( ph -> C e. V )
5 uspgr1e.e 
 |-  ( ph -> ( iEdg ` G ) = { <. A , { B , C } >. } )
6 prex 
 |-  { B , C } e. _V
7 6 snid 
 |-  { B , C } e. { { B , C } }
8 f1sng 
 |-  ( ( A e. X /\ { B , C } e. { { B , C } } ) -> { <. A , { B , C } >. } : { A } -1-1-> { { B , C } } )
9 2 7 8 sylancl 
 |-  ( ph -> { <. A , { B , C } >. } : { A } -1-1-> { { 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 f1ss 
 |-  ( ( { <. A , { B , C } >. } : { A } -1-1-> { { B , C } } /\ { { B , C } } C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) -> { <. A , { B , C } >. } : { A } -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
16 9 14 15 syl2anc 
 |-  ( ph -> { <. A , { B , C } >. } : { A } -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
17 6 a1i 
 |-  ( ph -> { B , C } e. _V )
18 17 3 upgr1elem 
 |-  ( ph -> { { B , C } } C_ { x e. ( _V \ { (/) } ) | ( # ` x ) <_ 2 } )
19 f1ss 
 |-  ( ( { <. A , { B , C } >. } : { A } -1-1-> { { B , C } } /\ { { B , C } } C_ { x e. ( _V \ { (/) } ) | ( # ` x ) <_ 2 } ) -> { <. A , { B , C } >. } : { A } -1-1-> { x e. ( _V \ { (/) } ) | ( # ` x ) <_ 2 } )
20 9 18 19 syl2anc 
 |-  ( ph -> { <. A , { B , C } >. } : { A } -1-1-> { x e. ( _V \ { (/) } ) | ( # ` x ) <_ 2 } )
21 f1dm 
 |-  ( { <. A , { B , C } >. } : { A } -1-1-> { x e. ( _V \ { (/) } ) | ( # ` x ) <_ 2 } -> dom { <. A , { B , C } >. } = { A } )
22 f1eq2 
 |-  ( dom { <. A , { B , C } >. } = { A } -> ( { <. A , { B , C } >. } : dom { <. A , { B , C } >. } -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } <-> { <. A , { B , C } >. } : { A } -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
23 20 21 22 3syl 
 |-  ( ph -> ( { <. A , { B , C } >. } : dom { <. A , { B , C } >. } -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } <-> { <. A , { B , C } >. } : { A } -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
24 16 23 mpbird 
 |-  ( ph -> { <. A , { B , C } >. } : dom { <. A , { B , C } >. } -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
25 5 dmeqd 
 |-  ( ph -> dom ( iEdg ` G ) = dom { <. A , { B , C } >. } )
26 eqidd 
 |-  ( ph -> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } = { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
27 5 25 26 f1eq123d 
 |-  ( ph -> ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } <-> { <. A , { B , C } >. } : dom { <. A , { B , C } >. } -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
28 24 27 mpbird 
 |-  ( ph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
29 1 1vgrex 
 |-  ( B e. V -> G e. _V )
30 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
31 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
32 30 31 isuspgr 
 |-  ( G e. _V -> ( G e. USPGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
33 3 29 32 3syl 
 |-  ( ph -> ( G e. USPGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
34 28 33 mpbird 
 |-  ( ph -> G e. USPGraph )