smfco

Description: The composition of a Borel sigma-measurable function with a sigma-measurable function, is sigma-measurable. Proposition 121E (g) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfco.s	$⊢ φ \to S \in SAlg$
	smfco.f	$⊢ φ \to F \in SMblFn (S)$
	smfco.j	$⊢ J = topGen (ran (.))$
	smfco.b	$⊢ B = SalGen (J)$
	smfco.h	$⊢ φ \to H \in SMblFn (B)$
Assertion	smfco	$⊢ φ \to H \circ F \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smfco.s	$⊢ φ \to S \in SAlg$
2		smfco.f	$⊢ φ \to F \in SMblFn (S)$
3		smfco.j	$⊢ J = topGen (ran (.))$
4		smfco.b	$⊢ B = SalGen (J)$
5		smfco.h	$⊢ φ \to H \in SMblFn (B)$
6		nfv	$⊢ Ⅎ a φ$
7		cnvimass	$⊢ F^{-1} [dom H] \subseteq dom F$
8	7	a1i	$⊢ φ \to F^{-1} [dom H] \subseteq dom F$
9		eqid	$⊢ dom F = dom F$
10	1 2 9	smfdmss	$⊢ φ \to dom F \subseteq ⋃ S$
11	8 10	sstrd	$⊢ φ \to F^{-1} [dom H] \subseteq ⋃ S$
12		retop	$⊢ topGen (ran (.)) \in Top$
13	3 12	eqeltri	$⊢ J \in Top$
14	13	a1i	$⊢ φ \to J \in Top$
15	14 4	salgencld	$⊢ φ \to B \in SAlg$
16		eqid	$⊢ dom H = dom H$
17	15 5 16	smff	$⊢ φ \to H : dom H ⟶ ℝ$
18	17	ffund	$⊢ φ \to Fun H$
19	1 2 9	smff	$⊢ φ \to F : dom F ⟶ ℝ$
20	19	ffund	$⊢ φ \to Fun F$
21	18 20	funcofd	$⊢ φ \to (H \circ F) : F^{-1} [dom H] ⟶ ran H$
22	17	frnd	$⊢ φ \to ran H \subseteq ℝ$
23	21 22	fssd	$⊢ φ \to (H \circ F) : F^{-1} [dom H] ⟶ ℝ$
24		cnvco	$⊢ {(H \circ F)}^{-1} = F^{-1} \circ H^{-1}$
25	24	imaeq1i	$⊢ {(H \circ F)}^{-1} [(−∞, a)] = (F^{-1} \circ H^{-1}) [(−∞, a)]$
26	23	adantr	$⊢ (φ \land a \in ℝ) \to (H \circ F) : F^{-1} [dom H] ⟶ ℝ$
27		rexr	$⊢ a \in ℝ \to a \in ℝ^{*}$
28	27	adantl	$⊢ (φ \land a \in ℝ) \to a \in ℝ^{*}$
29	26 28	preimaioomnf	$⊢ (φ \land a \in ℝ) \to {(H \circ F)}^{-1} [(−∞, a)] = \{x \in F^{-1} [dom H] \| (H \circ F) (x) < a\}$
30		imaco	$⊢ (F^{-1} \circ H^{-1}) [(−∞, a)] = F^{-1} [H^{-1} [(−∞, a)]]$
31	30	a1i	$⊢ (φ \land a \in ℝ) \to (F^{-1} \circ H^{-1}) [(−∞, a)] = F^{-1} [H^{-1} [(−∞, a)]]$
32	25 29 31	3eqtr3a	$⊢ (φ \land a \in ℝ) \to \{x \in F^{-1} [dom H] \| (H \circ F) (x) < a\} = F^{-1} [H^{-1} [(−∞, a)]]$
33	17	adantr	$⊢ (φ \land a \in ℝ) \to H : dom H ⟶ ℝ$
34	33 28	preimaioomnf	$⊢ (φ \land a \in ℝ) \to H^{-1} [(−∞, a)] = \{x \in dom H \| H (x) < a\}$
35	15	adantr	$⊢ (φ \land a \in ℝ) \to B \in SAlg$
36	5	adantr	$⊢ (φ \land a \in ℝ) \to H \in SMblFn (B)$
37		simpr	$⊢ (φ \land a \in ℝ) \to a \in ℝ$
38	35 36 16 37	smfpreimalt	$⊢ (φ \land a \in ℝ) \to \{x \in dom H \| H (x) < a\} \in (B ↾_{𝑡} dom H)$
39	34 38	eqeltrd	$⊢ (φ \land a \in ℝ) \to H^{-1} [(−∞, a)] \in (B ↾_{𝑡} dom H)$
40	15	elexd	$⊢ φ \to B \in V$
41	5	dmexd	$⊢ φ \to dom H \in V$
42		elrest	$⊢ (B \in V \land dom H \in V) \to (H^{-1} [(−∞, a)] \in (B ↾_{𝑡} dom H) \leftrightarrow \exists e \in B H^{-1} [(−∞, a)] = e \cap dom H)$
43	40 41 42	syl2anc	$⊢ φ \to (H^{-1} [(−∞, a)] \in (B ↾_{𝑡} dom H) \leftrightarrow \exists e \in B H^{-1} [(−∞, a)] = e \cap dom H)$
44	43	adantr	$⊢ (φ \land a \in ℝ) \to (H^{-1} [(−∞, a)] \in (B ↾_{𝑡} dom H) \leftrightarrow \exists e \in B H^{-1} [(−∞, a)] = e \cap dom H)$
45	39 44	mpbid	$⊢ (φ \land a \in ℝ) \to \exists e \in B H^{-1} [(−∞, a)] = e \cap dom H$
46		imaeq2	$⊢ H^{-1} [(−∞, a)] = e \cap dom H \to F^{-1} [H^{-1} [(−∞, a)]] = F^{-1} [e \cap dom H]$
47	46	3ad2ant3	$⊢ (φ \land e \in B \land H^{-1} [(−∞, a)] = e \cap dom H) \to F^{-1} [H^{-1} [(−∞, a)]] = F^{-1} [e \cap dom H]$
48		ovexd	$⊢ (φ \land e \in B) \to S ↾_{𝑡} dom F \in V$
49	2	elexd	$⊢ φ \to F \in V$
50		cnvexg	$⊢ F \in V \to F^{-1} \in V$
51		imaexg	$⊢ F^{-1} \in V \to F^{-1} [dom H] \in V$
52	49 50 51	3syl	$⊢ φ \to F^{-1} [dom H] \in V$
53	52	adantr	$⊢ (φ \land e \in B) \to F^{-1} [dom H] \in V$
54	1	adantr	$⊢ (φ \land e \in B) \to S \in SAlg$
55	2	adantr	$⊢ (φ \land e \in B) \to F \in SMblFn (S)$
56		simpr	$⊢ (φ \land e \in B) \to e \in B$
57		eqid	$⊢ F^{-1} [e] = F^{-1} [e]$
58	54 55 9 3 4 56 57	smfpimbor1	$⊢ (φ \land e \in B) \to F^{-1} [e] \in (S ↾_{𝑡} dom F)$
59		eqid	$⊢ F^{-1} [e] \cap F^{-1} [dom H] = F^{-1} [e] \cap F^{-1} [dom H]$
60	48 53 58 59	elrestd	$⊢ (φ \land e \in B) \to F^{-1} [e] \cap F^{-1} [dom H] \in ((S ↾_{𝑡} dom F) ↾_{𝑡} F^{-1} [dom H])$
61		inpreima	$⊢ Fun F \to F^{-1} [e \cap dom H] = F^{-1} [e] \cap F^{-1} [dom H]$
62	20 61	syl	$⊢ φ \to F^{-1} [e \cap dom H] = F^{-1} [e] \cap F^{-1} [dom H]$
63	62	adantr	$⊢ (φ \land e \in B) \to F^{-1} [e \cap dom H] = F^{-1} [e] \cap F^{-1} [dom H]$
64	2	dmexd	$⊢ φ \to dom F \in V$
65		restabs	$⊢ (S \in SAlg \land F^{-1} [dom H] \subseteq dom F \land dom F \in V) \to (S ↾_{𝑡} dom F) ↾_{𝑡} F^{-1} [dom H] = S ↾_{𝑡} F^{-1} [dom H]$
66	1 8 64 65	syl3anc	$⊢ φ \to (S ↾_{𝑡} dom F) ↾_{𝑡} F^{-1} [dom H] = S ↾_{𝑡} F^{-1} [dom H]$
67	66	eqcomd	$⊢ φ \to S ↾_{𝑡} F^{-1} [dom H] = (S ↾_{𝑡} dom F) ↾_{𝑡} F^{-1} [dom H]$
68	67	adantr	$⊢ (φ \land e \in B) \to S ↾_{𝑡} F^{-1} [dom H] = (S ↾_{𝑡} dom F) ↾_{𝑡} F^{-1} [dom H]$
69	60 63 68	3eltr4d	$⊢ (φ \land e \in B) \to F^{-1} [e \cap dom H] \in (S ↾_{𝑡} F^{-1} [dom H])$
70	69	3adant3	$⊢ (φ \land e \in B \land H^{-1} [(−∞, a)] = e \cap dom H) \to F^{-1} [e \cap dom H] \in (S ↾_{𝑡} F^{-1} [dom H])$
71	47 70	eqeltrd	$⊢ (φ \land e \in B \land H^{-1} [(−∞, a)] = e \cap dom H) \to F^{-1} [H^{-1} [(−∞, a)]] \in (S ↾_{𝑡} F^{-1} [dom H])$
72	71	3exp	$⊢ φ \to (e \in B \to (H^{-1} [(−∞, a)] = e \cap dom H \to F^{-1} [H^{-1} [(−∞, a)]] \in (S ↾_{𝑡} F^{-1} [dom H])))$
73	72	adantr	$⊢ (φ \land a \in ℝ) \to (e \in B \to (H^{-1} [(−∞, a)] = e \cap dom H \to F^{-1} [H^{-1} [(−∞, a)]] \in (S ↾_{𝑡} F^{-1} [dom H])))$
74	73	rexlimdv	$⊢ (φ \land a \in ℝ) \to (\exists e \in B H^{-1} [(−∞, a)] = e \cap dom H \to F^{-1} [H^{-1} [(−∞, a)]] \in (S ↾_{𝑡} F^{-1} [dom H]))$
75	45 74	mpd	$⊢ (φ \land a \in ℝ) \to F^{-1} [H^{-1} [(−∞, a)]] \in (S ↾_{𝑡} F^{-1} [dom H])$
76	32 75	eqeltrd	$⊢ (φ \land a \in ℝ) \to \{x \in F^{-1} [dom H] \| (H \circ F) (x) < a\} \in (S ↾_{𝑡} F^{-1} [dom H])$
77	6 1 11 23 76	issmfd	$⊢ φ \to H \circ F \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfco

Proof