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	$⊢ φ \to J \in Top$
	cnfsmf.k	$⊢ K = topGen (ran (.))$
	cnfsmf.f	$⊢ φ \to F \in ((J ↾_{𝑡} dom F) Cn K)$
	cnfsmf.s	$⊢ S = SalGen (J)$
Assertion	cnfsmf	$⊢ φ \to F \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		cnfsmf.1	$⊢ φ \to J \in Top$
2		cnfsmf.k	$⊢ K = topGen (ran (.))$
3		cnfsmf.f	$⊢ φ \to F \in ((J ↾_{𝑡} dom F) Cn K)$
4		cnfsmf.s	$⊢ S = SalGen (J)$
5		nfv	$⊢ Ⅎ a φ$
6	1 4	salgencld	$⊢ φ \to S \in SAlg$
7		eqid	$⊢ ⋃ (J ↾_{𝑡} dom F) = ⋃ (J ↾_{𝑡} dom F)$
8		eqid	$⊢ ⋃ K = ⋃ K$
9	7 8	cnf	$⊢ F \in ((J ↾_{𝑡} dom F) Cn K) \to F : ⋃ (J ↾_{𝑡} dom F) ⟶ ⋃ K$
10	3 9	syl	$⊢ φ \to F : ⋃ (J ↾_{𝑡} dom F) ⟶ ⋃ K$
11	10	fdmd	$⊢ φ \to dom F = ⋃ (J ↾_{𝑡} dom F)$
12		ovex	$⊢ J ↾_{𝑡} dom F \in V$
13	12	uniex	$⊢ ⋃ (J ↾_{𝑡} dom F) \in V$
14	13	a1i	$⊢ φ \to ⋃ (J ↾_{𝑡} dom F) \in V$
15	11 14	eqeltrd	$⊢ φ \to dom F \in V$
16	1 15	unirestss	$⊢ φ \to ⋃ (J ↾_{𝑡} dom F) \subseteq ⋃ J$
17	4	sssalgen	$⊢ J \in Top \to J \subseteq S$
18	1 17	syl	$⊢ φ \to J \subseteq S$
19	18	unissd	$⊢ φ \to ⋃ J \subseteq ⋃ S$
20	16 19	sstrd	$⊢ φ \to ⋃ (J ↾_{𝑡} dom F) \subseteq ⋃ S$
21	11 20	eqsstrd	$⊢ φ \to dom F \subseteq ⋃ S$
22		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
23	2	unieqi	$⊢ ⋃ K = ⋃ topGen (ran (.))$
24	22 23	eqtr4i	$⊢ ℝ = ⋃ K$
25	24	a1i	$⊢ φ \to ℝ = ⋃ K$
26	25	feq3d	$⊢ φ \to (F : ⋃ (J ↾_{𝑡} dom F) ⟶ ℝ \leftrightarrow F : ⋃ (J ↾_{𝑡} dom F) ⟶ ⋃ K)$
27	10 26	mpbird	$⊢ φ \to F : ⋃ (J ↾_{𝑡} dom F) ⟶ ℝ$
28	27	ffdmd	$⊢ φ \to F : dom F ⟶ ℝ$
29		ssrest	$⊢ (S \in SAlg \land J \subseteq S) \to J ↾_{𝑡} dom F \subseteq S ↾_{𝑡} dom F$
30	6 18 29	syl2anc	$⊢ φ \to J ↾_{𝑡} dom F \subseteq S ↾_{𝑡} dom F$
31	30	adantr	$⊢ (φ \land a \in ℝ) \to J ↾_{𝑡} dom F \subseteq S ↾_{𝑡} dom F$
32	11	rabeqdv	$⊢ φ \to \{x \in dom F \| F (x) < a\} = \{x \in ⋃ (J ↾_{𝑡} dom F) \| F (x) < a\}$
33	32	adantr	$⊢ (φ \land a \in ℝ) \to \{x \in dom F \| F (x) < a\} = \{x \in ⋃ (J ↾_{𝑡} dom F) \| F (x) < a\}$
34		nfcv	$⊢ \underline{Ⅎ} x a$
35		nfcv	$⊢ \underline{Ⅎ} x F$
36		nfv	$⊢ Ⅎ x (φ \land a \in ℝ)$
37		eqid	$⊢ \{x \in ⋃ (J ↾_{𝑡} dom F) \| F (x) < a\} = \{x \in ⋃ (J ↾_{𝑡} dom F) \| F (x) < a\}$
38		rexr	$⊢ a \in ℝ \to a \in ℝ^{*}$
39	38	adantl	$⊢ (φ \land a \in ℝ) \to a \in ℝ^{*}$
40	3	adantr	$⊢ (φ \land a \in ℝ) \to F \in ((J ↾_{𝑡} dom F) Cn K)$
41	34 35 36 2 7 37 39 40	rfcnpre2	$⊢ (φ \land a \in ℝ) \to \{x \in ⋃ (J ↾_{𝑡} dom F) \| F (x) < a\} \in (J ↾_{𝑡} dom F)$
42	33 41	eqeltrd	$⊢ (φ \land a \in ℝ) \to \{x \in dom F \| F (x) < a\} \in (J ↾_{𝑡} dom F)$
43	31 42	sseldd	$⊢ (φ \land a \in ℝ) \to \{x \in dom F \| F (x) < a\} \in (S ↾_{𝑡} dom F)$
44	5 6 21 28 43	issmfd	$⊢ φ \to F \in SMblFn (S)$

Metamath Proof Explorer

Theorem cnfsmf

Proof