Metamath Proof Explorer

Theorem umgrislfupgrlem

Description: Lemma for umgrislfupgr and usgrislfuspgr . (Contributed by AV, 27-Jan-2021)

Ref Expression
Assertion umgrislfupgrlem 
|- ( { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } i^i { x e. ~P V | 2 <_ ( # ` x ) } ) = { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 }

Proof

Step Hyp Ref Expression
1 2pos 
 |-  0 < 2
2 simprl 
 |-  ( ( 0 < 2 /\ ( x e. ~P V /\ 2 <_ ( # ` x ) ) ) -> x e. ~P V )
3 fveq2 
 |-  ( x = (/) -> ( # ` x ) = ( # ` (/) ) )
4 hash0 
 |-  ( # ` (/) ) = 0
5 3 4 eqtrdi 
 |-  ( x = (/) -> ( # ` x ) = 0 )
6 5 breq2d 
 |-  ( x = (/) -> ( 2 <_ ( # ` x ) <-> 2 <_ 0 ) )
7 2re 
 |-  2 e. RR
8 0re 
 |-  0 e. RR
9 7 8 lenlti 
 |-  ( 2 <_ 0 <-> -. 0 < 2 )
10 pm2.21 
 |-  ( -. 0 < 2 -> ( 0 < 2 -> x =/= (/) ) )
11 9 10 sylbi 
 |-  ( 2 <_ 0 -> ( 0 < 2 -> x =/= (/) ) )
12 6 11 syl6bi 
 |-  ( x = (/) -> ( 2 <_ ( # ` x ) -> ( 0 < 2 -> x =/= (/) ) ) )
13 12 adantld 
 |-  ( x = (/) -> ( ( x e. ~P V /\ 2 <_ ( # ` x ) ) -> ( 0 < 2 -> x =/= (/) ) ) )
14 13 impcomd 
 |-  ( x = (/) -> ( ( 0 < 2 /\ ( x e. ~P V /\ 2 <_ ( # ` x ) ) ) -> x =/= (/) ) )
15 ax-1 
 |-  ( x =/= (/) -> ( ( 0 < 2 /\ ( x e. ~P V /\ 2 <_ ( # ` x ) ) ) -> x =/= (/) ) )
16 14 15 pm2.61ine 
 |-  ( ( 0 < 2 /\ ( x e. ~P V /\ 2 <_ ( # ` x ) ) ) -> x =/= (/) )
17 eldifsn 
 |-  ( x e. ( ~P V \ { (/) } ) <-> ( x e. ~P V /\ x =/= (/) ) )
18 2 16 17 sylanbrc 
 |-  ( ( 0 < 2 /\ ( x e. ~P V /\ 2 <_ ( # ` x ) ) ) -> x e. ( ~P V \ { (/) } ) )
19 simprr 
 |-  ( ( 0 < 2 /\ ( x e. ~P V /\ 2 <_ ( # ` x ) ) ) -> 2 <_ ( # ` x ) )
20 18 19 jca 
 |-  ( ( 0 < 2 /\ ( x e. ~P V /\ 2 <_ ( # ` x ) ) ) -> ( x e. ( ~P V \ { (/) } ) /\ 2 <_ ( # ` x ) ) )
21 20 ex 
 |-  ( 0 < 2 -> ( ( x e. ~P V /\ 2 <_ ( # ` x ) ) -> ( x e. ( ~P V \ { (/) } ) /\ 2 <_ ( # ` x ) ) ) )
22 eldifi 
 |-  ( x e. ( ~P V \ { (/) } ) -> x e. ~P V )
23 22 anim1i 
 |-  ( ( x e. ( ~P V \ { (/) } ) /\ 2 <_ ( # ` x ) ) -> ( x e. ~P V /\ 2 <_ ( # ` x ) ) )
24 21 23 impbid1 
 |-  ( 0 < 2 -> ( ( x e. ~P V /\ 2 <_ ( # ` x ) ) <-> ( x e. ( ~P V \ { (/) } ) /\ 2 <_ ( # ` x ) ) ) )
25 24 rabbidva2 
 |-  ( 0 < 2 -> { x e. ~P V | 2 <_ ( # ` x ) } = { x e. ( ~P V \ { (/) } ) | 2 <_ ( # ` x ) } )
26 1 25 ax-mp 
 |-  { x e. ~P V | 2 <_ ( # ` x ) } = { x e. ( ~P V \ { (/) } ) | 2 <_ ( # ` x ) }
27 26 ineq2i 
 |-  ( { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } i^i { x e. ~P V | 2 <_ ( # ` x ) } ) = ( { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } i^i { x e. ( ~P V \ { (/) } ) | 2 <_ ( # ` x ) } )
28 inrab 
 |-  ( { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } i^i { x e. ( ~P V \ { (/) } ) | 2 <_ ( # ` x ) } ) = { x e. ( ~P V \ { (/) } ) | ( ( # ` x ) <_ 2 /\ 2 <_ ( # ` x ) ) }
29 hashxnn0 
 |-  ( x e. _V -> ( # ` x ) e. NN0* )
30 29 elv 
 |-  ( # ` x ) e. NN0*
31 xnn0xr 
 |-  ( ( # ` x ) e. NN0* -> ( # ` x ) e. RR* )
32 30 31 ax-mp 
 |-  ( # ` x ) e. RR*
33 7 rexri 
 |-  2 e. RR*
34 xrletri3 
 |-  ( ( ( # ` x ) e. RR* /\ 2 e. RR* ) -> ( ( # ` x ) = 2 <-> ( ( # ` x ) <_ 2 /\ 2 <_ ( # ` x ) ) ) )
35 32 33 34 mp2an 
 |-  ( ( # ` x ) = 2 <-> ( ( # ` x ) <_ 2 /\ 2 <_ ( # ` x ) ) )
36 35 bicomi 
 |-  ( ( ( # ` x ) <_ 2 /\ 2 <_ ( # ` x ) ) <-> ( # ` x ) = 2 )
37 36 rabbii 
 |-  { x e. ( ~P V \ { (/) } ) | ( ( # ` x ) <_ 2 /\ 2 <_ ( # ` x ) ) } = { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 }
38 27 28 37 3eqtri 
 |-  ( { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } i^i { x e. ~P V | 2 <_ ( # ` x ) } ) = { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 }