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	⊢ Ⅎ 𝑥 𝜑
	decsmf.y	⊢ Ⅎ 𝑦 𝜑
	decsmf.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	decsmf.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
	decsmf.i	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
	decsmf.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
	decsmf.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
Assertion	decsmf	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		decsmf.x	⊢ Ⅎ 𝑥 𝜑
2		decsmf.y	⊢ Ⅎ 𝑦 𝜑
3		decsmf.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4		decsmf.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
5		decsmf.i	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
6		decsmf.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
7		decsmf.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
8		nfv	⊢ Ⅎ 𝑎 𝜑
9		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
10	6 9	eqeltri	⊢ 𝐽 ∈ Top
11	10	a1i	⊢ ( 𝜑 → 𝐽 ∈ Top )
12	11 7	salgencld	⊢ ( 𝜑 → 𝐵 ∈ SAlg )
13	11 7	unisalgen2	⊢ ( 𝜑 → ∪ 𝐵 = ∪ 𝐽 )
14	6	unieqi	⊢ ∪ 𝐽 = ∪ ( topGen ‘ ran (,) )
15	14	a1i	⊢ ( 𝜑 → ∪ 𝐽 = ∪ ( topGen ‘ ran (,) ) )
16		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
17	16	eqcomi	⊢ ∪ ( topGen ‘ ran (,) ) = ℝ
18	17	a1i	⊢ ( 𝜑 → ∪ ( topGen ‘ ran (,) ) = ℝ )
19	13 15 18	3eqtrrd	⊢ ( 𝜑 → ℝ = ∪ 𝐵 )
20	3 19	sseqtrd	⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝐵 )
21		nfv	⊢ Ⅎ 𝑥 𝑎 ∈ ℝ
22	1 21	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑎 ∈ ℝ )
23		nfv	⊢ Ⅎ 𝑦 𝑎 ∈ ℝ
24	2 23	nfan	⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑎 ∈ ℝ )
25	3	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐴 ⊆ ℝ )
26	4	frexr	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐹 : 𝐴 ⟶ ℝ* )
28		breq1	⊢ ( 𝑥 = 𝑤 → ( 𝑥 ≤ 𝑦 ↔ 𝑤 ≤ 𝑦 ) )
29		fveq2	⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
30	29	breq2d	⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑤 ) ) )
31	28 30	imbi12d	⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑤 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑤 ) ) ) )
32		breq2	⊢ ( 𝑦 = 𝑧 → ( 𝑤 ≤ 𝑦 ↔ 𝑤 ≤ 𝑧 ) )
33		fveq2	⊢ ( 𝑦 = 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
34	33	breq1d	⊢ ( 𝑦 = 𝑧 → ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) ) )
35	32 34	imbi12d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑤 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑤 ) ) ↔ ( 𝑤 ≤ 𝑧 → ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) ) ) )
36	31 35	cbvral2vw	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) ) )
37	5 36	sylib	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) ) )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ∀ 𝑤 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) ) )
39	38 36	sylibr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
40		rexr	⊢ ( 𝑎 ∈ ℝ → 𝑎 ∈ ℝ* )
41	40	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ* )
42		eqid	⊢ { 𝑥 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } = { 𝑥 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) }
43		fveq2	⊢ ( 𝑤 = 𝑥 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑥 ) )
44	43	breq2d	⊢ ( 𝑤 = 𝑥 → ( 𝑎 < ( 𝐹 ‘ 𝑤 ) ↔ 𝑎 < ( 𝐹 ‘ 𝑥 ) ) )
45	44	cbvrabv	⊢ { 𝑤 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑤 ) } = { 𝑥 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) }
46	45	supeq1i	⊢ sup ( { 𝑤 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑤 ) } , ℝ* , < ) = sup ( { 𝑥 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } , ℝ* , < )
47		eqid	⊢ ( -∞ (,) sup ( { 𝑤 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑤 ) } , ℝ* , < ) ) = ( -∞ (,) sup ( { 𝑤 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑤 ) } , ℝ* , < ) )
48		eqid	⊢ ( -∞ (,] sup ( { 𝑤 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑤 ) } , ℝ* , < ) ) = ( -∞ (,] sup ( { 𝑤 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑤 ) } , ℝ* , < ) )
49	22 24 25 27 39 6 7 41 42 46 47 48	decsmflem	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ∃ 𝑏 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } = ( 𝑏 ∩ 𝐴 ) )
50	12	elexd	⊢ ( 𝜑 → 𝐵 ∈ V )
51		reex	⊢ ℝ ∈ V
52	51	a1i	⊢ ( 𝜑 → ℝ ∈ V )
53	52 3	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
54		elrest	⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( { 𝑥 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝐵 ↾t 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } = ( 𝑏 ∩ 𝐴 ) ) )
55	50 53 54	syl2anc	⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝐵 ↾t 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } = ( 𝑏 ∩ 𝐴 ) ) )
56	55	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( { 𝑥 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝐵 ↾t 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐵 { 𝑥 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } = ( 𝑏 ∩ 𝐴 ) ) )
57	49 56	mpbird	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐴 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝐵 ↾t 𝐴 ) )
58	8 12 20 4 57	issmfgtd	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝐵 ) )