Metamath Proof Explorer

Theorem rnmptlb

Description: Boundness below of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypothesis rnmptlb.1 ⊢φ→∃y∈ℝ∀x∈Ay≤B
Assertion rnmptlb ⊢φ→∃y∈ℝ∀z∈ran⁡x∈A⟼By≤z

Proof

Step Hyp Ref Expression
1 rnmptlb.1 ⊢φ→∃y∈ℝ∀x∈Ay≤B
2 eqid ⊢x∈A⟼B=x∈A⟼B
3 2 elrnmpt ⊢z∈V→z∈ran⁡x∈A⟼B↔∃x∈Az=B
4 3 elv ⊢z∈ran⁡x∈A⟼B↔∃x∈Az=B
5 nfra1 ⊢Ⅎx∀x∈Aw≤B
6 nfv ⊢Ⅎxw≤z
7 rspa ⊢∀x∈Aw≤B∧x∈A→w≤B
8 7 3adant3 ⊢∀x∈Aw≤B∧x∈A∧z=B→w≤B
9 simp3 ⊢∀x∈Aw≤B∧x∈A∧z=B→z=B
10 8 9 breqtrrd ⊢∀x∈Aw≤B∧x∈A∧z=B→w≤z
11 10 3exp ⊢∀x∈Aw≤B→x∈A→z=B→w≤z
12 5 6 11 rexlimd ⊢∀x∈Aw≤B→∃x∈Az=B→w≤z
13 12 imp ⊢∀x∈Aw≤B∧∃x∈Az=B→w≤z
14 13 adantll ⊢φ∧w∈ℝ∧∀x∈Aw≤B∧∃x∈Az=B→w≤z
15 4 14 sylan2b ⊢φ∧w∈ℝ∧∀x∈Aw≤B∧z∈ran⁡x∈A⟼B→w≤z
16 15 ralrimiva ⊢φ∧w∈ℝ∧∀x∈Aw≤B→∀z∈ran⁡x∈A⟼Bw≤z
17 breq1 ⊢y=w→y≤B↔w≤B
18 17 ralbidv ⊢y=w→∀x∈Ay≤B↔∀x∈Aw≤B
19 18 cbvrexvw ⊢∃y∈ℝ∀x∈Ay≤B↔∃w∈ℝ∀x∈Aw≤B
20 1 19 sylib ⊢φ→∃w∈ℝ∀x∈Aw≤B
21 16 20 reximddv3 ⊢φ→∃w∈ℝ∀z∈ran⁡x∈A⟼Bw≤z
22 breq1 ⊢w=y→w≤z↔y≤z
23 22 ralbidv ⊢w=y→∀z∈ran⁡x∈A⟼Bw≤z↔∀z∈ran⁡x∈A⟼By≤z
24 23 cbvrexvw ⊢∃w∈ℝ∀z∈ran⁡x∈A⟼Bw≤z↔∃y∈ℝ∀z∈ran⁡x∈A⟼By≤z
25 21 24 sylib ⊢φ→∃y∈ℝ∀z∈ran⁡x∈A⟼By≤z