Metamath Proof Explorer

Theorem umgrislfupgr

Description: A multigraph is a loop-free pseudograph. (Contributed by AV, 27-Jan-2021)

Ref Expression
Hypotheses umgrislfupgr.v 
|- V = ( Vtx ` G )
umgrislfupgr.i 
|- I = ( iEdg ` G )
Assertion umgrislfupgr 
|- ( G e. UMGraph <-> ( G e. UPGraph /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) )

Proof

Step Hyp Ref Expression
1 umgrislfupgr.v 
 |-  V = ( Vtx ` G )
2 umgrislfupgr.i 
 |-  I = ( iEdg ` G )
3 umgrupgr 
 |-  ( G e. UMGraph -> G e. UPGraph )
4 1 2 umgrf 
 |-  ( G e. UMGraph -> I : dom I --> { x e. ~P V | ( # ` x ) = 2 } )
5 id 
 |-  ( I : dom I --> { x e. ~P V | ( # ` x ) = 2 } -> I : dom I --> { x e. ~P V | ( # ` x ) = 2 } )
6 2re 
 |-  2 e. RR
7 6 leidi 
 |-  2 <_ 2
8 7 a1i 
 |-  ( ( # ` x ) = 2 -> 2 <_ 2 )
9 breq2 
 |-  ( ( # ` x ) = 2 -> ( 2 <_ ( # ` x ) <-> 2 <_ 2 ) )
10 8 9 mpbird 
 |-  ( ( # ` x ) = 2 -> 2 <_ ( # ` x ) )
11 10 a1i 
 |-  ( x e. ~P V -> ( ( # ` x ) = 2 -> 2 <_ ( # ` x ) ) )
12 11 ss2rabi 
 |-  { x e. ~P V | ( # ` x ) = 2 } C_ { x e. ~P V | 2 <_ ( # ` x ) }
13 12 a1i 
 |-  ( I : dom I --> { x e. ~P V | ( # ` x ) = 2 } -> { x e. ~P V | ( # ` x ) = 2 } C_ { x e. ~P V | 2 <_ ( # ` x ) } )
14 5 13 fssd 
 |-  ( I : dom I --> { x e. ~P V | ( # ` x ) = 2 } -> I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } )
15 4 14 syl 
 |-  ( G e. UMGraph -> I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } )
16 3 15 jca 
 |-  ( G e. UMGraph -> ( G e. UPGraph /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) )
17 1 2 upgrf 
 |-  ( G e. UPGraph -> I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
18 fin 
 |-  ( I : dom I --> ( { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } i^i { x e. ~P V | 2 <_ ( # ` x ) } ) <-> ( I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) )
19 umgrislfupgrlem 
 |-  ( { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } i^i { x e. ~P V | 2 <_ ( # ` x ) } ) = { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 }
20 feq3 
 |-  ( ( { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } i^i { x e. ~P V | 2 <_ ( # ` x ) } ) = { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } -> ( I : dom I --> ( { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } i^i { x e. ~P V | 2 <_ ( # ` x ) } ) <-> I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } ) )
21 19 20 ax-mp 
 |-  ( I : dom I --> ( { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } i^i { x e. ~P V | 2 <_ ( # ` x ) } ) <-> I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } )
22 18 21 sylbb1 
 |-  ( ( I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } )
23 17 22 sylan 
 |-  ( ( G e. UPGraph /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } )
24 1 2 isumgr 
 |-  ( G e. UPGraph -> ( G e. UMGraph <-> I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } ) )
25 24 adantr 
 |-  ( ( G e. UPGraph /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> ( G e. UMGraph <-> I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } ) )
26 23 25 mpbird 
 |-  ( ( G e. UPGraph /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> G e. UMGraph )
27 16 26 impbii 
 |-  ( G e. UMGraph <-> ( G e. UPGraph /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) )