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

Metamath Proof Explorer

Theorem rnmptbdlem

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

Ref Expression
Hypotheses rnmptbdlem.x ⊢ Ⅎ 𝑥 𝜑
rnmptbdlem.y ⊢ Ⅎ 𝑦 𝜑
rnmptbdlem.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
Assertion rnmptbdlem ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 rnmptbdlem.x ⊢ Ⅎ 𝑥 𝜑
2 rnmptbdlem.y ⊢ Ⅎ 𝑦 𝜑
3 rnmptbdlem.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4 nfcv ⊢ Ⅎ 𝑥 ℝ
5 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦
6 4 5 nfrexw ⊢ Ⅎ 𝑥 ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦
7 1 6 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
8 simpr ⊢ ( ( 𝜑 ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
9 7 8 rnmptbdd ⊢ ( ( 𝜑 ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
10 9 ex ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )
11 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
12 11 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
13 nfv ⊢ Ⅎ 𝑥 𝑧 ≤ 𝑦
14 12 13 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦
15 1 14 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
16 breq1 ⊢ ( 𝑧 = 𝐵 → ( 𝑧 ≤ 𝑦 ↔ 𝐵 ≤ 𝑦 ) )
17 simplr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
18 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
19 simpr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
20 3 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
21 18 19 20 elrnmpt1d ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
22 16 17 21 rspcdva ⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝑦 )
23 15 22 ralrimia ⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
24 23 ex ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) )
25 24 a1d ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ) )
26 2 25 reximdai ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) )
27 10 26 impbid ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )