Metamath Proof Explorer

Theorem ausgrusgrb

Description: The equivalence of the definitions of a simple graph. (Contributed by Alexander van der Vekens, 28-Aug-2017) (Revised by AV, 14-Oct-2020)

Ref Expression
Hypothesis ausgr.1 
|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }
Assertion ausgrusgrb 
|- ( ( V e. X /\ E e. Y ) -> ( V G E <-> <. V , ( _I |` E ) >. e. USGraph ) )

Proof

Step Hyp Ref Expression
1 ausgr.1 
 |-  G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }
2 1 isausgr 
 |-  ( ( V e. X /\ E e. Y ) -> ( V G E <-> E C_ { x e. ~P V | ( # ` x ) = 2 } ) )
3 f1oi 
 |-  ( _I |` E ) : E -1-1-onto-> E
4 dff1o5 
 |-  ( ( _I |` E ) : E -1-1-onto-> E <-> ( ( _I |` E ) : E -1-1-> E /\ ran ( _I |` E ) = E ) )
5 f1ss 
 |-  ( ( ( _I |` E ) : E -1-1-> E /\ E C_ { x e. ~P V | ( # ` x ) = 2 } ) -> ( _I |` E ) : E -1-1-> { x e. ~P V | ( # ` x ) = 2 } )
6 dmresi 
 |-  dom ( _I |` E ) = E
7 6 eqcomi 
 |-  E = dom ( _I |` E )
8 f1eq2 
 |-  ( E = dom ( _I |` E ) -> ( ( _I |` E ) : E -1-1-> { x e. ~P V | ( # ` x ) = 2 } <-> ( _I |` E ) : dom ( _I |` E ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } ) )
9 7 8 ax-mp 
 |-  ( ( _I |` E ) : E -1-1-> { x e. ~P V | ( # ` x ) = 2 } <-> ( _I |` E ) : dom ( _I |` E ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } )
10 5 9 sylib 
 |-  ( ( ( _I |` E ) : E -1-1-> E /\ E C_ { x e. ~P V | ( # ` x ) = 2 } ) -> ( _I |` E ) : dom ( _I |` E ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } )
11 10 ex 
 |-  ( ( _I |` E ) : E -1-1-> E -> ( E C_ { x e. ~P V | ( # ` x ) = 2 } -> ( _I |` E ) : dom ( _I |` E ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } ) )
12 11 a1d 
 |-  ( ( _I |` E ) : E -1-1-> E -> ( ( V e. X /\ E e. Y ) -> ( E C_ { x e. ~P V | ( # ` x ) = 2 } -> ( _I |` E ) : dom ( _I |` E ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } ) ) )
