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