Metamath Proof Explorer

Theorem infxrunb3rnmpt

Description: The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses infxrunb3rnmpt.1 ⊢Ⅎxφ
infxrunb3rnmpt.2 ⊢Ⅎyφ
infxrunb3rnmpt.3 ⊢φ∧x∈A→B∈ℝ*
Assertion infxrunb3rnmpt ⊢φ→∀y∈ℝ∃x∈AB≤y↔supran⁡x∈A⟼Bℝ*<=−∞

Proof

Step Hyp Ref Expression
1 infxrunb3rnmpt.1 ⊢Ⅎxφ
2 infxrunb3rnmpt.2 ⊢Ⅎyφ
3 infxrunb3rnmpt.3 ⊢φ∧x∈A→B∈ℝ*
4 nfmpt1 ⊢Ⅎ_xx∈A⟼B
5 4 nfrn ⊢Ⅎ_xran⁡x∈A⟼B
6 nfv ⊢Ⅎxz≤y
7 5 6 nfrexw ⊢Ⅎx∃z∈ran⁡x∈A⟼Bz≤y
8 simpr ⊢φ∧x∈A→x∈A
9 eqid ⊢x∈A⟼B=x∈A⟼B
10 9 elrnmpt1 ⊢x∈A∧B∈ℝ*→B∈ran⁡x∈A⟼B
11 8 3 10 syl2anc ⊢φ∧x∈A→B∈ran⁡x∈A⟼B
12 11 3adant3 ⊢φ∧x∈A∧B≤y→B∈ran⁡x∈A⟼B
13 simp3 ⊢φ∧x∈A∧B≤y→B≤y
14 breq1 ⊢z=B→z≤y↔B≤y
15 14 rspcev ⊢B∈ran⁡x∈A⟼B∧B≤y→∃z∈ran⁡x∈A⟼Bz≤y
16 12 13 15 syl2anc ⊢φ∧x∈A∧B≤y→∃z∈ran⁡x∈A⟼Bz≤y
17 16 3exp ⊢φ→x∈A→B≤y→∃z∈ran⁡x∈A⟼Bz≤y
18 1 7 17 rexlimd ⊢φ→∃x∈AB≤y→∃z∈ran⁡x∈A⟼Bz≤y
19 nfv ⊢Ⅎz∃x∈AB≤y
20 vex ⊢z∈V
21 9 elrnmpt ⊢z∈V→z∈ran⁡x∈A⟼B↔∃x∈Az=B
22 20 21 ax-mp ⊢z∈ran⁡x∈A⟼B↔∃x∈Az=B
23 22 biimpi ⊢z∈ran⁡x∈A⟼B→∃x∈Az=B
24 14 biimpcd ⊢z≤y→z=B→B≤y
25 24 a1d ⊢z≤y→x∈A→z=B→B≤y
26 6 25 reximdai ⊢z≤y→∃x∈Az=B→∃x∈AB≤y
27 26 com12 ⊢∃x∈Az=B→z≤y→∃x∈AB≤y
28 23 27 syl ⊢z∈ran⁡x∈A⟼B→z≤y→∃x∈AB≤y
29 19 28 rexlimi ⊢∃z∈ran⁡x∈A⟼Bz≤y→∃x∈AB≤y
30 29 a1i ⊢φ→∃z∈ran⁡x∈A⟼Bz≤y→∃x∈AB≤y
31 18 30 impbid ⊢φ→∃x∈AB≤y↔∃z∈ran⁡x∈A⟼Bz≤y
32 2 31 ralbid ⊢φ→∀y∈ℝ∃x∈AB≤y↔∀y∈ℝ∃z∈ran⁡x∈A⟼Bz≤y
33 1 9 3 rnmptssd ⊢φ→ran⁡x∈A⟼B⊆ℝ*
34 infxrunb3 ⊢ran⁡x∈A⟼B⊆ℝ*→∀y∈ℝ∃z∈ran⁡x∈A⟼Bz≤y↔supran⁡x∈A⟼Bℝ*<=−∞
35 33 34 syl ⊢φ→∀y∈ℝ∃z∈ran⁡x∈A⟼Bz≤y↔supran⁡x∈A⟼Bℝ*<=−∞
36 32 35 bitrd ⊢φ→∀y∈ℝ∃x∈AB≤y↔supran⁡x∈A⟼Bℝ*<=−∞