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

Proof

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