Theorem decsmflem

Description: A nonincreasing function is Borel measurable. Proposition 121D (c) of Fremlin1 p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	decsmflem.x	$$⊢Ⅎx\phi$$
	decsmflem.y	$$⊢Ⅎy\phi$$
	decsmflem.a	$$⊢\phi \to A\subseteq ℝ$$
	decsmflem.f	$$⊢\phi \to F:A⟶{ℝ}^{*}$$
	decsmflem.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)$$
	decsmflem.j	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	decsmflem.b	$$⊢B=\mathrm{SalGen}\left(J\right)$$
	decsmflem.r	$$⊢\phi \to R\in {ℝ}^{*}$$
	decsmflem.l	$$⊢Y=\left\{x\in A|R<F\left(x\right)\right\}$$
	decsmflem.c	$$⊢C=sup\left(Y,{ℝ}^{*},<\right)$$
	decsmflem.d	$$⊢D=\left(\mathrm{-\infty },C\right)$$
	decsmflem.e	$$⊢E=\left(\mathrm{-\infty },C\right]$$
Assertion	decsmflem	$$⊢\phi \to \exists b\in BY=b\cap A$$

Proof

Step	Hyp	Ref	Expression
1		decsmflem.x	$$⊢Ⅎx\phi$$
2		decsmflem.y	$$⊢Ⅎy\phi$$
3		decsmflem.a	$$⊢\phi \to A\subseteq ℝ$$
4		decsmflem.f	$$⊢\phi \to F:A⟶{ℝ}^{*}$$
5		decsmflem.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)$$
6		decsmflem.j	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
7		decsmflem.b	$$⊢B=\mathrm{SalGen}\left(J\right)$$
8		decsmflem.r	$$⊢\phi \to R\in {ℝ}^{*}$$
9		decsmflem.l	$$⊢Y=\left\{x\in A|R<F\left(x\right)\right\}$$
10		decsmflem.c	$$⊢C=sup\left(Y,{ℝ}^{*},<\right)$$
11		decsmflem.d	$$⊢D=\left(\mathrm{-\infty },C\right)$$
12		decsmflem.e	$$⊢E=\left(\mathrm{-\infty },C\right]$$
13		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
14	13	a1i	$$⊢\left(\phi \wedge C\in Y\right)\to \mathrm{-\infty }\in {ℝ}^{*}$$
15		ssrab2	$$⊢\left\{x\in A|R<F\left(x\right)\right\}\subseteq A$$
16	9 15	eqsstri	$$⊢Y\subseteq A$$
17	16	a1i	$$⊢\phi \to Y\subseteq A$$
18	17 3	sstrd	$$⊢\phi \to Y\subseteq ℝ$$
19	18	sselda	$$⊢\left(\phi \wedge C\in Y\right)\to C\in ℝ$$
20	14 19 6 7	iocborel	$$⊢\left(\phi \wedge C\in Y\right)\to \left(\mathrm{-\infty },C\right]\in B$$
21	12 20	eqeltrid	$$⊢\left(\phi \wedge C\in Y\right)\to E\in B$$
22		nfrab1	$$⊢\underset{\_}{Ⅎ}x\left\{x\in A|R<F\left(x\right)\right\}$$
23	9 22	nfcxfr	$$⊢\underset{\_}{Ⅎ}xY$$
24		nfcv	$$⊢\underset{\_}{Ⅎ}x{ℝ}^{*}$$
25		nfcv	$$⊢\underset{\_}{Ⅎ}x<$$
26	23 24 25	nfsup	$$⊢\underset{\_}{Ⅎ}xsup\left(Y,{ℝ}^{*},<\right)$$
27	10 26	nfcxfr	$$⊢\underset{\_}{Ⅎ}xC$$
28	27 23	nfel	$$⊢ℲxC\in Y$$
29	1 28	nfan	$$⊢Ⅎx\left(\phi \wedge C\in Y\right)$$
30	3	adantr	$$⊢\left(\phi \wedge C\in Y\right)\to A\subseteq ℝ$$
31	4	adantr	$$⊢\left(\phi \wedge C\in Y\right)\to F:A⟶{ℝ}^{*}$$
32	5	adantr	$$⊢\left(\phi \wedge C\in Y\right)\to \forall x\in A\forall y\in A\left(x\le y\to F\left(y\right)\le F\left(x\right)\right)$$
33	8	adantr	$$⊢\left(\phi \wedge C\in Y\right)\to R\in {ℝ}^{*}$$
34		simpr	$$⊢\left(\phi \wedge C\in Y\right)\to C\in Y$$
35	29 30 31 32 33 9 10 34 12	pimdecfgtioc	$$⊢\left(\phi \wedge C\in Y\right)\to Y=E\cap A$$
36		ineq1	$$⊢b=E\to b\cap A=E\cap A$$
37	36	rspceeqv	$$⊢\left(E\in B\wedge Y=E\cap A\right)\to \exists b\in BY=b\cap A$$
38	21 35 37	syl2anc	$$⊢\left(\phi \wedge C\in Y\right)\to \exists b\in BY=b\cap A$$
39	6 7	iooborel	$$⊢\left(\mathrm{-\infty },C\right)\in B$$
40	11 39	eqeltri	$$⊢D\in B$$
41	40	a1i	$$⊢\phi \to D\in B$$
42	41	adantr	$$⊢\left(\phi \wedge \neg C\in Y\right)\to D\in B$$
43	28	nfn	$$⊢Ⅎx\neg C\in Y$$
44	1 43	nfan	$$⊢Ⅎx\left(\phi \wedge \neg C\in Y\right)$$
45		nfv	$$⊢Ⅎy\neg C\in Y$$
46	2 45	nfan	$$⊢Ⅎy\left(\phi \wedge \neg C\in Y\right)$$
47	3	adantr	$$⊢\left(\phi \wedge \neg C\in Y\right)\to A\subseteq ℝ$$
48	4	adantr	$$⊢\left(\phi \wedge \neg C\in Y\right)\to F:A⟶{ℝ}^{*}$$
49	5	adantr	$$⊢\left(\phi \wedge \neg C\in Y\right)\to \forall x\in A\forall y\in A\left(x\le y\to F\left(y\right)\le F\left(x\right)\right)$$
50	8	adantr	$$⊢\left(\phi \wedge \neg C\in Y\right)\to R\in {ℝ}^{*}$$
51		simpr	$$⊢\left(\phi \wedge \neg C\in Y\right)\to \neg C\in Y$$
52	44 46 47 48 49 50 9 10 51 11	pimdecfgtioo	$$⊢\left(\phi \wedge \neg C\in Y\right)\to Y=D\cap A$$
53		ineq1	$$⊢b=D\to b\cap A=D\cap A$$
54	53	rspceeqv	$$⊢\left(D\in B\wedge Y=D\cap A\right)\to \exists b\in BY=b\cap A$$
55	42 52 54	syl2anc	$$⊢\left(\phi \wedge \neg C\in Y\right)\to \exists b\in BY=b\cap A$$
56	38 55	pm2.61dan	$$⊢\phi \to \exists b\in BY=b\cap A$$