Metamath Proof Explorer

Theorem usgruspgrb

Description: A class is a simple graph iff it is a simple pseudograph without loops. (Contributed by AV, 18-Oct-2020)

Ref Expression
Assertion usgruspgrb 
|- ( G e. USGraph <-> ( G e. USPGraph /\ A. e e. ( Edg ` G ) ( # ` e ) = 2 ) )

Proof

Step Hyp Ref Expression
1 usgruspgr 
 |-  ( G e. USGraph -> G e. USPGraph )
2 edgusgr 
 |-  ( ( G e. USGraph /\ e e. ( Edg ` G ) ) -> ( e e. ~P ( Vtx ` G ) /\ ( # ` e ) = 2 ) )
3 2 simprd 
 |-  ( ( G e. USGraph /\ e e. ( Edg ` G ) ) -> ( # ` e ) = 2 )
4 3 ralrimiva 
 |-  ( G e. USGraph -> A. e e. ( Edg ` G ) ( # ` e ) = 2 )
5 1 4 jca 
 |-  ( G e. USGraph -> ( G e. USPGraph /\ A. e e. ( Edg ` G ) ( # ` e ) = 2 ) )
6 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
7 6 a1i 
 |-  ( G e. USPGraph -> ( Edg ` G ) = ran ( iEdg ` G ) )
8 7 raleqdv 
 |-  ( G e. USPGraph -> ( A. e e. ( Edg ` G ) ( # ` e ) = 2 <-> A. e e. ran ( iEdg ` G ) ( # ` e ) = 2 ) )
9 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
10 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
11 9 10 uspgrf 
 |-  ( G e. USPGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
12 f1f 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
13 12 frnd 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> ran ( iEdg ` G ) C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
14 ssel2 
 |-  ( ( ran ( iEdg ` G ) C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } /\ y e. ran ( iEdg ` G ) ) -> y e. { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } )
15 14 expcom 
 |-  ( y e. ran ( iEdg ` G ) -> ( ran ( iEdg ` G ) C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> y e. { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) )
16 fveqeq2 
 |-  ( e = y -> ( ( # ` e ) = 2 <-> ( # ` y ) = 2 ) )
17 16 rspcv 
 |-  ( y e. ran ( iEdg ` G ) -> ( A. e e. ran ( iEdg ` G ) ( # ` e ) = 2 -> ( # ` y ) = 2 ) )
18 fveq2 
 |-  ( x = y -> ( # ` x ) = ( # ` y ) )
19 18 breq1d 
 |-  ( x = y -> ( ( # ` x ) <_ 2 <-> ( # ` y ) <_ 2 ) )
20 19 elrab 
 |-  ( y e. { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } <-> ( y e. ( ~P ( Vtx ` G ) \ { (/) } ) /\ ( # ` y ) <_ 2 ) )
21 eldifi 
 |-  ( y e. ( ~P ( Vtx ` G ) \ { (/) } ) -> y e. ~P ( Vtx ` G ) )
22 21 anim1i 
 |-  ( ( y e. ( ~P ( Vtx ` G ) \ { (/) } ) /\ ( # ` y ) = 2 ) -> ( y e. ~P ( Vtx ` G ) /\ ( # ` y ) = 2 ) )
23 fveqeq2 
 |-  ( x = y -> ( ( # ` x ) = 2 <-> ( # ` y ) = 2 ) )
24 23 elrab 
 |-  ( y e. { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } <-> ( y e. ~P ( Vtx ` G ) /\ ( # ` y ) = 2 ) )
25 22 24 sylibr 
 |-  ( ( y e. ( ~P ( Vtx ` G ) \ { (/) } ) /\ ( # ` y ) = 2 ) -> y e. { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } )
26 25 ex 
 |-  ( y e. ( ~P ( Vtx ` G ) \ { (/) } ) -> ( ( # ` y ) = 2 -> y e. { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) )
27 26 adantr 
 |-  ( ( y e. ( ~P ( Vtx ` G ) \ { (/) } ) /\ ( # ` y ) <_ 2 ) -> ( ( # ` y ) = 2 -> y e. { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) )
28 20 27 sylbi 
 |-  ( y e. { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> ( ( # ` y ) = 2 -> y e. { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) )
29 17 28 syl9 
 |-  ( y e. ran ( iEdg ` G ) -> ( y e. { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> ( A. e e. ran ( iEdg ` G ) ( # ` e ) = 2 -> y e. { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) ) )
30 15 29 syld 
 |-  ( y e. ran ( iEdg ` G ) -> ( ran ( iEdg ` G ) C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> ( A. e e. ran ( iEdg ` G ) ( # ` e ) = 2 -> y e. { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) ) )
31 30 com13 
 |-  ( A. e e. ran ( iEdg ` G ) ( # ` e ) = 2 -> ( ran ( iEdg ` G ) C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> ( y e. ran ( iEdg ` G ) -> y e. { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) ) )
32 31 imp 
 |-  ( ( A. e e. ran ( iEdg ` G ) ( # ` e ) = 2 /\ ran ( iEdg ` G ) C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) -> ( y e. ran ( iEdg ` G ) -> y e. { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) )
33 32 ssrdv 
 |-  ( ( A. e e. ran ( iEdg ` G ) ( # ` e ) = 2 /\ ran ( iEdg ` G ) C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } ) -> ran ( iEdg ` G ) C_ { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } )
34 33 ex 
 |-  ( A. e e. ran ( iEdg ` G ) ( # ` e ) = 2 -> ( ran ( iEdg ` G ) C_ { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> ran ( iEdg ` G ) C_ { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) )
35 13 34 mpan9 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } /\ A. e e. ran ( iEdg ` G ) ( # ` e ) = 2 ) -> ran ( iEdg ` G ) C_ { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } )
36 f1ssr 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } /\ ran ( iEdg ` G ) C_ { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } )
37 35 36 syldan 
 |-  ( ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } /\ A. e e. ran ( iEdg ` G ) ( # ` e ) = 2 ) -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } )
38 37 ex 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ( ~P ( Vtx ` G ) \ { (/) } ) | ( # ` x ) <_ 2 } -> ( A. e e. ran ( iEdg ` G ) ( # ` e ) = 2 -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) )
39 11 38 syl 
 |-  ( G e. USPGraph -> ( A. e e. ran ( iEdg ` G ) ( # ` e ) = 2 -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) )
40 8 39 sylbid 
 |-  ( G e. USPGraph -> ( A. e e. ( Edg ` G ) ( # ` e ) = 2 -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) )
41 40 imp 
 |-  ( ( G e. USPGraph /\ A. e e. ( Edg ` G ) ( # ` e ) = 2 ) -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } )
42 9 10 isusgrs 
 |-  ( G e. USPGraph -> ( G e. USGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) )
43 42 adantr 
 |-  ( ( G e. USPGraph /\ A. e e. ( Edg ` G ) ( # ` e ) = 2 ) -> ( G e. USGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> { x e. ~P ( Vtx ` G ) | ( # ` x ) = 2 } ) )
44 41 43 mpbird 
 |-  ( ( G e. USPGraph /\ A. e e. ( Edg ` G ) ( # ` e ) = 2 ) -> G e. USGraph )
45 5 44 impbii 
 |-  ( G e. USGraph <-> ( G e. USPGraph /\ A. e e. ( Edg ` G ) ( # ` e ) = 2 ) )