Theorem decsmf

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

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

Proof

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