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 biimtrdi ⊢ 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