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

Proof

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

Metamath Proof Explorer

Theorem decsmflem

Proof