Theorem sssmf 47276

Description: The restriction of a sigma-measurable function, is sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypotheses

Ref	Expression
sssmf.s	⊢ (𝜑 → 𝑆 ∈ SAlg)
sssmf.f	⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))

Assertion

Ref	Expression
sssmf	⊢ (𝜑 → (𝐹 ↾ 𝐵) ∈ (SMblFn‘𝑆))

Proof of Theorem sssmf

Dummy variables 𝑎 𝑤 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1933	. 2 ⊢ Ⅎ𝑎𝜑
2		sssmf.s	. 2 ⊢ (𝜑 → 𝑆 ∈ SAlg)
3		inss2 4189	. . 3 ⊢ (𝐵 ∩ dom 𝐹) ⊆ dom 𝐹
4		sssmf.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))
5		eqid 2761	. . . 4 ⊢ dom 𝐹 = dom 𝐹
6	2, 4, 5	smfdmss 47271	. . 3 ⊢ (𝜑 → dom 𝐹 ⊆ ∪ 𝑆)
7	3, 6	sstrid 3947	. 2 ⊢ (𝜑 → (𝐵 ∩ dom 𝐹) ⊆ ∪ 𝑆)
8		resindm 6014	. . . 4 ⊢ (𝐹 ↾ (𝐵 ∩ dom 𝐹)) = (𝐹 ↾ 𝐵)
9	8	a1i 11	. . 3 ⊢ (𝜑 → (𝐹 ↾ (𝐵 ∩ dom 𝐹)) = (𝐹 ↾ 𝐵))
10	2, 4, 5	smff 47270	. . . 4 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℝ)
11	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝐵 ∩ dom 𝐹) ⊆ dom 𝐹)
12	10, 11	fssresd 6727	. . 3 ⊢ (𝜑 → (𝐹 ↾ (𝐵 ∩ dom 𝐹)):(𝐵 ∩ dom 𝐹)⟶ℝ)
13	9, 12	feq1dd 6670	. 2 ⊢ (𝜑 → (𝐹 ↾ 𝐵):(𝐵 ∩ dom 𝐹)⟶ℝ)
14	2	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑆 ∈ SAlg)
15	4	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝐹 ∈ (SMblFn‘𝑆))
16		simpr 488	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
17	14, 15, 5, 16	smfpreimalt 47269	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t dom 𝐹))
18	4	dmexd 7880	. . . . . 6 ⊢ (𝜑 → dom 𝐹 ∈ V)
19		elrest 17439	. . . . . 6 ⊢ ((𝑆 ∈ SAlg ∧ dom 𝐹 ∈ V) → ({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t dom 𝐹) ↔ ∃𝑤 ∈ 𝑆 {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)))
20	2, 18, 19	syl2anc 593	. . . . 5 ⊢ (𝜑 → ({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t dom 𝐹) ↔ ∃𝑤 ∈ 𝑆 {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)))
21	20	adantr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} ∈ (𝑆 ↾t dom 𝐹) ↔ ∃𝑤 ∈ 𝑆 {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)))
22	17, 21	mpbid 234	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ∃𝑤 ∈ 𝑆 {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹))
23		elinel1 4153	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐵 ∩ dom 𝐹) → 𝑥 ∈ 𝐵)
24	23	fvresd 6883	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐵 ∩ dom 𝐹) → ((𝐹 ↾ 𝐵)‘𝑥) = (𝐹‘𝑥))
25	24	breq1d 5109	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐵 ∩ dom 𝐹) → (((𝐹 ↾ 𝐵)‘𝑥) < 𝑎 ↔ (𝐹‘𝑥) < 𝑎))
26	25	rabbiia 3417	. . . . . . 7 ⊢ {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ ((𝐹 ↾ 𝐵)‘𝑥) < 𝑎} = {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹‘𝑥) < 𝑎}
27		rabss2 4030	. . . . . . . . . . 11 ⊢ ((𝐵 ∩ dom 𝐹) ⊆ dom 𝐹 → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹‘𝑥) < 𝑎} ⊆ {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎})
28	3, 27	ax-mp 5	. . . . . . . . . 10 ⊢ {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹‘𝑥) < 𝑎} ⊆ {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎}
29		id 22	. . . . . . . . . . 11 ⊢ ({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹))
30		inss1 4188	. . . . . . . . . . 11 ⊢ (𝑤 ∩ dom 𝐹) ⊆ 𝑤
31	29, 30	eqsstrdi 3980	. . . . . . . . . 10 ⊢ ({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} ⊆ 𝑤)
32	28, 31	sstrid 3947	. . . . . . . . 9 ⊢ ({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹‘𝑥) < 𝑎} ⊆ 𝑤)
33		ssrab2 4033	. . . . . . . . . 10 ⊢ {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹‘𝑥) < 𝑎} ⊆ (𝐵 ∩ dom 𝐹)
34	33	a1i 11	. . . . . . . . 9 ⊢ ({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹‘𝑥) < 𝑎} ⊆ (𝐵 ∩ dom 𝐹))
35	32, 34	ssind 4192	. . . . . . . 8 ⊢ ({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹‘𝑥) < 𝑎} ⊆ (𝑤 ∩ (𝐵 ∩ dom 𝐹)))
36		nfrab1 3433	. . . . . . . . . 10 ⊢ Ⅎ𝑥{𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎}
37	36	nfeq1 2938	. . . . . . . . 9 ⊢ Ⅎ𝑥{𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)
38		nfcv 2923	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑤 ∩ (𝐵 ∩ dom 𝐹))
39		nfrab1 3433	. . . . . . . . 9 ⊢ Ⅎ𝑥{𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹‘𝑥) < 𝑎}
40		elinel2 4154	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹)) → 𝑥 ∈ (𝐵 ∩ dom 𝐹))
41	40	adantl 485	. . . . . . . . . 10 ⊢ (({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) ∧ 𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))) → 𝑥 ∈ (𝐵 ∩ dom 𝐹))
42		elinel1 4153	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹)) → 𝑥 ∈ 𝑤)
43	40	elin2d 4157	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹)) → 𝑥 ∈ dom 𝐹)
44	42, 43	elind 4152	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹)) → 𝑥 ∈ (𝑤 ∩ dom 𝐹))
45	44	adantl 485	. . . . . . . . . . . 12 ⊢ (({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) ∧ 𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))) → 𝑥 ∈ (𝑤 ∩ dom 𝐹))
46	29	eqcomd 2767	. . . . . . . . . . . . 13 ⊢ ({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → (𝑤 ∩ dom 𝐹) = {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎})
47	46	adantr 484	. . . . . . . . . . . 12 ⊢ (({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) ∧ 𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))) → (𝑤 ∩ dom 𝐹) = {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎})
48	45, 47	eleqtrd 2863	. . . . . . . . . . 11 ⊢ (({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) ∧ 𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))) → 𝑥 ∈ {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎})
49		rabidim2 45644	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} → (𝐹‘𝑥) < 𝑎)
50	48, 49	syl 17	. . . . . . . . . 10 ⊢ (({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) ∧ 𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))) → (𝐹‘𝑥) < 𝑎)
51	41, 50	rabidd 45697	. . . . . . . . 9 ⊢ (({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) ∧ 𝑥 ∈ (𝑤 ∩ (𝐵 ∩ dom 𝐹))) → 𝑥 ∈ {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹‘𝑥) < 𝑎})
52	37, 38, 39, 51	ssdf2 45683	. . . . . . . 8 ⊢ ({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → (𝑤 ∩ (𝐵 ∩ dom 𝐹)) ⊆ {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹‘𝑥) < 𝑎})
53	35, 52	eqssd 3953	. . . . . . 7 ⊢ ({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ (𝐵 ∩ dom 𝐹)))
54	26, 53	eqtrid 2808	. . . . . 6 ⊢ ({𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ ((𝐹 ↾ 𝐵)‘𝑥) < 𝑎} = (𝑤 ∩ (𝐵 ∩ dom 𝐹)))
55	54	3ad2ant3 1147	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑤 ∈ 𝑆 ∧ {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ ((𝐹 ↾ 𝐵)‘𝑥) < 𝑎} = (𝑤 ∩ (𝐵 ∩ dom 𝐹)))
56	14	3ad2ant1 1145	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑤 ∈ 𝑆 ∧ {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)) → 𝑆 ∈ SAlg)
57		simp1l 1210	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑤 ∈ 𝑆 ∧ {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)) → 𝜑)
58	18, 11	ssexd 5279	. . . . . . 7 ⊢ (𝜑 → (𝐵 ∩ dom 𝐹) ∈ V)
59	57, 58	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑤 ∈ 𝑆 ∧ {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)) → (𝐵 ∩ dom 𝐹) ∈ V)
60		simp2 1149	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑤 ∈ 𝑆 ∧ {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)) → 𝑤 ∈ 𝑆)
61		eqid 2761	. . . . . 6 ⊢ (𝑤 ∩ (𝐵 ∩ dom 𝐹)) = (𝑤 ∩ (𝐵 ∩ dom 𝐹))
62	56, 59, 60, 61	elrestd 45650	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑤 ∈ 𝑆 ∧ {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)) → (𝑤 ∩ (𝐵 ∩ dom 𝐹)) ∈ (𝑆 ↾t (𝐵 ∩ dom 𝐹)))
63	55, 62	eqeltrd 2861	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ 𝑤 ∈ 𝑆 ∧ {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹)) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ ((𝐹 ↾ 𝐵)‘𝑥) < 𝑎} ∈ (𝑆 ↾t (𝐵 ∩ dom 𝐹)))
64	63	rexlimdv3a 3166	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∃𝑤 ∈ 𝑆 {𝑥 ∈ dom 𝐹 ∣ (𝐹‘𝑥) < 𝑎} = (𝑤 ∩ dom 𝐹) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ ((𝐹 ↾ 𝐵)‘𝑥) < 𝑎} ∈ (𝑆 ↾t (𝐵 ∩ dom 𝐹))))
65	22, 64	mpd 15	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → {𝑥 ∈ (𝐵 ∩ dom 𝐹) ∣ ((𝐹 ↾ 𝐵)‘𝑥) < 𝑎} ∈ (𝑆 ↾t (𝐵 ∩ dom 𝐹)))
66	1, 2, 7, 13, 65	issmfd 47273	1 ⊢ (𝜑 → (𝐹 ↾ 𝐵) ∈ (SMblFn‘𝑆))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141  ∃wrex 3085  {crab 3413  Vcvv 3453   ∩ cin 3903   ⊆ wss 3904  ∪ cuni 4864   class class class wbr 5099  dom cdm 5645   ↾ cres 5647  ‘cfv 6517  (class class class)co 7392  ℝcr 11069   < clt 11213   ↾_t crest 17432  SAlgcsalg 46846  SMblFncsmblfn 47233

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-cnex 11126  ax-resscn 11127  ax-pre-lttri 11144  ax-pre-lttrn 11145

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-po 5553  df-so 5554  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-ov 7395  df-oprab 7396  df-mpo 7397  df-1st 7966  df-2nd 7967  df-er 8673  df-pm 8806  df-en 8924  df-dom 8925  df-sdom 8926  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-ioo 13350  df-ico 13352  df-rest 17434  df-smblfn 47234

This theorem is referenced by:  sssmfmpt  47288