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	$$⊢Ⅎx\phi$$
	supxrleubrnmptf.a	$$⊢\underset{\_}{Ⅎ}xA$$
	supxrleubrnmptf.n	$$⊢\underset{\_}{Ⅎ}xC$$
	supxrleubrnmptf.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
	supxrleubrnmptf.c	$$⊢\phi \to C\in {ℝ}^{*}$$
Assertion	supxrleubrnmptf	$$⊢\phi \to \left(sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)\le C\leftrightarrow \forall x\in AB\le C\right)$$

Proof

Step	Hyp	Ref	Expression
1		supxrleubrnmptf.x	$$⊢Ⅎx\phi$$
2		supxrleubrnmptf.a	$$⊢\underset{\_}{Ⅎ}xA$$
3		supxrleubrnmptf.n	$$⊢\underset{\_}{Ⅎ}xC$$
4		supxrleubrnmptf.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}$$
5		supxrleubrnmptf.c	$$⊢\phi \to C\in {ℝ}^{*}$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
8		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
9		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
10	2 6 7 8 9	cbvmptf	$$⊢\left(x\in A⟼B\right)=\left(y\in A⟼⦋y/x⦌B\right)$$
11	10	rneqi	$$⊢\mathrm{ran}\left(x\in A⟼B\right)=\mathrm{ran}\left(y\in A⟼⦋y/x⦌B\right)$$
12	11	supeq1i	$$⊢sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left(y\in A⟼⦋y/x⦌B\right),{ℝ}^{*},<\right)$$
13	12	breq1i	$$⊢sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)\le C\leftrightarrow sup\left(\mathrm{ran}\left(y\in A⟼⦋y/x⦌B\right),{ℝ}^{*},<\right)\le C$$
14	13	a1i	$$⊢\phi \to \left(sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)\le C\leftrightarrow sup\left(\mathrm{ran}\left(y\in A⟼⦋y/x⦌B\right),{ℝ}^{*},<\right)\le C\right)$$
15		nfv	$$⊢Ⅎy\phi$$
16	2	nfcri	$$⊢Ⅎxy\in A$$
17	1 16	nfan	$$⊢Ⅎx\left(\phi \wedge y\in A\right)$$
18	8	nfel1	$$⊢Ⅎx⦋y/x⦌B\in {ℝ}^{*}$$
19	17 18	nfim	$$⊢Ⅎx\left(\left(\phi \wedge y\in A\right)\to ⦋y/x⦌B\in {ℝ}^{*}\right)$$
20		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
21	20	anbi2d	$$⊢x=y\to \left(\left(\phi \wedge x\in A\right)\leftrightarrow \left(\phi \wedge y\in A\right)\right)$$
22	9	eleq1d	$$⊢x=y\to \left(B\in {ℝ}^{*}\leftrightarrow ⦋y/x⦌B\in {ℝ}^{*}\right)$$
23	21 22	imbi12d	$$⊢x=y\to \left(\left(\left(\phi \wedge x\in A\right)\to B\in {ℝ}^{*}\right)\leftrightarrow \left(\left(\phi \wedge y\in A\right)\to ⦋y/x⦌B\in {ℝ}^{*}\right)\right)$$
24	19 23 4	chvarfv	$$⊢\left(\phi \wedge y\in A\right)\to ⦋y/x⦌B\in {ℝ}^{*}$$
25	15 24 5	supxrleubrnmpt	$$⊢\phi \to \left(sup\left(\mathrm{ran}\left(y\in A⟼⦋y/x⦌B\right),{ℝ}^{*},<\right)\le C\leftrightarrow \forall y\in A⦋y/x⦌B\le C\right)$$
26		nfcv	$$⊢\underset{\_}{Ⅎ}x\le$$
27	8 26 3	nfbr	$$⊢Ⅎx⦋y/x⦌B\le C$$
28		nfv	$$⊢ℲyB\le C$$
29		eqcom	$$⊢x=y\leftrightarrow y=x$$
30	29	imbi1i	$$⊢\left(x=y\to B=⦋y/x⦌B\right)\leftrightarrow \left(y=x\to B=⦋y/x⦌B\right)$$
31		eqcom	$$⊢B=⦋y/x⦌B\leftrightarrow ⦋y/x⦌B=B$$
32	31	imbi2i	$$⊢\left(y=x\to B=⦋y/x⦌B\right)\leftrightarrow \left(y=x\to ⦋y/x⦌B=B\right)$$
33	30 32	bitri	$$⊢\left(x=y\to B=⦋y/x⦌B\right)\leftrightarrow \left(y=x\to ⦋y/x⦌B=B\right)$$
34	9 33	mpbi	$$⊢y=x\to ⦋y/x⦌B=B$$
35	34	breq1d	$$⊢y=x\to \left(⦋y/x⦌B\le C\leftrightarrow B\le C\right)$$
36	6 2 27 28 35	cbvralfw	$$⊢\forall y\in A⦋y/x⦌B\le C\leftrightarrow \forall x\in AB\le C$$
37	36	a1i	$$⊢\phi \to \left(\forall y\in A⦋y/x⦌B\le C\leftrightarrow \forall x\in AB\le C\right)$$
38	14 25 37	3bitrd	$$⊢\phi \to \left(sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)\le C\leftrightarrow \forall x\in AB\le C\right)$$