Theorem incsmf

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

	Ref	Expression
Hypotheses	incsmf.a	$$⊢\phi \to A\subseteq ℝ$$
	incsmf.f	$$⊢\phi \to F:A⟶ℝ$$
	incsmf.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)$$
	incsmf.j	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
	incsmf.b	$$⊢B=\mathrm{SalGen}\left(J\right)$$
Assertion	incsmf	$$⊢\phi \to F\in \mathrm{SMblFn}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		incsmf.a	$$⊢\phi \to A\subseteq ℝ$$
2		incsmf.f	$$⊢\phi \to F:A⟶ℝ$$
3		incsmf.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)$$
4		incsmf.j	$$⊢J=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
5		incsmf.b	$$⊢B=\mathrm{SalGen}\left(J\right)$$
6		nfv	$$⊢Ⅎa\phi$$
7		retop	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
8	4 7	eqeltri	$$⊢J\in \mathrm{Top}$$
9	8	a1i	$$⊢\phi \to J\in \mathrm{Top}$$
10	9 5	salgencld	$$⊢\phi \to B\in \mathrm{SAlg}$$
11	9 5	unisalgen2	$$⊢\phi \to \bigcup B=\bigcup J$$
12	4	unieqi	$$⊢\bigcup J=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
13	12	a1i	$$⊢\phi \to \bigcup J=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
14		uniretop	$$⊢ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
15	14	eqcomi	$$⊢\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=ℝ$$
16	15	a1i	$$⊢\phi \to \bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=ℝ$$
17	11 13 16	3eqtrrd	$$⊢\phi \to ℝ=\bigcup B$$
18	1 17	sseqtrd	$$⊢\phi \to A\subseteq \bigcup B$$
19		nfv	$$⊢Ⅎw\left(\phi \wedge a\in ℝ\right)$$
20		nfv	$$⊢Ⅎz\left(\phi \wedge a\in ℝ\right)$$
21	1	adantr	$$⊢\left(\phi \wedge a\in ℝ\right)\to A\subseteq ℝ$$
22	2	frexr	$$⊢\phi \to F:A⟶{ℝ}^{*}$$
23	22	adantr	$$⊢\left(\phi \wedge a\in ℝ\right)\to F:A⟶{ℝ}^{*}$$
24		breq1	$$⊢x=w\to \left(x\le y\leftrightarrow w\le y\right)$$
25		fveq2	$$⊢x=w\to F\left(x\right)=F\left(w\right)$$
26	25	breq1d	$$⊢x=w\to \left(F\left(x\right)\le F\left(y\right)\leftrightarrow F\left(w\right)\le F\left(y\right)\right)$$
27	24 26	imbi12d	$$⊢x=w\to \left(\left(x\le y\to F\left(x\right)\le F\left(y\right)\right)\leftrightarrow \left(w\le y\to F\left(w\right)\le F\left(y\right)\right)\right)$$
28		breq2	$$⊢y=z\to \left(w\le y\leftrightarrow w\le z\right)$$
29		fveq2	$$⊢y=z\to F\left(y\right)=F\left(z\right)$$
30	29	breq2d	$$⊢y=z\to \left(F\left(w\right)\le F\left(y\right)\leftrightarrow F\left(w\right)\le F\left(z\right)\right)$$
31	28 30	imbi12d	$$⊢y=z\to \left(\left(w\le y\to F\left(w\right)\le F\left(y\right)\right)\leftrightarrow \left(w\le z\to F\left(w\right)\le F\left(z\right)\right)\right)$$
32	27 31	cbvral2vw	$$⊢\forall x\in A\forall y\in A\left(x\le y\to F\left(x\right)\le F\left(y\right)\right)\leftrightarrow \forall w\in A\forall z\in A\left(w\le z\to F\left(w\right)\le F\left(z\right)\right)$$
33	3 32	sylib	$$⊢\phi \to \forall w\in A\forall z\in A\left(w\le z\to F\left(w\right)\le F\left(z\right)\right)$$
34	33	adantr	$$⊢\left(\phi \wedge a\in ℝ\right)\to \forall w\in A\forall z\in A\left(w\le z\to F\left(w\right)\le F\left(z\right)\right)$$
35		rexr	$$⊢a\in ℝ\to a\in {ℝ}^{*}$$
36	35	adantl	$$⊢\left(\phi \wedge a\in ℝ\right)\to a\in {ℝ}^{*}$$
37	25	breq1d	$$⊢x=w\to \left(F\left(x\right)<a\leftrightarrow F\left(w\right)<a\right)$$
38	37	cbvrabv	$$⊢\left\{x\in A|F\left(x\right)<a\right\}=\left\{w\in A|F\left(w\right)<a\right\}$$
39		eqid	$$⊢sup\left(\left\{x\in A|F\left(x\right)<a\right\},{ℝ}^{*},<\right)=sup\left(\left\{x\in A|F\left(x\right)<a\right\},{ℝ}^{*},<\right)$$
40		eqid	$$⊢\left(\mathrm{-\infty },sup\left(\left\{x\in A|F\left(x\right)<a\right\},{ℝ}^{*},<\right)\right)=\left(\mathrm{-\infty },sup\left(\left\{x\in A|F\left(x\right)<a\right\},{ℝ}^{*},<\right)\right)$$
41		eqid	$$⊢\left(\mathrm{-\infty },sup\left(\left\{x\in A|F\left(x\right)<a\right\},{ℝ}^{*},<\right)\right]=\left(\mathrm{-\infty },sup\left(\left\{x\in A|F\left(x\right)<a\right\},{ℝ}^{*},<\right)\right]$$
42	19 20 21 23 34 4 5 36 38 39 40 41	incsmflem	$$⊢\left(\phi \wedge a\in ℝ\right)\to \exists b\in B\left\{x\in A|F\left(x\right)<a\right\}=b\cap A$$
43		reex	$$⊢ℝ\in \mathrm{V}$$
44	43	a1i	$$⊢\phi \to ℝ\in \mathrm{V}$$
45	44 1	ssexd	$$⊢\phi \to A\in \mathrm{V}$$
46		elrest	$$⊢\left(B\in \mathrm{SAlg}\wedge A\in \mathrm{V}\right)\to \left(\left\{x\in A|F\left(x\right)<a\right\}\in \left(B{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists b\in B\left\{x\in A|F\left(x\right)<a\right\}=b\cap A\right)$$
47	10 45 46	syl2anc	$$⊢\phi \to \left(\left\{x\in A|F\left(x\right)<a\right\}\in \left(B{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists b\in B\left\{x\in A|F\left(x\right)<a\right\}=b\cap A\right)$$
48	47	adantr	$$⊢\left(\phi \wedge a\in ℝ\right)\to \left(\left\{x\in A|F\left(x\right)<a\right\}\in \left(B{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists b\in B\left\{x\in A|F\left(x\right)<a\right\}=b\cap A\right)$$
49	42 48	mpbird	$$⊢\left(\phi \wedge a\in ℝ\right)\to \left\{x\in A|F\left(x\right)<a\right\}\in \left(B{\upharpoonright }_{𝑡}A\right)$$
50	6 10 18 2 49	issmfd	$$⊢\phi \to F\in \mathrm{SMblFn}\left(B\right)$$