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

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

Proof

Step Hyp Ref Expression
1 rnmptlb.1 ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 )
2 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3 2 elrnmpt ⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
4 3 elv ⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
5 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵
6 nfv ⊢ Ⅎ 𝑥 𝑤 ≤ 𝑧
7 rspa ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑤 ≤ 𝐵 )
8 7 3adant3 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝑤 ≤ 𝐵 )
9 simp3 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝑧 = 𝐵 )
10 8 9 breqtrrd ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝑤 ≤ 𝑧 )
11 10 3exp ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ≤ 𝑧 ) ) )
12 5 6 11 rexlimd ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ≤ 𝑧 ) )
13 12 imp ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → 𝑤 ≤ 𝑧 )
14 13 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → 𝑤 ≤ 𝑧 )
15 4 14 sylan2b ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 ) ∧ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑤 ≤ 𝑧 )
16 15 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 ) → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑧 )
17 breq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ≤ 𝐵 ↔ 𝑤 ≤ 𝐵 ) )
18 17 ralbidv ⊢ ( 𝑦 = 𝑤 → ( ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 ) )
19 18 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 )
20 1 19 sylib ⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑤 ≤ 𝐵 )
21 16 20 reximddv3 ⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑧 )
22 breq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ≤ 𝑧 ↔ 𝑦 ≤ 𝑧 ) )
23 22 ralbidv ⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑧 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 ) )
24 23 cbvrexvw ⊢ ( ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑧 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 )
25 21 24 sylib ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 )