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	\|- F/ x ph
	incsmflem.y	\|- F/ y ph
	incsmflem.a	\|- ( ph -> A C_ RR )
	incsmflem.f	\|- ( ph -> F : A --> RR* )
	incsmflem.i	\|- ( ph -> A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )
	incsmflem.j	\|- J = ( topGen ` ran (,) )
	incsmflem.b	\|- B = ( SalGen ` J )
	incsmflem.r	\|- ( ph -> R e. RR* )
	incsmflem.l	\|- Y = { x e. A \| ( F ` x ) < R }
	incsmflem.c	\|- C = sup ( Y , RR* , < )
	incsmflem.d	\|- D = ( -oo (,) C )
	incsmflem.e	\|- E = ( -oo (,] C )
Assertion	incsmflem	\|- ( ph -> E. b e. B Y = ( b i^i A ) )

Proof

Step	Hyp	Ref	Expression
1		incsmflem.x	\|- F/ x ph
2		incsmflem.y	\|- F/ y ph
3		incsmflem.a	\|- ( ph -> A C_ RR )
4		incsmflem.f	\|- ( ph -> F : A --> RR* )
5		incsmflem.i	\|- ( ph -> A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )
6		incsmflem.j	\|- J = ( topGen ` ran (,) )
7		incsmflem.b	\|- B = ( SalGen ` J )
8		incsmflem.r	\|- ( ph -> R e. RR* )
9		incsmflem.l	\|- Y = { x e. A \| ( F ` x ) < R }
10		incsmflem.c	\|- C = sup ( Y , RR* , < )
11		incsmflem.d	\|- D = ( -oo (,) C )
12		incsmflem.e	\|- E = ( -oo (,] C )
13		mnfxr	\|- -oo e. RR*
14	13	a1i	\|- ( ( ph /\ C e. Y ) -> -oo e. RR* )
15		ssrab2	\|- { x e. A \| ( F ` x ) < R } C_ A
16	9 15	eqsstri	\|- Y C_ A
17	16	a1i	\|- ( ph -> Y C_ A )
18	17 3	sstrd	\|- ( ph -> Y C_ RR )
19	18	sselda	\|- ( ( ph /\ C e. Y ) -> C e. RR )
20	14 19 6 7	iocborel	\|- ( ( ph /\ C e. Y ) -> ( -oo (,] C ) e. B )
21	12 20	eqeltrid	\|- ( ( ph /\ C e. Y ) -> E e. B )
22		nfcv	\|- F/_ x C
23		nfrab1	\|- F/_ x { x e. A \| ( F ` x ) < R }
24	9 23	nfcxfr	\|- F/_ x Y
25	22 24	nfel	\|- F/ x C e. Y
26	1 25	nfan	\|- F/ x ( ph /\ C e. Y )
27		nfv	\|- F/ y C e. Y
28	2 27	nfan	\|- F/ y ( ph /\ C e. Y )
29	3	adantr	\|- ( ( ph /\ C e. Y ) -> A C_ RR )
30	4	adantr	\|- ( ( ph /\ C e. Y ) -> F : A --> RR* )
31	5	adantr	\|- ( ( ph /\ C e. Y ) -> A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )
32	8	adantr	\|- ( ( ph /\ C e. Y ) -> R e. RR* )
33		simpr	\|- ( ( ph /\ C e. Y ) -> C e. Y )
34	26 28 29 30 31 32 9 10 33 12	pimincfltioc	\|- ( ( ph /\ C e. Y ) -> Y = ( E i^i A ) )
35		ineq1	\|- ( b = E -> ( b i^i A ) = ( E i^i A ) )
36	35	rspceeqv	\|- ( ( E e. B /\ Y = ( E i^i A ) ) -> E. b e. B Y = ( b i^i A ) )
37	21 34 36	syl2anc	\|- ( ( ph /\ C e. Y ) -> E. b e. B Y = ( b i^i A ) )
38	6 7	iooborel	\|- ( -oo (,) C ) e. B
39	11 38	eqeltri	\|- D e. B
40	39	a1i	\|- ( ph -> D e. B )
41	40	adantr	\|- ( ( ph /\ -. C e. Y ) -> D e. B )
42	25	nfn	\|- F/ x -. C e. Y
43	1 42	nfan	\|- F/ x ( ph /\ -. C e. Y )
44		nfv	\|- F/ y -. C e. Y
45	2 44	nfan	\|- F/ y ( ph /\ -. C e. Y )
46	3	adantr	\|- ( ( ph /\ -. C e. Y ) -> A C_ RR )
47	4	adantr	\|- ( ( ph /\ -. C e. Y ) -> F : A --> RR* )
48	5	adantr	\|- ( ( ph /\ -. C e. Y ) -> A. x e. A A. y e. A ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )
49	8	adantr	\|- ( ( ph /\ -. C e. Y ) -> R e. RR* )
50		simpr	\|- ( ( ph /\ -. C e. Y ) -> -. C e. Y )
51	43 45 46 47 48 49 9 10 50 11	pimincfltioo	\|- ( ( ph /\ -. C e. Y ) -> Y = ( D i^i A ) )
52		ineq1	\|- ( b = D -> ( b i^i A ) = ( D i^i A ) )
53	52	rspceeqv	\|- ( ( D e. B /\ Y = ( D i^i A ) ) -> E. b e. B Y = ( b i^i A ) )
54	41 51 53	syl2anc	\|- ( ( ph /\ -. C e. Y ) -> E. b e. B Y = ( b i^i A ) )
55	37 54	pm2.61dan	\|- ( ph -> E. b e. B Y = ( b i^i A ) )

Metamath Proof Explorer

Theorem incsmflem

Proof