suprleubrnmpt

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

	Ref	Expression
Hypotheses	suprleubrnmpt.x	⊢ Ⅎ 𝑥 𝜑
	suprleubrnmpt.a	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	suprleubrnmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	suprleubrnmpt.e	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
	suprleubrnmpt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
Assertion	suprleubrnmpt	⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )

Proof

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

Metamath Proof Explorer

Theorem suprleubrnmpt

Proof