13 12 adantr 
 |-  ( ( ( _I |` E ) : E -1-1-> E /\ ran ( _I |` E ) = E ) -> ( ( V e. X /\ E e. Y ) -> ( E C_ { x e. ~P V | ( # ` x ) = 2 } -> ( _I |` E ) : dom ( _I |` E ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } ) ) )
14 4 13 sylbi 
 |-  ( ( _I |` E ) : E -1-1-onto-> E -> ( ( V e. X /\ E e. Y ) -> ( E C_ { x e. ~P V | ( # ` x ) = 2 } -> ( _I |` E ) : dom ( _I |` E ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } ) ) )
15 3 14 ax-mp 
 |-  ( ( V e. X /\ E e. Y ) -> ( E C_ { x e. ~P V | ( # ` x ) = 2 } -> ( _I |` E ) : dom ( _I |` E ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } ) )
16 df-f 
 |-  ( ( _I |` E ) : dom ( _I |` E ) --> { x e. ~P V | ( # ` x ) = 2 } <-> ( ( _I |` E ) Fn dom ( _I |` E ) /\ ran ( _I |` E ) C_ { x e. ~P V | ( # ` x ) = 2 } ) )
17 rnresi 
 |-  ran ( _I |` E ) = E
18 17 sseq1i 
 |-  ( ran ( _I |` E ) C_ { x e. ~P V | ( # ` x ) = 2 } <-> E C_ { x e. ~P V | ( # ` x ) = 2 } )
19 18 biimpi 
 |-  ( ran ( _I |` E ) C_ { x e. ~P V | ( # ` x ) = 2 } -> E C_ { x e. ~P V | ( # ` x ) = 2 } )
20 19 a1d 
 |-  ( ran ( _I |` E ) C_ { x e. ~P V | ( # ` x ) = 2 } -> ( ( V e. X /\ E e. Y ) -> E C_ { x e. ~P V | ( # ` x ) = 2 } ) )
21 16 20 simplbiim 
 |-  ( ( _I |` E ) : dom ( _I |` E ) --> { x e. ~P V | ( # ` x ) = 2 } -> ( ( V e. X /\ E e. Y ) -> E C_ { x e. ~P V | ( # ` x ) = 2 } ) )
22 f1f 
 |-  ( ( _I |` E ) : dom ( _I |` E ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } -> ( _I |` E ) : dom ( _I |` E ) --> { x e. ~P V | ( # ` x ) = 2 } )
23 21 22 syl11 
 |-  ( ( V e. X /\ E e. Y ) -> ( ( _I |` E ) : dom ( _I |` E ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } -> E C_ { x e. ~P V | ( # ` x ) = 2 } ) )
24 15 23 impbid 
 |-  ( ( V e. X /\ E e. Y ) -> ( E C_ { x e. ~P V | ( # ` x ) = 2 } <-> ( _I |` E ) : dom ( _I |` E ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } ) )
25 resiexg 
 |-  ( E e. Y -> ( _I |` E ) e. _V )
26 opiedgfv 
 |-  ( ( V e. X /\ ( _I |` E ) e. _V ) -> ( iEdg ` <. V , ( _I |` E ) >. ) = ( _I |` E ) )
27 25 26 sylan2 
 |-  ( ( V e. X /\ E e. Y ) -> ( iEdg ` <. V , ( _I |` E ) >. ) = ( _I |` E ) )
28 27 dmeqd 
 |-  ( ( V e. X /\ E e. Y ) -> dom ( iEdg ` <. V , ( _I |` E ) >. ) = dom ( _I |` E ) )
29 opvtxfv 
 |-  ( ( V e. X /\ ( _I |` E ) e. _V ) -> ( Vtx ` <. V , ( _I |` E ) >. ) = V )
30 25 29 sylan2 
 |-  ( ( V e. X /\ E e. Y ) -> ( Vtx ` <. V , ( _I |` E ) >. ) = V )
31 30 pweqd 
 |-  ( ( V e. X /\ E e. Y ) -> ~P ( Vtx ` <. V , ( _I |` E ) >. ) = ~P V )
32 31 rabeqdv 
 |-  ( ( V e. X /\ E e. Y ) -> { x e. ~P ( Vtx ` <. V , ( _I |` E ) >. ) | ( # ` x ) = 2 } = { x e. ~P V | ( # ` x ) = 2 } )
33 27 28 32 f1eq123d 
 |-  ( ( V e. X /\ E e. Y ) -> ( ( iEdg ` <. V , ( _I |` E ) >. ) : dom ( iEdg ` <. V , ( _I |` E ) >. ) -1-1-> { x e. ~P ( Vtx ` <. V , ( _I |` E ) >. ) | ( # ` x ) = 2 } <-> ( _I |` E ) : dom ( _I |` E ) -1-1-> { x e. ~P V | ( # ` x ) = 2 } ) )
34 24 33 bitr4d 
 |-  ( ( V e. X /\ E e. Y ) -> ( E C_ { x e. ~P V | ( # ` x ) = 2 } <-> ( iEdg ` <. V , ( _I |` E ) >. ) : dom ( iEdg ` <. V , ( _I |` E ) >. ) -1-1-> { x e. ~P ( Vtx ` <. V , ( _I |` E ) >. ) | ( # ` x ) = 2 } ) )
35 opex 
 |-  <. V , ( _I |` E ) >. e. _V
36 eqid 
 |-  ( Vtx ` <. V , ( _I |` E ) >. ) = ( Vtx ` <. V , ( _I |` E ) >. )
37 eqid 
 |-  ( iEdg ` <. V , ( _I |` E ) >. ) = ( iEdg ` <. V , ( _I |` E ) >. )
38 36 37 isusgrs 
 |-  ( <. V , ( _I |` E ) >. e. _V -> ( <. V , ( _I |` E ) >. e. USGraph <-> ( iEdg ` <. V , ( _I |` E ) >. ) : dom ( iEdg ` <. V , ( _I |` E ) >. ) -1-1-> { x e. ~P ( Vtx ` <. V , ( _I |` E ) >. ) | ( # ` x ) = 2 } ) )
39 35 38 ax-mp 
 |-  ( <. V , ( _I |` E ) >. e. USGraph <-> ( iEdg ` <. V , ( _I |` E ) >. ) : dom ( iEdg ` <. V , ( _I |` E ) >. ) -1-1-> { x e. ~P ( Vtx ` <. V , ( _I |` E ) >. ) | ( # ` x ) = 2 } )
40 39 bicomi 
 |-  ( ( iEdg ` <. V , ( _I |` E ) >. ) : dom ( iEdg ` <. V , ( _I |` E ) >. ) -1-1-> { x e. ~P ( Vtx ` <. V , ( _I |` E ) >. ) | ( # ` x ) = 2 } <-> <. V , ( _I |` E ) >. e. USGraph )
41 40 a1i 
 |-  ( ( V e. X /\ E e. Y ) -> ( ( iEdg ` <. V , ( _I |` E ) >. ) : dom ( iEdg ` <. V , ( _I |` E ) >. ) -1-1-> { x e. ~P ( Vtx ` <. V , ( _I |` E ) >. ) | ( # ` x ) = 2 } <-> <. V , ( _I |` E ) >. e. USGraph ) )
42 2 34 41 3bitrd 
 |-  ( ( V e. X /\ E e. Y ) -> ( V G E <-> <. V , ( _I |` E ) >. e. USGraph ) )