Theorem pimdecfgtioc

Description: Given a nonincreasing function, the preimage of an unbounded above, open interval, when the supremum of the preimage belongs to the preimage. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	pimdecfgtioc.x	$$⊢Ⅎx\phi$$
	pimdecfgtioc.a	$$⊢\phi \to A\subseteq ℝ$$
	pimdecfgtioc.f	$$⊢\phi \to F:A⟶{ℝ}^{*}$$
	pimdecfgtioc.i	$$⊢\phi \to \forall x\in A\forall y\in A\left(x\le y\to F\left(y\right)\le F\left(x\right)\right)$$
	pimdecfgtioc.r	$$⊢\phi \to R\in {ℝ}^{*}$$
	pimdecfgtioc.y	$$⊢Y=\left\{x\in A|R<F\left(x\right)\right\}$$
	pimdecfgtioc.c	$$⊢S=sup\left(Y,{ℝ}^{*},<\right)$$
	pimdecfgtioc.e	$$⊢\phi \to S\in Y$$
	pimdecfgtioc.d	$$⊢I=\left(\mathrm{-\infty },S\right]$$
Assertion	pimdecfgtioc	$$⊢\phi \to Y=I\cap A$$

Proof

Step	Hyp	Ref	Expression
1		pimdecfgtioc.x	$$⊢Ⅎx\phi$$
2		pimdecfgtioc.a	$$⊢\phi \to A\subseteq ℝ$$
3		pimdecfgtioc.f	$$⊢\phi \to F:A⟶{ℝ}^{*}$$
4		pimdecfgtioc.i	$$⊢\phi \to \forall x\in A\forall y\in A\left(x\le y\to F\left(y\right)\le F\left(x\right)\right)$$
5		pimdecfgtioc.r	$$⊢\phi \to R\in {ℝ}^{*}$$
6		pimdecfgtioc.y	$$⊢Y=\left\{x\in A|R<F\left(x\right)\right\}$$
7		pimdecfgtioc.c	$$⊢S=sup\left(Y,{ℝ}^{*},<\right)$$
8		pimdecfgtioc.e	$$⊢\phi \to S\in Y$$
9		pimdecfgtioc.d	$$⊢I=\left(\mathrm{-\infty },S\right]$$
10		ssrab2	$$⊢\left\{x\in A|R<F\left(x\right)\right\}\subseteq A$$
11	6 10	eqsstri	$$⊢Y\subseteq A$$
12	11	a1i	$$⊢\phi \to Y\subseteq A$$
13	12 2	sstrd	$$⊢\phi \to Y\subseteq ℝ$$
14	13 7 8 9	ressiocsup	$$⊢\phi \to Y\subseteq I$$
15	14 12	ssind	$$⊢\phi \to Y\subseteq I\cap A$$
16		elinel2	$$⊢x\in \left(I\cap A\right)\to x\in A$$
17	16	adantl	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to x\in A$$
18	5	adantr	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to R\in {ℝ}^{*}$$
19	11 8	sselid	$$⊢\phi \to S\in A$$
20	3 19	ffvelrnd	$$⊢\phi \to F\left(S\right)\in {ℝ}^{*}$$
21	20	adantr	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to F\left(S\right)\in {ℝ}^{*}$$
22	3	adantr	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to F:A⟶{ℝ}^{*}$$
23	22 17	ffvelrnd	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to F\left(x\right)\in {ℝ}^{*}$$
24	8 6	eleqtrdi	$$⊢\phi \to S\in \left\{x\in A|R<F\left(x\right)\right\}$$
25		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in A|R<F\left(x\right)\right\}$$
26	6 25	nfcxfr	$$⊢\underset{\_}{Ⅎ}xY$$
27		nfcv	$$⊢\underset{\_}{Ⅎ}x{ℝ}^{*}$$
28		nfcv	$$⊢\underset{\_}{Ⅎ}x<$$
29	26 27 28	nfsup	$$⊢\underset{\_}{Ⅎ}xsup\left(Y,{ℝ}^{*},<\right)$$
30	7 29	nfcxfr	$$⊢\underset{\_}{Ⅎ}xS$$
31		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
32		nfcv	$$⊢\underset{\_}{Ⅎ}xR$$
33		nfcv	$$⊢\underset{\_}{Ⅎ}xF$$
34	33 30	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(S\right)$$
35	32 28 34	nfbr	$$⊢ℲxR<F\left(S\right)$$
36		fveq2	$$⊢x=S\to F\left(x\right)=F\left(S\right)$$
37	36	breq2d	$$⊢x=S\to \left(R<F\left(x\right)\leftrightarrow R<F\left(S\right)\right)$$
38	30 31 35 37	elrabf	$$⊢S\in \left\{x\in A|R<F\left(x\right)\right\}\leftrightarrow \left(S\in A\wedge R<F\left(S\right)\right)$$
39	24 38	sylib	$$⊢\phi \to \left(S\in A\wedge R<F\left(S\right)\right)$$
40	39	simprd	$$⊢\phi \to R<F\left(S\right)$$
41	40	adantr	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to R<F\left(S\right)$$
42	19	adantr	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to S\in A$$
43	4	r19.21bi	$$⊢\left(\phi \wedge x\in A\right)\to \forall y\in A\left(x\le y\to F\left(y\right)\le F\left(x\right)\right)$$
44	17 43	syldan	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to \forall y\in A\left(x\le y\to F\left(y\right)\le F\left(x\right)\right)$$
45	42 44	jca	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to \left(S\in A\wedge \forall y\in A\left(x\le y\to F\left(y\right)\le F\left(x\right)\right)\right)$$
46		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
47	46	a1i	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to \mathrm{-\infty }\in {ℝ}^{*}$$
48		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
49	13 8	sseldd	$$⊢\phi \to S\in ℝ$$
50	48 49	sselid	$$⊢\phi \to S\in {ℝ}^{*}$$
51	50	adantr	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to S\in {ℝ}^{*}$$
52		elinel1	$$⊢x\in \left(I\cap A\right)\to x\in I$$
53	52 9	eleqtrdi	$$⊢x\in \left(I\cap A\right)\to x\in \left(\mathrm{-\infty },S\right]$$
54	53	adantl	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to x\in \left(\mathrm{-\infty },S\right]$$
55		iocleub	$$⊢\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge S\in {ℝ}^{*}\wedge x\in \left(\mathrm{-\infty },S\right]\right)\to x\le S$$
56	47 51 54 55	syl3anc	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to x\le S$$
57		breq2	$$⊢y=S\to \left(x\le y\leftrightarrow x\le S\right)$$
58		fveq2	$$⊢y=S\to F\left(y\right)=F\left(S\right)$$
59	58	breq1d	$$⊢y=S\to \left(F\left(y\right)\le F\left(x\right)\leftrightarrow F\left(S\right)\le F\left(x\right)\right)$$
60	57 59	imbi12d	$$⊢y=S\to \left(\left(x\le y\to F\left(y\right)\le F\left(x\right)\right)\leftrightarrow \left(x\le S\to F\left(S\right)\le F\left(x\right)\right)\right)$$
61	60	rspcva	$$⊢\left(S\in A\wedge \forall y\in A\left(x\le y\to F\left(y\right)\le F\left(x\right)\right)\right)\to \left(x\le S\to F\left(S\right)\le F\left(x\right)\right)$$
62	45 56 61	sylc	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to F\left(S\right)\le F\left(x\right)$$
63	18 21 23 41 62	xrltletrd	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to R<F\left(x\right)$$
64	17 63	jca	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to \left(x\in A\wedge R<F\left(x\right)\right)$$
65	6	rabeq2i	$$⊢x\in Y\leftrightarrow \left(x\in A\wedge R<F\left(x\right)\right)$$
66	64 65	sylibr	$$⊢\left(\phi \wedge x\in \left(I\cap A\right)\right)\to x\in Y$$
67	66	ex	$$⊢\phi \to \left(x\in \left(I\cap A\right)\to x\in Y\right)$$
68	1 67	ralrimi	$$⊢\phi \to \forall x\in \left(I\cap A\right)x\in Y$$
69		nfv	$$⊢Ⅎxz\in \left(I\cap A\right)$$
70	69	nfci	$$⊢\underset{\_}{Ⅎ}x\left(I\cap A\right)$$
71	70 26	dfss3f	$$⊢I\cap A\subseteq Y\leftrightarrow \forall x\in \left(I\cap A\right)x\in Y$$
72	68 71	sylibr	$$⊢\phi \to I\cap A\subseteq Y$$
73	15 72	eqssd	$$⊢\phi \to Y=I\cap A$$