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

Proof

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