Theorem rnmptbd2

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

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

Proof

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