Metamath Proof Explorer

Theorem rnmptbddlem

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

Ref Expression
Hypotheses rnmptbddlem.x ⊢ Ⅎ x φ
rnmptbddlem.b ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
Assertion rnmptbddlem ⊢ φ → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y

Proof

Step Hyp Ref Expression
1 rnmptbddlem.x ⊢ Ⅎ x φ
2 rnmptbddlem.b ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
3 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
4 3 elrnmpt ⊢ z ∈ V → z ∈ ran ⁡ x ∈ A ⟼ B ↔ ∃ x ∈ A z = B
5 4 elv ⊢ z ∈ ran ⁡ x ∈ A ⟼ B ↔ ∃ x ∈ A z = B
6 nfv ⊢ Ⅎ x y ∈ ℝ
7 1 6 nfan ⊢ Ⅎ x φ ∧ y ∈ ℝ
8 nfra1 ⊢ Ⅎ x ∀ x ∈ A B ≤ y
9 7 8 nfan ⊢ Ⅎ x φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y
10 nfv ⊢ Ⅎ x z ≤ y
11 simp3 ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ z = B → z = B
12 rspa ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A → B ≤ y
13 12 3adant3 ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ z = B → B ≤ y
14 11 13 eqbrtrd ⊢ ∀ x ∈ A B ≤ y ∧ x ∈ A ∧ z = B → z ≤ y
15 14 3exp ⊢ ∀ x ∈ A B ≤ y → x ∈ A → z = B → z ≤ y
16 15 adantl ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y → x ∈ A → z = B → z ≤ y
17 9 10 16 rexlimd ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y → ∃ x ∈ A z = B → z ≤ y
18 17 imp ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y ∧ ∃ x ∈ A z = B → z ≤ y
19 5 18 sylan2b ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y ∧ z ∈ ran ⁡ x ∈ A ⟼ B → z ≤ y
20 19 ralrimiva ⊢ φ ∧ y ∈ ℝ ∧ ∀ x ∈ A B ≤ y → ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
21 20 2 reximddv3 ⊢ φ → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y