Metamath Proof Explorer

Theorem umgrreslem

Description: Lemma for umgrres and usgrres . (Contributed by AV, 27-Nov-2020) (Revised by AV, 19-Dec-2021)

Ref Expression
Hypotheses upgrres.v 
|- V = ( Vtx ` G )
upgrres.e 
|- E = ( iEdg ` G )
upgrres.f 
|- F = { i e. dom E | N e/ ( E ` i ) }
Assertion umgrreslem 
|- ( ( G e. UMGraph /\ N e. V ) -> ran ( E |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )

Proof

Step Hyp Ref Expression
1 upgrres.v 
 |-  V = ( Vtx ` G )
2 upgrres.e 
 |-  E = ( iEdg ` G )
3 upgrres.f 
 |-  F = { i e. dom E | N e/ ( E ` i ) }
4 df-ima 
 |-  ( E " F ) = ran ( E |` F )
5 fveq2 
 |-  ( i = j -> ( E ` i ) = ( E ` j ) )
6 neleq2 
 |-  ( ( E ` i ) = ( E ` j ) -> ( N e/ ( E ` i ) <-> N e/ ( E ` j ) ) )
7 5 6 syl 
 |-  ( i = j -> ( N e/ ( E ` i ) <-> N e/ ( E ` j ) ) )
8 7 3 elrab2 
 |-  ( j e. F <-> ( j e. dom E /\ N e/ ( E ` j ) ) )
9 1 2 umgrf 
 |-  ( G e. UMGraph -> E : dom E --> { p e. ~P V | ( # ` p ) = 2 } )
10 ffvelcdm 
 |-  ( ( E : dom E --> { p e. ~P V | ( # ` p ) = 2 } /\ j e. dom E ) -> ( E ` j ) e. { p e. ~P V | ( # ` p ) = 2 } )
11 fveqeq2 
 |-  ( p = ( E ` j ) -> ( ( # ` p ) = 2 <-> ( # ` ( E ` j ) ) = 2 ) )
12 11 elrab 
 |-  ( ( E ` j ) e. { p e. ~P V | ( # ` p ) = 2 } <-> ( ( E ` j ) e. ~P V /\ ( # ` ( E ` j ) ) = 2 ) )
13 simpll 
 |-  ( ( ( ( E ` j ) e. ~P V /\ ( # ` ( E ` j ) ) = 2 ) /\ N e/ ( E ` j ) ) -> ( E ` j ) e. ~P V )
14 elpwi 
 |-  ( ( E ` j ) e. ~P V -> ( E ` j ) C_ V )
15 14 adantr 
 |-  ( ( ( E ` j ) e. ~P V /\ ( # ` ( E ` j ) ) = 2 ) -> ( E ` j ) C_ V )
16 15 adantr 
 |-  ( ( ( ( E ` j ) e. ~P V /\ ( # ` ( E ` j ) ) = 2 ) /\ N e/ ( E ` j ) ) -> ( E ` j ) C_ V )
17 simpr 
 |-  ( ( ( ( E ` j ) e. ~P V /\ ( # ` ( E ` j ) ) = 2 ) /\ N e/ ( E ` j ) ) -> N e/ ( E ` j ) )
18 elpwdifsn 
 |-  ( ( ( E ` j ) e. ~P V /\ ( E ` j ) C_ V /\ N e/ ( E ` j ) ) -> ( E ` j ) e. ~P ( V \ { N } ) )
19 13 16 17 18 syl3anc 
 |-  ( ( ( ( E ` j ) e. ~P V /\ ( # ` ( E ` j ) ) = 2 ) /\ N e/ ( E ` j ) ) -> ( E ` j ) e. ~P ( V \ { N } ) )
20 simpr 
 |-  ( ( ( E ` j ) e. ~P V /\ ( # ` ( E ` j ) ) = 2 ) -> ( # ` ( E ` j ) ) = 2 )
21 20 adantr 
 |-  ( ( ( ( E ` j ) e. ~P V /\ ( # ` ( E ` j ) ) = 2 ) /\ N e/ ( E ` j ) ) -> ( # ` ( E ` j ) ) = 2 )
22 11 19 21 elrabd 
 |-  ( ( ( ( E ` j ) e. ~P V /\ ( # ` ( E ` j ) ) = 2 ) /\ N e/ ( E ` j ) ) -> ( E ` j ) e. { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )
23 22 ex 
 |-  ( ( ( E ` j ) e. ~P V /\ ( # ` ( E ` j ) ) = 2 ) -> ( N e/ ( E ` j ) -> ( E ` j ) e. { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) )
24 23 a1d 
 |-  ( ( ( E ` j ) e. ~P V /\ ( # ` ( E ` j ) ) = 2 ) -> ( N e. V -> ( N e/ ( E ` j ) -> ( E ` j ) e. { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) ) )
25 12 24 sylbi 
 |-  ( ( E ` j ) e. { p e. ~P V | ( # ` p ) = 2 } -> ( N e. V -> ( N e/ ( E ` j ) -> ( E ` j ) e. { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) ) )
26 10 25 syl 
 |-  ( ( E : dom E --> { p e. ~P V | ( # ` p ) = 2 } /\ j e. dom E ) -> ( N e. V -> ( N e/ ( E ` j ) -> ( E ` j ) e. { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) ) )
27 26 ex 
 |-  ( E : dom E --> { p e. ~P V | ( # ` p ) = 2 } -> ( j e. dom E -> ( N e. V -> ( N e/ ( E ` j ) -> ( E ` j ) e. { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) ) ) )
28 27 com23 
 |-  ( E : dom E --> { p e. ~P V | ( # ` p ) = 2 } -> ( N e. V -> ( j e. dom E -> ( N e/ ( E ` j ) -> ( E ` j ) e. { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) ) ) )
29 9 28 syl 
 |-  ( G e. UMGraph -> ( N e. V -> ( j e. dom E -> ( N e/ ( E ` j ) -> ( E ` j ) e. { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) ) ) )
30 29 imp4b 
 |-  ( ( G e. UMGraph /\ N e. V ) -> ( ( j e. dom E /\ N e/ ( E ` j ) ) -> ( E ` j ) e. { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) )
31 8 30 biimtrid 
 |-  ( ( G e. UMGraph /\ N e. V ) -> ( j e. F -> ( E ` j ) e. { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) )
32 31 ralrimiv 
 |-  ( ( G e. UMGraph /\ N e. V ) -> A. j e. F ( E ` j ) e. { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )
33 umgruhgr 
 |-  ( G e. UMGraph -> G e. UHGraph )
34 2 uhgrfun 
 |-  ( G e. UHGraph -> Fun E )
35 33 34 syl 
 |-  ( G e. UMGraph -> Fun E )
36 35 adantr 
 |-  ( ( G e. UMGraph /\ N e. V ) -> Fun E )
37 3 ssrab3 
 |-  F C_ dom E
38 funimass4 
 |-  ( ( Fun E /\ F C_ dom E ) -> ( ( E " F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } <-> A. j e. F ( E ` j ) e. { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) )
39 36 37 38 sylancl 
 |-  ( ( G e. UMGraph /\ N e. V ) -> ( ( E " F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } <-> A. j e. F ( E ` j ) e. { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } ) )
40 32 39 mpbird 
 |-  ( ( G e. UMGraph /\ N e. V ) -> ( E " F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )
41 4 40 eqsstrrid 
 |-  ( ( G e. UMGraph /\ N e. V ) -> ran ( E |` F ) C_ { p e. ~P ( V \ { N } ) | ( # ` p ) = 2 } )