Theorem rnmptbdd

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

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

Proof

Step	Hyp	Ref	Expression
1		rnmptbdd.x	⊢ Ⅎ 𝑥 𝜑
2		rnmptbdd.b	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
3		breq2	⊢ ( 𝑦 = 𝑣 → ( 𝐵 ≤ 𝑦 ↔ 𝐵 ≤ 𝑣 ) )
4	3	ralbidv	⊢ ( 𝑦 = 𝑣 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑣 ) )
5	4	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃ 𝑣 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑣 )
6	2 5	sylib	⊢ ( 𝜑 → ∃ 𝑣 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑣 )
7	1 6	rnmptbddlem	⊢ ( 𝜑 → ∃ 𝑣 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑣 )
8		breq2	⊢ ( 𝑣 = 𝑦 → ( 𝑤 ≤ 𝑣 ↔ 𝑤 ≤ 𝑦 ) )
9	8	ralbidv	⊢ ( 𝑣 = 𝑦 → ( ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑣 ↔ ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑦 ) )
10		breq1	⊢ ( 𝑤 = 𝑧 → ( 𝑤 ≤ 𝑦 ↔ 𝑧 ≤ 𝑦 ) )
11	10	cbvralvw	⊢ ( ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑦 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
12	9 11	bitrdi	⊢ ( 𝑣 = 𝑦 → ( ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑣 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )
13	12	cbvrexvw	⊢ ( ∃ 𝑣 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑣 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
14	7 13	sylib	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )