This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ Ⅎ 𝑥 𝜑
rnmptbddlem.b ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
Assertion rnmptbddlem ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )

Proof

Step Hyp Ref Expression
1 rnmptbddlem.x ⊢ Ⅎ 𝑥 𝜑
2 rnmptbddlem.b ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
3 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4 3 elrnmpt ⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
5 4 elv ⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
6 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ ℝ
7 1 6 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ ℝ )
8 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦
9 7 8 nfan ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
10 nfv ⊢ Ⅎ 𝑥 𝑧 ≤ 𝑦
11 simp3 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝑧 = 𝐵 )
12 rspa ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝑦 )
13 12 3adant3 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝐵 ≤ 𝑦 )
14 11 13 eqbrtrd ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝑧 ≤ 𝑦 )
15 14 3exp ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑧 ≤ 𝑦 ) ) )
16 15 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑧 ≤ 𝑦 ) ) )
17 9 10 16 rexlimd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ≤ 𝑦 ) )
18 17 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → 𝑧 ≤ 𝑦 )
19 5 18 sylan2b ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑧 ≤ 𝑦 )
20 19 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
21 20 2 reximddv3 ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )