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 ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 )