Metamath Proof Explorer

Theorem umgrres1lem

Description: Lemma for umgrres1 . (Contributed by AV, 27-Nov-2020)

Ref Expression
Hypotheses upgrres1.v 
|- V = ( Vtx ` G )
upgrres1.e 
|- E = ( Edg ` G )
upgrres1.f 
|- F = { e e. E | N e/ e }
Assertion umgrres1lem 
|- ( ( G e. UMGraph /\ N e. V ) -> ran ( _I |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )

Proof

Step Hyp Ref Expression
1 upgrres1.v 
 |-  V = ( Vtx ` G )
2 upgrres1.e 
 |-  E = ( Edg ` G )
3 upgrres1.f 
 |-  F = { e e. E | N e/ e }
4 rnresi 
 |-  ran ( _I |` F ) = F
5 simpr 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ e e. E ) -> e e. E )
6 5 adantr 
 |-  ( ( ( ( G e. UMGraph /\ N e. V ) /\ e e. E ) /\ N e/ e ) -> e e. E )
7 umgruhgr 
 |-  ( G e. UMGraph -> G e. UHGraph )
8 2 eleq2i 
 |-  ( e e. E <-> e e. ( Edg ` G ) )
9 8 biimpi 
 |-  ( e e. E -> e e. ( Edg ` G ) )
10 edguhgr 
 |-  ( ( G e. UHGraph /\ e e. ( Edg ` G ) ) -> e e. ~P ( Vtx ` G ) )
11 elpwi 
 |-  ( e e. ~P ( Vtx ` G ) -> e C_ ( Vtx ` G ) )
12 11 1 sseqtrrdi 
 |-  ( e e. ~P ( Vtx ` G ) -> e C_ V )
13 10 12 syl 
 |-  ( ( G e. UHGraph /\ e e. ( Edg ` G ) ) -> e C_ V )
14 7 9 13 syl2an 
 |-  ( ( G e. UMGraph /\ e e. E ) -> e C_ V )
15 14 ad4ant13 
 |-  ( ( ( ( G e. UMGraph /\ N e. V ) /\ e e. E ) /\ N e/ e ) -> e C_ V )
16 simpr 
 |-  ( ( ( ( G e. UMGraph /\ N e. V ) /\ e e. E ) /\ N e/ e ) -> N e/ e )
17 elpwdifsn 
 |-  ( ( e e. E /\ e C_ V /\ N e/ e ) -> e e. ~P ( V \ { N } ) )
18 6 15 16 17 syl3anc 
 |-  ( ( ( ( G e. UMGraph /\ N e. V ) /\ e e. E ) /\ N e/ e ) -> e e. ~P ( V \ { N } ) )
19 18 ex 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ e e. E ) -> ( N e/ e -> e e. ~P ( V \ { N } ) ) )
20 19 ralrimiva 
 |-  ( ( G e. UMGraph /\ N e. V ) -> A. e e. E ( N e/ e -> e e. ~P ( V \ { N } ) ) )
21 rabss 
 |-  ( { e e. E | N e/ e } C_ ~P ( V \ { N } ) <-> A. e e. E ( N e/ e -> e e. ~P ( V \ { N } ) ) )
22 20 21 sylibr 
 |-  ( ( G e. UMGraph /\ N e. V ) -> { e e. E | N e/ e } C_ ~P ( V \ { N } ) )
23 3 22 eqsstrid 
 |-  ( ( G e. UMGraph /\ N e. V ) -> F C_ ~P ( V \ { N } ) )
24 elrabi 
 |-  ( p e. { e e. E | N e/ e } -> p e. E )
25 24 2 eleqtrdi 
 |-  ( p e. { e e. E | N e/ e } -> p e. ( Edg ` G ) )
26 edgumgr 
 |-  ( ( G e. UMGraph /\ p e. ( Edg ` G ) ) -> ( p e. ~P ( Vtx ` G ) /\ ( # ` p ) = 2 ) )
27 26 simprd 
 |-  ( ( G e. UMGraph /\ p e. ( Edg ` G ) ) -> ( # ` p ) = 2 )
28 27 ex 
 |-  ( G e. UMGraph -> ( p e. ( Edg ` G ) -> ( # ` p ) = 2 ) )
29 28 adantr 
 |-  ( ( G e. UMGraph /\ N e. V ) -> ( p e. ( Edg ` G ) -> ( # ` p ) = 2 ) )
30 25 29 syl5com 
 |-  ( p e. { e e. E | N e/ e } -> ( ( G e. UMGraph /\ N e. V ) -> ( # ` p ) = 2 ) )
31 30 3 eleq2s 
 |-  ( p e. F -> ( ( G e. UMGraph /\ N e. V ) -> ( # ` p ) = 2 ) )
32 31 impcom 
 |-  ( ( ( G e. UMGraph /\ N e. V ) /\ p e. F ) -> ( # ` p ) = 2 )
33 23 32 ssrabdv 
 |-  ( ( G e. UMGraph /\ N e. V ) -> F C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )
34 4 33 eqsstrid 
 |-  ( ( G e. UMGraph /\ N e. V ) -> ran ( _I |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )