Theorem rnmptbddlem

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

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

Proof

Step	Hyp	Ref	Expression
1		rnmptbddlem.x	⊢ Ⅎ 𝑥 𝜑
2		rnmptbddlem.b	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
3		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4	3	elrnmpt	⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
5	4	elv	⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
6		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ ℝ
7	1 6	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ ℝ )
8		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦
9	7 8	nfan	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
10		nfv	⊢ Ⅎ 𝑥 𝑧 ≤ 𝑦
11		simp3	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝑧 = 𝐵 )
12		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝑦 )
13	12	3adant3	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝐵 ≤ 𝑦 )
14	11 13	eqbrtrd	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵 ) → 𝑧 ≤ 𝑦 )
15	14	3exp	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑧 ≤ 𝑦 ) ) )
16	15	adantl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑧 ≤ 𝑦 ) ) )
17	9 10 16	rexlimd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ≤ 𝑦 ) )
18	17	imp	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → 𝑧 ≤ 𝑦 )
19	5 18	sylan2b	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) ∧ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑧 ≤ 𝑦 )
20	19	ralrimiva	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
21	20 2	reximddv3	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )