Metamath Proof Explorer

Theorem umgr2v2e

Description: A multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020)

Ref Expression
Hypothesis umgr2v2evtx.g 
|- G = <. V , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >.
Assertion umgr2v2e 
|- ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> G e. UMGraph )

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g 
 |-  G = <. V , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >.
2 c0ex 
 |-  0 e. _V
3 1ex 
 |-  1 e. _V
4 2 3 pm3.2i 
 |-  ( 0 e. _V /\ 1 e. _V )
5 prex 
 |-  { A , B } e. _V
6 5 5 pm3.2i 
 |-  ( { A , B } e. _V /\ { A , B } e. _V )
7 0ne1 
 |-  0 =/= 1
8 7 a1i 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> 0 =/= 1 )
9 fprg 
 |-  ( ( ( 0 e. _V /\ 1 e. _V ) /\ ( { A , B } e. _V /\ { A , B } e. _V ) /\ 0 =/= 1 ) -> { <. 0 , { A , B } >. , <. 1 , { A , B } >. } : { 0 , 1 } --> { { A , B } , { A , B } } )
10 4 6 8 9 mp3an12i 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> { <. 0 , { A , B } >. , <. 1 , { A , B } >. } : { 0 , 1 } --> { { A , B } , { A , B } } )
11 dfsn2 
 |-  { { A , B } } = { { A , B } , { A , B } }
12 fveqeq2 
 |-  ( e = { A , B } -> ( ( # ` e ) = 2 <-> ( # ` { A , B } ) = 2 ) )
13 prelpwi 
 |-  ( ( A e. V /\ B e. V ) -> { A , B } e. ~P V )
14 13 3adant1 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> { A , B } e. ~P V )
15 1 umgr2v2evtx 
 |-  ( V e. W -> ( Vtx ` G ) = V )
16 15 3ad2ant1 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( Vtx ` G ) = V )
17 16 pweqd 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ~P ( Vtx ` G ) = ~P V )
18 14 17 eleqtrrd 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> { A , B } e. ~P ( Vtx ` G ) )
19 18 adantr 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> { A , B } e. ~P ( Vtx ` G ) )
20 hashprg 
 |-  ( ( A e. V /\ B e. V ) -> ( A =/= B <-> ( # ` { A , B } ) = 2 ) )
21 20 biimpd 
 |-  ( ( A e. V /\ B e. V ) -> ( A =/= B -> ( # ` { A , B } ) = 2 ) )
22 21 3adant1 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( A =/= B -> ( # ` { A , B } ) = 2 ) )
23 22 imp 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( # ` { A , B } ) = 2 )
24 12 19 23 elrabd 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> { A , B } e. { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } )
25 24 snssd 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> { { A , B } } C_ { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } )
26 11 25 eqsstrrid 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> { { A , B } , { A , B } } C_ { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } )
27 10 26 fssd 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> { <. 0 , { A , B } >. , <. 1 , { A , B } >. } : { 0 , 1 } --> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } )
28 27 ffdmd 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> { <. 0 , { A , B } >. , <. 1 , { A , B } >. } : dom { <. 0 , { A , B } >. , <. 1 , { A , B } >. } --> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } )
29 1 umgr2v2eiedg 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( iEdg ` G ) = { <. 0 , { A , B } >. , <. 1 , { A , B } >. } )
30 29 adantr 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( iEdg ` G ) = { <. 0 , { A , B } >. , <. 1 , { A , B } >. } )
31 30 dmeqd 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> dom ( iEdg ` G ) = dom { <. 0 , { A , B } >. , <. 1 , { A , B } >. } )
32 30 31 feq12d 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( ( iEdg ` G ) : dom ( iEdg ` G ) --> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } <-> { <. 0 , { A , B } >. , <. 1 , { A , B } >. } : dom { <. 0 , { A , B } >. , <. 1 , { A , B } >. } --> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } ) )
33 28 32 mpbird 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } )
34 opex 
 |-  <. V , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >. e. _V
35 1 34 eqeltri 
 |-  G e. _V
36 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
37 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
38 36 37 isumgrs 
 |-  ( G e. _V -> ( G e. UMGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } ) )
39 35 38 mp1i 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> ( G e. UMGraph <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> { e e. ~P ( Vtx ` G ) | ( # ` e ) = 2 } ) )
40 33 39 mpbird 
 |-  ( ( ( V e. W /\ A e. V /\ B e. V ) /\ A =/= B ) -> G e. UMGraph )