Metamath Proof Explorer

Theorem upgrreslem

Description: Lemma for upgrres . (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 upgrreslem 
|- ( ( G e. UPGraph /\ 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 upgrf 
 |-  ( G e. UPGraph -> E : dom E --> { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } )
10 ffvelrn 
 |-  ( ( E : dom E --> { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } /\ j e. dom E ) -> ( E ` j ) e. { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } )
11 fveq2 
 |-  ( p = ( E ` j ) -> ( # ` p ) = ( # ` ( E ` j ) ) )
12 11 breq1d 
 |-  ( p = ( E ` j ) -> ( ( # ` p ) <_ 2 <-> ( # ` ( E ` j ) ) <_ 2 ) )
13 12 elrab 
 |-  ( ( E ` j ) e. { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } <-> ( ( E ` j ) e. ( ~P V \ { (/) } ) /\ ( # ` ( E ` j ) ) <_ 2 ) )
14 eldifsn 
 |-  ( ( E ` j ) e. ( ~P V \ { (/) } ) <-> ( ( E ` j ) e. ~P V /\ ( E ` j ) =/= (/) ) )
15 simpl 
 |-  ( ( ( E ` j ) e. ~P V /\ N e/ ( E ` j ) ) -> ( E ` j ) e. ~P V )
16 elpwi 
 |-  ( ( E ` j ) e. ~P V -> ( E ` j ) C_ V )
17 16 adantr 
 |-  ( ( ( E ` j ) e. ~P V /\ N e/ ( E ` j ) ) -> ( E ` j ) C_ V )
18 simpr 
 |-  ( ( ( E ` j ) e. ~P V /\ N e/ ( E ` j ) ) -> N e/ ( E ` j ) )
19 elpwdifsn 
 |-  ( ( ( E ` j ) e. ~P V /\ ( E ` j ) C_ V /\ N e/ ( E ` j ) ) -> ( E ` j ) e. ~P ( V \ { N } ) )
20 15 17 18 19 syl3anc 
 |-  ( ( ( E ` j ) e. ~P V /\ N e/ ( E ` j ) ) -> ( E ` j ) e. ~P ( V \ { N } ) )
21 20 ex 
 |-  ( ( E ` j ) e. ~P V -> ( N e/ ( E ` j ) -> ( E ` j ) e. ~P ( V \ { N } ) ) )
22 21 adantr 
 |-  ( ( ( E ` j ) e. ~P V /\ ( E ` j ) =/= (/) ) -> ( N e/ ( E ` j ) -> ( E ` j ) e. ~P ( V \ { N } ) ) )
23 14 22 sylbi 
 |-  ( ( E ` j ) e. ( ~P V \ { (/) } ) -> ( N e/ ( E ` j ) -> ( E ` j ) e. ~P ( V \ { N } ) ) )
24 23 adantr 
 |-  ( ( ( E ` j ) e. ( ~P V \ { (/) } ) /\ ( # ` ( E ` j ) ) <_ 2 ) -> ( N e/ ( E ` j ) -> ( E ` j ) e. ~P ( V \ { N } ) ) )
25 24 imp 
 |-  ( ( ( ( E ` j ) e. ( ~P V \ { (/) } ) /\ ( # ` ( E ` j ) ) <_ 2 ) /\ N e/ ( E ` j ) ) -> ( E ` j ) e. ~P ( V \ { N } ) )
26 eldifsni 
 |-  ( ( E ` j ) e. ( ~P V \ { (/) } ) -> ( E ` j ) =/= (/) )
27 26 adantr 
 |-  ( ( ( E ` j ) e. ( ~P V \ { (/) } ) /\ ( # ` ( E ` j ) ) <_ 2 ) -> ( E ` j ) =/= (/) )
28 27 adantr 
 |-  ( ( ( ( E ` j ) e. ( ~P V \ { (/) } ) /\ ( # ` ( E ` j ) ) <_ 2 ) /\ N e/ ( E ` j ) ) -> ( E ` j ) =/= (/) )
29 eldifsn 
 |-  ( ( E ` j ) e. ( ~P ( V \ { N } ) \ { (/) } ) <-> ( ( E ` j ) e. ~P ( V \ { N } ) /\ ( E ` j ) =/= (/) ) )
30 25 28 29 sylanbrc 
 |-  ( ( ( ( E ` j ) e. ( ~P V \ { (/) } ) /\ ( # ` ( E ` j ) ) <_ 2 ) /\ N e/ ( E ` j ) ) -> ( E ` j ) e. ( ~P ( V \ { N } ) \ { (/) } ) )
31 simpr 
 |-  ( ( ( E ` j ) e. ( ~P V \ { (/) } ) /\ ( # ` ( E ` j ) ) <_ 2 ) -> ( # ` ( E ` j ) ) <_ 2 )
32 31 adantr 
 |-  ( ( ( ( E ` j ) e. ( ~P V \ { (/) } ) /\ ( # ` ( E ` j ) ) <_ 2 ) /\ N e/ ( E ` j ) ) -> ( # ` ( E ` j ) ) <_ 2 )
33 12 30 32 elrabd 
 |-  ( ( ( ( E ` j ) e. ( ~P V \ { (/) } ) /\ ( # ` ( E ` j ) ) <_ 2 ) /\ N e/ ( E ` j ) ) -> ( E ` j ) e. { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } )
34 33 ex 
 |-  ( ( ( E ` j ) e. ( ~P V \ { (/) } ) /\ ( # ` ( E ` j ) ) <_ 2 ) -> ( N e/ ( E ` j ) -> ( E ` j ) e. { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } ) )
35 34 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 } ) ) )
36 13 35 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 } ) ) )
37 10 36 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 } ) ) )
38 37 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 } ) ) ) )
39 38 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 } ) ) ) )
40 9 39 syl 
 |-  ( G e. UPGraph -> ( N e. V -> ( j e. dom E -> ( N e/ ( E ` j ) -> ( E ` j ) e. { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } ) ) ) )
41 40 imp4b 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( ( j e. dom E /\ N e/ ( E ` j ) ) -> ( E ` j ) e. { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } ) )
42 8 41 syl5bi 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( j e. F -> ( E ` j ) e. { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } ) )
43 42 ralrimiv 
 |-  ( ( G e. UPGraph /\ N e. V ) -> A. j e. F ( E ` j ) e. { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } )
44 upgruhgr 
 |-  ( G e. UPGraph -> G e. UHGraph )
45 2 uhgrfun 
 |-  ( G e. UHGraph -> Fun E )
46 44 45 syl 
 |-  ( G e. UPGraph -> Fun E )
47 46 adantr 
 |-  ( ( G e. UPGraph /\ N e. V ) -> Fun E )
48 3 ssrab3 
 |-  F C_ dom E
49 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 } ) )
50 47 48 49 sylancl 
 |-  ( ( G e. UPGraph /\ 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 } ) )
51 43 50 mpbird 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( E " F ) C_ { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } )
52 4 51 eqsstrrid 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ran ( E |` F ) C_ { p e. ( ~P ( V \ { N } ) \ { (/) } ) | ( # ` p ) <_ 2 } )