Metamath Proof Explorer

Theorem usgrislfuspgr

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

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

Proof

Step Hyp Ref Expression
1 usgrislfuspgr.v 
 |-  V = ( Vtx ` G )
2 usgrislfuspgr.i 
 |-  I = ( iEdg ` G )
3 usgruspgr 
 |-  ( G e. USGraph -> G e. USPGraph )
4 1 2 usgrfs 
 |-  ( G e. USGraph -> I : dom I -1-1-> { x e. ~P V | ( # ` x ) = 2 } )
5 f1f 
 |-  ( I : dom I -1-1-> { 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 -1-1-> { 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 -1-1-> { x e. ~P V | ( # ` x ) = 2 } -> I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } )
15 4 14 syl 
 |-  ( G e. USGraph -> I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } )
16 3 15 jca 
 |-  ( G e. USGraph -> ( G e. USPGraph /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) )
17 1 2 uspgrf 
 |-  ( G e. USPGraph -> I : dom I -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
18 df-f1 
 |-  ( I : dom I -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } <-> ( I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } /\ Fun `' I ) )
19 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 ) } ) )
20 umgrislfupgrlem 
 |-  ( { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } i^i { x e. ~P V | 2 <_ ( # ` x ) } ) = { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 }
21 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 } ) )
22 20 21 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 } )
23 19 22 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 } )
24 23 anim1i 
 |-  ( ( ( I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ Fun `' I ) -> ( I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } /\ Fun `' I ) )
25 df-f1 
 |-  ( I : dom I -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } <-> ( I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } /\ Fun `' I ) )
26 24 25 sylibr 
 |-  ( ( ( I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ Fun `' I ) -> I : dom I -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } )
27 26 ex 
 |-  ( ( I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> ( Fun `' I -> I : dom I -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } ) )
28 27 impancom 
 |-  ( ( I : dom I --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } /\ Fun `' I ) -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> I : dom I -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } ) )
29 18 28 sylbi 
 |-  ( I : dom I -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> I : dom I -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } ) )
30 29 imp 
 |-  ( ( I : dom I -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> I : dom I -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } )
31 17 30 sylan 
 |-  ( ( G e. USPGraph /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> I : dom I -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } )
32 1 2 isusgr 
 |-  ( G e. USPGraph -> ( G e. USGraph <-> I : dom I -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } ) )
33 32 adantr 
 |-  ( ( G e. USPGraph /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> ( G e. USGraph <-> I : dom I -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } ) )
34 31 33 mpbird 
 |-  ( ( G e. USPGraph /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> G e. USGraph )
35 16 34 impbii 
 |-  ( G e. USGraph <-> ( G e. USPGraph /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) )