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 ∈ A y ≤ B
Assertion rnmptlb ⊢ φ → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B y ≤ z

Proof

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