Theorem incsmflem

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

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

Proof

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