Theorem supxrleubrnmptf

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, 2-Jan-2022)

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

Proof

Step	Hyp	Ref	Expression
1		supxrleubrnmptf.x	⊢ Ⅎ 𝑥 𝜑
2		supxrleubrnmptf.a	⊢ Ⅎ 𝑥 𝐴
3		supxrleubrnmptf.n	⊢ Ⅎ 𝑥 𝐶
4		supxrleubrnmptf.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
5		supxrleubrnmptf.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
6		nfcv	⊢ Ⅎ 𝑦 𝐴
7		nfcv	⊢ Ⅎ 𝑦 𝐵
8		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
9		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
10	2 6 7 8 9	cbvmptf	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
11	10	rneqi	⊢ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ran ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
12	11	supeq1i	⊢ sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) = sup ( ran ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) , ℝ* , < )
13	12	breq1i	⊢ ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ≤ 𝐶 ↔ sup ( ran ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) , ℝ* , < ) ≤ 𝐶 )
14	13	a1i	⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ≤ 𝐶 ↔ sup ( ran ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) , ℝ* , < ) ≤ 𝐶 ) )
15		nfv	⊢ Ⅎ 𝑦 𝜑
16	2	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
17	1 16	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ 𝐴 )
18	8	nfel1	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ*
19	17 18	nfim	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ* )
20		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
21	20	anbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ) )
22	9	eleq1d	⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∈ ℝ* ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ* ) )
23	21 22	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ* ) ) )
24	19 23 4	chvarfv	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ* )
25	15 24 5	supxrleubrnmpt	⊢ ( 𝜑 → ( sup ( ran ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) , ℝ* , < ) ≤ 𝐶 ↔ ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ 𝐶 ) )
26		nfcv	⊢ Ⅎ 𝑥 ≤
27	8 26 3	nfbr	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ 𝐶
28		nfv	⊢ Ⅎ 𝑦 𝐵 ≤ 𝐶
29		eqcom	⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 )
30	29	imbi1i	⊢ ( ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑦 = 𝑥 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
31		eqcom	⊢ ( 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 )
32	31	imbi2i	⊢ ( ( 𝑦 = 𝑥 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 ) )
33	30 32	bitri	⊢ ( ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 ) )
34	9 33	mpbi	⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 )
35	34	breq1d	⊢ ( 𝑦 = 𝑥 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ 𝐶 ↔ 𝐵 ≤ 𝐶 ) )
36	6 2 27 28 35	cbvralfw	⊢ ( ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 )
37	36	a1i	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )
38	14 25 37	3bitrd	⊢ ( 𝜑 → ( sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )