Theorem supxrleubrnmpt

Description: The supremum of a nonempty bounded indexed set of extended reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	supxrleubrnmpt.x	⊢ Ⅎ 𝑥 𝜑
	supxrleubrnmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
	supxrleubrnmpt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
Assertion	supxrleubrnmpt	⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		supxrleubrnmpt.x	⊢ Ⅎ 𝑥 𝜑
2		supxrleubrnmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
3		supxrleubrnmpt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
4		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5	1 4 2	rnmptssd	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ* )
6		supxrleub	⊢ ( ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ≤ 𝐶 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) )
7	5 3 6	syl2anc	⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ≤ 𝐶 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) )
8		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
9	8	nfrn	⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
10		nfv	⊢ Ⅎ 𝑥 𝑧 ≤ 𝐶
11	9 10	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶
12	1 11	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
14	4	elrnmpt1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ* ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
15	13 2 14	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
16	15	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
17		simplr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 )
18		breq1	⊢ ( 𝑧 = 𝐵 → ( 𝑧 ≤ 𝐶 ↔ 𝐵 ≤ 𝐶 ) )
19	18	rspcva	⊢ ( ( 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) → 𝐵 ≤ 𝐶 )
20	16 17 19	syl2anc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
21	20	ex	⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) → ( 𝑥 ∈ 𝐴 → 𝐵 ≤ 𝐶 ) )
22	12 21	ralrimi	⊢ ( ( 𝜑 ∧ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 )
23	22	ex	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )
24		vex	⊢ 𝑧 ∈ V
25	4	elrnmpt	⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
26	24 25	ax-mp	⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
27	26	biimpi	⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
28	27	adantl	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ∧ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
29		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶
30		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
31	18	biimprcd	⊢ ( 𝐵 ≤ 𝐶 → ( 𝑧 = 𝐵 → 𝑧 ≤ 𝐶 ) )
32	30 31	syl	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑧 = 𝐵 → 𝑧 ≤ 𝐶 ) )
33	32	ex	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 → ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑧 ≤ 𝐶 ) ) )
34	29 10 33	rexlimd	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ≤ 𝐶 ) )
35	34	adantr	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ∧ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ≤ 𝐶 ) )
36	28 35	mpd	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ∧ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑧 ≤ 𝐶 )
37	36	ralrimiva	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 )
38	37	a1i	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ) )
39	23 38	impbid	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )
40	7 39	bitrd	⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )