Metamath Proof Explorer


Theorem umgrislfupgrlem

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

Ref Expression
Assertion umgrislfupgrlem x 𝒫 V | x 2 x 𝒫 V | 2 x = x 𝒫 V | x = 2

Proof

Step Hyp Ref Expression
1 2pos 0 < 2
2 simprl 0 < 2 x 𝒫 V 2 x x 𝒫 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
8 0re 0
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 𝒫 V 2 x 0 < 2 x
14 13 impcomd x = 0 < 2 x 𝒫 V 2 x x
15 ax-1 x 0 < 2 x 𝒫 V 2 x x
16 14 15 pm2.61ine 0 < 2 x 𝒫 V 2 x x
17 eldifsn x 𝒫 V x 𝒫 V x
18 2 16 17 sylanbrc 0 < 2 x 𝒫 V 2 x x 𝒫 V
19 simprr 0 < 2 x 𝒫 V 2 x 2 x
20 18 19 jca 0 < 2 x 𝒫 V 2 x x 𝒫 V 2 x
21 20 ex 0 < 2 x 𝒫 V 2 x x 𝒫 V 2 x
22 eldifi x 𝒫 V x 𝒫 V
23 22 anim1i x 𝒫 V 2 x x 𝒫 V 2 x
24 21 23 impbid1 0 < 2 x 𝒫 V 2 x x 𝒫 V 2 x
25 24 rabbidva2 0 < 2 x 𝒫 V | 2 x = x 𝒫 V | 2 x
26 1 25 ax-mp x 𝒫 V | 2 x = x 𝒫 V | 2 x
27 26 ineq2i x 𝒫 V | x 2 x 𝒫 V | 2 x = x 𝒫 V | x 2 x 𝒫 V | 2 x
28 inrab x 𝒫 V | x 2 x 𝒫 V | 2 x = x 𝒫 V | x 2 2 x
29 hashxnn0 x V x 0 *
30 29 elv x 0 *
31 xnn0xr x 0 * x *
32 30 31 ax-mp x *
33 7 rexri 2 *
34 xrletri3 x * 2 * 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 𝒫 V | x 2 2 x = x 𝒫 V | x = 2
38 27 28 37 3eqtri x 𝒫 V | x 2 x 𝒫 V | 2 x = x 𝒫 V | x = 2