Theorem 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	⊢ Ⅎ 𝑥 𝜑
	decsmflem.y	⊢ Ⅎ 𝑦 𝜑
	decsmflem.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	decsmflem.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
	decsmflem.i	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
	decsmflem.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
	decsmflem.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
	decsmflem.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
	decsmflem.l	⊢ 𝑌 = { 𝑥 ∈ 𝐴 ∣ 𝑅 < ( 𝐹 ‘ 𝑥 ) }
	decsmflem.c	⊢ 𝐶 = sup ( 𝑌 , ℝ* , < )
	decsmflem.d	⊢ 𝐷 = ( -∞ (,) 𝐶 )
	decsmflem.e	⊢ 𝐸 = ( -∞ (,] 𝐶 )
Assertion	decsmflem	⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝐵 𝑌 = ( 𝑏 ∩ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		decsmflem.x	⊢ Ⅎ 𝑥 𝜑
2		decsmflem.y	⊢ Ⅎ 𝑦 𝜑
3		decsmflem.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4		decsmflem.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
5		decsmflem.i	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
6		decsmflem.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
7		decsmflem.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
8		decsmflem.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
9		decsmflem.l	⊢ 𝑌 = { 𝑥 ∈ 𝐴 ∣ 𝑅 < ( 𝐹 ‘ 𝑥 ) }
10		decsmflem.c	⊢ 𝐶 = sup ( 𝑌 , ℝ* , < )
11		decsmflem.d	⊢ 𝐷 = ( -∞ (,) 𝐶 )
12		decsmflem.e	⊢ 𝐸 = ( -∞ (,] 𝐶 )
13		mnfxr	⊢ -∞ ∈ ℝ*
14	13	a1i	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑌 ) → -∞ ∈ ℝ* )
15		ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ 𝑅 < ( 𝐹 ‘ 𝑥 ) } ⊆ 𝐴
16	9 15	eqsstri	⊢ 𝑌 ⊆ 𝐴
17	16	a1i	⊢ ( 𝜑 → 𝑌 ⊆ 𝐴 )
18	17 3	sstrd	⊢ ( 𝜑 → 𝑌 ⊆ ℝ )
19	18	sselda	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑌 ) → 𝐶 ∈ ℝ )
20	14 19 6 7	iocborel	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑌 ) → ( -∞ (,] 𝐶 ) ∈ 𝐵 )
21	12 20	eqeltrid	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑌 ) → 𝐸 ∈ 𝐵 )
22		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝑅 < ( 𝐹 ‘ 𝑥 ) }
23	9 22	nfcxfr	⊢ Ⅎ 𝑥 𝑌
24		nfcv	⊢ Ⅎ 𝑥 ℝ*
25		nfcv	⊢ Ⅎ 𝑥 <
26	23 24 25	nfsup	⊢ Ⅎ 𝑥 sup ( 𝑌 , ℝ* , < )
27	10 26	nfcxfr	⊢ Ⅎ 𝑥 𝐶
28	27 23	nfel	⊢ Ⅎ 𝑥 𝐶 ∈ 𝑌
29	1 28	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝐶 ∈ 𝑌 )
30	3	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑌 ) → 𝐴 ⊆ ℝ )
31	4	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑌 ) → 𝐹 : 𝐴 ⟶ ℝ* )
32	5	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑌 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
33	8	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑌 ) → 𝑅 ∈ ℝ* )
34		simpr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑌 ) → 𝐶 ∈ 𝑌 )
35	29 30 31 32 33 9 10 34 12	pimdecfgtioc	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑌 ) → 𝑌 = ( 𝐸 ∩ 𝐴 ) )
36		ineq1	⊢ ( 𝑏 = 𝐸 → ( 𝑏 ∩ 𝐴 ) = ( 𝐸 ∩ 𝐴 ) )
37	36	rspceeqv	⊢ ( ( 𝐸 ∈ 𝐵 ∧ 𝑌 = ( 𝐸 ∩ 𝐴 ) ) → ∃ 𝑏 ∈ 𝐵 𝑌 = ( 𝑏 ∩ 𝐴 ) )
38	21 35 37	syl2anc	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝑌 ) → ∃ 𝑏 ∈ 𝐵 𝑌 = ( 𝑏 ∩ 𝐴 ) )
39	6 7	iooborel	⊢ ( -∞ (,) 𝐶 ) ∈ 𝐵
40	11 39	eqeltri	⊢ 𝐷 ∈ 𝐵
41	40	a1i	⊢ ( 𝜑 → 𝐷 ∈ 𝐵 )
42	41	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝑌 ) → 𝐷 ∈ 𝐵 )
43	28	nfn	⊢ Ⅎ 𝑥 ¬ 𝐶 ∈ 𝑌
44	1 43	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ¬ 𝐶 ∈ 𝑌 )
45		nfv	⊢ Ⅎ 𝑦 ¬ 𝐶 ∈ 𝑌
46	2 45	nfan	⊢ Ⅎ 𝑦 ( 𝜑 ∧ ¬ 𝐶 ∈ 𝑌 )
47	3	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝑌 ) → 𝐴 ⊆ ℝ )
48	4	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝑌 ) → 𝐹 : 𝐴 ⟶ ℝ* )
49	5	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝑌 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
50	8	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝑌 ) → 𝑅 ∈ ℝ* )
51		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝑌 ) → ¬ 𝐶 ∈ 𝑌 )
52	44 46 47 48 49 50 9 10 51 11	pimdecfgtioo	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝑌 ) → 𝑌 = ( 𝐷 ∩ 𝐴 ) )
53		ineq1	⊢ ( 𝑏 = 𝐷 → ( 𝑏 ∩ 𝐴 ) = ( 𝐷 ∩ 𝐴 ) )
54	53	rspceeqv	⊢ ( ( 𝐷 ∈ 𝐵 ∧ 𝑌 = ( 𝐷 ∩ 𝐴 ) ) → ∃ 𝑏 ∈ 𝐵 𝑌 = ( 𝑏 ∩ 𝐴 ) )
55	42 52 54	syl2anc	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ 𝑌 ) → ∃ 𝑏 ∈ 𝐵 𝑌 = ( 𝑏 ∩ 𝐴 ) )
56	38 55	pm2.61dan	⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝐵 𝑌 = ( 𝑏 ∩ 𝐴 ) )