Theorem cnfsmf

Description: A continuous function is measurable. Proposition 121D (b) of Fremlin1 p. 36 is a special case of this theorem, where the topology on the domain is induced by the standard topology on n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	cnfsmf.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
	cnfsmf.k	⊢ 𝐾 = ( topGen ‘ ran (,) )
	cnfsmf.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ↾t dom 𝐹 ) Cn 𝐾 ) )
	cnfsmf.s	⊢ 𝑆 = ( SalGen ‘ 𝐽 )
Assertion	cnfsmf	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		cnfsmf.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		cnfsmf.k	⊢ 𝐾 = ( topGen ‘ ran (,) )
3		cnfsmf.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ↾t dom 𝐹 ) Cn 𝐾 ) )
4		cnfsmf.s	⊢ 𝑆 = ( SalGen ‘ 𝐽 )
5		nfv	⊢ Ⅎ 𝑎 𝜑
6	1 4	salgencld	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
7		eqid	⊢ ∪ ( 𝐽 ↾t dom 𝐹 ) = ∪ ( 𝐽 ↾t dom 𝐹 )
8		eqid	⊢ ∪ 𝐾 = ∪ 𝐾
9	7 8	cnf	⊢ ( 𝐹 ∈ ( ( 𝐽 ↾t dom 𝐹 ) Cn 𝐾 ) → 𝐹 : ∪ ( 𝐽 ↾t dom 𝐹 ) ⟶ ∪ 𝐾 )
10	3 9	syl	⊢ ( 𝜑 → 𝐹 : ∪ ( 𝐽 ↾t dom 𝐹 ) ⟶ ∪ 𝐾 )
11	10	fdmd	⊢ ( 𝜑 → dom 𝐹 = ∪ ( 𝐽 ↾t dom 𝐹 ) )
12		ovex	⊢ ( 𝐽 ↾t dom 𝐹 ) ∈ V
13	12	uniex	⊢ ∪ ( 𝐽 ↾t dom 𝐹 ) ∈ V
14	13	a1i	⊢ ( 𝜑 → ∪ ( 𝐽 ↾t dom 𝐹 ) ∈ V )
15	11 14	eqeltrd	⊢ ( 𝜑 → dom 𝐹 ∈ V )
16	1 15	unirestss	⊢ ( 𝜑 → ∪ ( 𝐽 ↾t dom 𝐹 ) ⊆ ∪ 𝐽 )
17	4	sssalgen	⊢ ( 𝐽 ∈ Top → 𝐽 ⊆ 𝑆 )
18	1 17	syl	⊢ ( 𝜑 → 𝐽 ⊆ 𝑆 )
19	18	unissd	⊢ ( 𝜑 → ∪ 𝐽 ⊆ ∪ 𝑆 )
20	16 19	sstrd	⊢ ( 𝜑 → ∪ ( 𝐽 ↾t dom 𝐹 ) ⊆ ∪ 𝑆 )
21	11 20	eqsstrd	⊢ ( 𝜑 → dom 𝐹 ⊆ ∪ 𝑆 )
22		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
23	2	unieqi	⊢ ∪ 𝐾 = ∪ ( topGen ‘ ran (,) )
24	22 23	eqtr4i	⊢ ℝ = ∪ 𝐾
25	24	a1i	⊢ ( 𝜑 → ℝ = ∪ 𝐾 )
26	25	feq3d	⊢ ( 𝜑 → ( 𝐹 : ∪ ( 𝐽 ↾t dom 𝐹 ) ⟶ ℝ ↔ 𝐹 : ∪ ( 𝐽 ↾t dom 𝐹 ) ⟶ ∪ 𝐾 ) )
27	10 26	mpbird	⊢ ( 𝜑 → 𝐹 : ∪ ( 𝐽 ↾t dom 𝐹 ) ⟶ ℝ )
28	27	ffdmd	⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ )
29		ssrest	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐽 ⊆ 𝑆 ) → ( 𝐽 ↾t dom 𝐹 ) ⊆ ( 𝑆 ↾t dom 𝐹 ) )
30	6 18 29	syl2anc	⊢ ( 𝜑 → ( 𝐽 ↾t dom 𝐹 ) ⊆ ( 𝑆 ↾t dom 𝐹 ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝐽 ↾t dom 𝐹 ) ⊆ ( 𝑆 ↾t dom 𝐹 ) )
32	11	rabeqdv	⊢ ( 𝜑 → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = { 𝑥 ∈ ∪ ( 𝐽 ↾t dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = { 𝑥 ∈ ∪ ( 𝐽 ↾t dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
34		nfcv	⊢ Ⅎ 𝑥 𝑎
35		nfcv	⊢ Ⅎ 𝑥 𝐹
36		nfv	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑎 ∈ ℝ )
37		eqid	⊢ { 𝑥 ∈ ∪ ( 𝐽 ↾t dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = { 𝑥 ∈ ∪ ( 𝐽 ↾t dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 }
38		rexr	⊢ ( 𝑎 ∈ ℝ → 𝑎 ∈ ℝ* )
39	38	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ* )
40	3	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐹 ∈ ( ( 𝐽 ↾t dom 𝐹 ) Cn 𝐾 ) )
41	34 35 36 2 7 37 39 40	rfcnpre2	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ∪ ( 𝐽 ↾t dom 𝐹 ) ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝐽 ↾t dom 𝐹 ) )
42	33 41	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝐽 ↾t dom 𝐹 ) )
43	31 42	sseldd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t dom 𝐹 ) )
44	5 6 21 28 43	issmfd	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )