Theorem rnmptbd

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

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

Proof

Step	Hyp	Ref	Expression
1		rnmptbd.x	⊢ Ⅎ 𝑥 𝜑
2		rnmptbd.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3		breq2	⊢ ( 𝑦 = 𝑤 → ( 𝐵 ≤ 𝑦 ↔ 𝐵 ≤ 𝑤 ) )
4	3	ralbidv	⊢ ( 𝑦 = 𝑤 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) )
5	4	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 )
6	5	a1i	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ) )
7		nfv	⊢ Ⅎ 𝑤 𝜑
8	1 7 2	rnmptbdlem	⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑤 ↔ ∃ 𝑤 ∈ ℝ ∀ 𝑢 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑢 ≤ 𝑤 ) )
9		breq2	⊢ ( 𝑤 = 𝑦 → ( 𝑢 ≤ 𝑤 ↔ 𝑢 ≤ 𝑦 ) )
10	9	ralbidv	⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑢 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑢 ≤ 𝑤 ↔ ∀ 𝑢 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑢 ≤ 𝑦 ) )
11		breq1	⊢ ( 𝑢 = 𝑧 → ( 𝑢 ≤ 𝑦 ↔ 𝑧 ≤ 𝑦 ) )
12	11	cbvralvw	⊢ ( ∀ 𝑢 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑢 ≤ 𝑦 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
13	10 12	bitrdi	⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑢 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑢 ≤ 𝑤 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )
14	13	cbvrexvw	⊢ ( ∃ 𝑤 ∈ ℝ ∀ 𝑢 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑢 ≤ 𝑤 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
15	14	a1i	⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑢 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑢 ≤ 𝑤 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )
16	6 8 15	3bitrd	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) )