issmflem

Description: The predicate " F is a real-valued measurable function w.r.t. to the sigma-algebra S ". A function is measurable iff the preimages of all open intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of F is required to be a subset of the underlying set of S . Definition 121C of Fremlin1 p. 36, and Proposition 121B (i) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	issmflem.s	$⊢ φ \to S \in SAlg$
	issmflem.d	$⊢ D = dom F$
Assertion	issmflem	$⊢ φ \to (F \in SMblFn (S) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D)))$

Proof

Step	Hyp	Ref	Expression
1		issmflem.s	$⊢ φ \to S \in SAlg$
2		issmflem.d	$⊢ D = dom F$
3		simpr	$⊢ (φ \land F \in SMblFn (S)) \to F \in SMblFn (S)$
4		df-smblfn	$⊢ SMblFn = (s \in SAlg ⟼ \{f \in (ℝ ↑_{𝑝𝑚} ⋃ s) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (s ↾_{𝑡} dom f)\})$
5		unieq	$⊢ s = S \to ⋃ s = ⋃ S$
6	5	oveq2d	$⊢ s = S \to ℝ ↑_{𝑝𝑚} ⋃ s = ℝ ↑_{𝑝𝑚} ⋃ S$
7	6	rabeqdv	$⊢ s = S \to \{f \in (ℝ ↑_{𝑝𝑚} ⋃ s) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (s ↾_{𝑡} dom f)\} = \{f \in (ℝ ↑_{𝑝𝑚} ⋃ S) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (s ↾_{𝑡} dom f)\}$
8		oveq1	$⊢ s = S \to s ↾_{𝑡} dom f = S ↾_{𝑡} dom f$
9	8	eleq2d	$⊢ s = S \to (f^{-1} [(−∞, a)] \in (s ↾_{𝑡} dom f) \leftrightarrow f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f))$
10	9	ralbidv	$⊢ s = S \to (\forall a \in ℝ f^{-1} [(−∞, a)] \in (s ↾_{𝑡} dom f) \leftrightarrow \forall a \in ℝ f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f))$
11	10	rabbidv	$⊢ s = S \to \{f \in (ℝ ↑_{𝑝𝑚} ⋃ S) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (s ↾_{𝑡} dom f)\} = \{f \in (ℝ ↑_{𝑝𝑚} ⋃ S) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f)\}$
12	7 11	eqtrd	$⊢ s = S \to \{f \in (ℝ ↑_{𝑝𝑚} ⋃ s) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (s ↾_{𝑡} dom f)\} = \{f \in (ℝ ↑_{𝑝𝑚} ⋃ S) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f)\}$
13		ovex	$⊢ ℝ ↑_{𝑝𝑚} ⋃ S \in V$
14	13	rabex	$⊢ \{f \in (ℝ ↑_{𝑝𝑚} ⋃ S) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f)\} \in V$
15	14	a1i	$⊢ φ \to \{f \in (ℝ ↑_{𝑝𝑚} ⋃ S) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f)\} \in V$
16	4 12 1 15	fvmptd3	$⊢ φ \to SMblFn (S) = \{f \in (ℝ ↑_{𝑝𝑚} ⋃ S) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f)\}$
17	16	adantr	$⊢ (φ \land F \in SMblFn (S)) \to SMblFn (S) = \{f \in (ℝ ↑_{𝑝𝑚} ⋃ S) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f)\}$
18	3 17	eleqtrd	$⊢ (φ \land F \in SMblFn (S)) \to F \in \{f \in (ℝ ↑_{𝑝𝑚} ⋃ S) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f)\}$
19		elrabi	$⊢ F \in \{f \in (ℝ ↑_{𝑝𝑚} ⋃ S) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f)\} \to F \in (ℝ ↑_{𝑝𝑚} ⋃ S)$
20	18 19	syl	$⊢ (φ \land F \in SMblFn (S)) \to F \in (ℝ ↑_{𝑝𝑚} ⋃ S)$
21		elpmi2	$⊢ F \in (ℝ ↑_{𝑝𝑚} ⋃ S) \to dom F \subseteq ⋃ S$
22	2 21	eqsstrid	$⊢ F \in (ℝ ↑_{𝑝𝑚} ⋃ S) \to D \subseteq ⋃ S$
23	22	adantl	$⊢ (φ \land F \in (ℝ ↑_{𝑝𝑚} ⋃ S)) \to D \subseteq ⋃ S$
24	20 23	syldan	$⊢ (φ \land F \in SMblFn (S)) \to D \subseteq ⋃ S$
25		elpmi	$⊢ F \in (ℝ ↑_{𝑝𝑚} ⋃ S) \to (F : dom F ⟶ ℝ \land dom F \subseteq ⋃ S)$
26	20 25	syl	$⊢ (φ \land F \in SMblFn (S)) \to (F : dom F ⟶ ℝ \land dom F \subseteq ⋃ S)$
27	26	simpld	$⊢ (φ \land F \in SMblFn (S)) \to F : dom F ⟶ ℝ$
28	2	feq2i	$⊢ F : D ⟶ ℝ \leftrightarrow F : dom F ⟶ ℝ$
29	28	a1i	$⊢ (φ \land F \in SMblFn (S)) \to (F : D ⟶ ℝ \leftrightarrow F : dom F ⟶ ℝ)$
30	27 29	mpbird	$⊢ (φ \land F \in SMblFn (S)) \to F : D ⟶ ℝ$
31		cnveq	$⊢ f = F \to f^{-1} = F^{-1}$
32	31	imaeq1d	$⊢ f = F \to f^{-1} [(−∞, a)] = F^{-1} [(−∞, a)]$
33		dmeq	$⊢ f = F \to dom f = dom F$
34	33	oveq2d	$⊢ f = F \to S ↾_{𝑡} dom f = S ↾_{𝑡} dom F$
35	32 34	eleq12d	$⊢ f = F \to (f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f) \leftrightarrow F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F))$
36	35	ralbidv	$⊢ f = F \to (\forall a \in ℝ f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f) \leftrightarrow \forall a \in ℝ F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F))$
37	36	elrab	$⊢ F \in \{f \in (ℝ ↑_{𝑝𝑚} ⋃ S) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f)\} \leftrightarrow (F \in (ℝ ↑_{𝑝𝑚} ⋃ S) \land \forall a \in ℝ F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F))$
38	37	simprbi	$⊢ F \in \{f \in (ℝ ↑_{𝑝𝑚} ⋃ S) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f)\} \to \forall a \in ℝ F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F)$
39	18 38	syl	$⊢ (φ \land F \in SMblFn (S)) \to \forall a \in ℝ F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F)$
40	39	adantr	$⊢ ((φ \land F \in SMblFn (S)) \land a \in ℝ) \to \forall a \in ℝ F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F)$
41		simpr	$⊢ ((φ \land F \in SMblFn (S)) \land a \in ℝ) \to a \in ℝ$
42		rspa	$⊢ (\forall a \in ℝ F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F) \land a \in ℝ) \to F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F)$
43	40 41 42	syl2anc	$⊢ ((φ \land F \in SMblFn (S)) \land a \in ℝ) \to F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F)$
44	30	adantr	$⊢ ((φ \land F \in SMblFn (S)) \land a \in ℝ) \to F : D ⟶ ℝ$
45		simpl	$⊢ (F : D ⟶ ℝ \land a \in ℝ) \to F : D ⟶ ℝ$
46		simpr	$⊢ (F : D ⟶ ℝ \land a \in ℝ) \to a \in ℝ$
47	46	rexrd	$⊢ (F : D ⟶ ℝ \land a \in ℝ) \to a \in ℝ^{*}$
48	45 47	preimaioomnf	$⊢ (F : D ⟶ ℝ \land a \in ℝ) \to F^{-1} [(−∞, a)] = \{x \in D \| F (x) < a\}$
49	48	eqcomd	$⊢ (F : D ⟶ ℝ \land a \in ℝ) \to \{x \in D \| F (x) < a\} = F^{-1} [(−∞, a)]$
50	44 41 49	syl2anc	$⊢ ((φ \land F \in SMblFn (S)) \land a \in ℝ) \to \{x \in D \| F (x) < a\} = F^{-1} [(−∞, a)]$
51	2	oveq2i	$⊢ S ↾_{𝑡} D = S ↾_{𝑡} dom F$
52	51	a1i	$⊢ ((φ \land F \in SMblFn (S)) \land a \in ℝ) \to S ↾_{𝑡} D = S ↾_{𝑡} dom F$
53	50 52	eleq12d	$⊢ ((φ \land F \in SMblFn (S)) \land a \in ℝ) \to (\{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D) \leftrightarrow F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F))$
54	43 53	mpbird	$⊢ ((φ \land F \in SMblFn (S)) \land a \in ℝ) \to \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D)$
55	54	ralrimiva	$⊢ (φ \land F \in SMblFn (S)) \to \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D)$
56	24 30 55	3jca	$⊢ (φ \land F \in SMblFn (S)) \to (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D))$
57	56	ex	$⊢ φ \to (F \in SMblFn (S) \to (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D)))$
58		reex	$⊢ ℝ \in V$
59	58	a1i	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ)) \to ℝ \in V$
60	1	uniexd	$⊢ φ \to ⋃ S \in V$
61	60	adantr	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ)) \to ⋃ S \in V$
62		simprr	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ)) \to F : D ⟶ ℝ$
63		fssxp	$⊢ F : D ⟶ ℝ \to F \subseteq D \times ℝ$
64	63	adantl	$⊢ (D \subseteq ⋃ S \land F : D ⟶ ℝ) \to F \subseteq D \times ℝ$
65		xpss1	$⊢ D \subseteq ⋃ S \to D \times ℝ \subseteq ⋃ S \times ℝ$
66	65	adantr	$⊢ (D \subseteq ⋃ S \land F : D ⟶ ℝ) \to D \times ℝ \subseteq ⋃ S \times ℝ$
67	64 66	sstrd	$⊢ (D \subseteq ⋃ S \land F : D ⟶ ℝ) \to F \subseteq ⋃ S \times ℝ$
68	67	adantl	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ)) \to F \subseteq ⋃ S \times ℝ$
69		dmss	$⊢ F \subseteq ⋃ S \times ℝ \to dom F \subseteq dom (⋃ S \times ℝ)$
70		dmxpss	$⊢ dom (⋃ S \times ℝ) \subseteq ⋃ S$
71	70	a1i	$⊢ F \subseteq ⋃ S \times ℝ \to dom (⋃ S \times ℝ) \subseteq ⋃ S$
72	69 71	sstrd	$⊢ F \subseteq ⋃ S \times ℝ \to dom F \subseteq ⋃ S$
73	72	adantl	$⊢ (φ \land F \subseteq ⋃ S \times ℝ) \to dom F \subseteq ⋃ S$
74	2 73	eqsstrid	$⊢ (φ \land F \subseteq ⋃ S \times ℝ) \to D \subseteq ⋃ S$
75	68 74	syldan	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ)) \to D \subseteq ⋃ S$
76		elpm2r	$⊢ ((ℝ \in V \land ⋃ S \in V) \land (F : D ⟶ ℝ \land D \subseteq ⋃ S)) \to F \in (ℝ ↑_{𝑝𝑚} ⋃ S)$
77	59 61 62 75 76	syl22anc	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ)) \to F \in (ℝ ↑_{𝑝𝑚} ⋃ S)$
78	77	3adantr3	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D))) \to F \in (ℝ ↑_{𝑝𝑚} ⋃ S)$
79	2	a1i	$⊢ (F : D ⟶ ℝ \land a \in ℝ) \to D = dom F$
80	79	oveq2d	$⊢ (F : D ⟶ ℝ \land a \in ℝ) \to S ↾_{𝑡} D = S ↾_{𝑡} dom F$
81	49 80	eleq12d	$⊢ (F : D ⟶ ℝ \land a \in ℝ) \to (\{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D) \leftrightarrow F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F))$
82	81	ralbidva	$⊢ F : D ⟶ ℝ \to (\forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D) \leftrightarrow \forall a \in ℝ F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F))$
83	82	biimpd	$⊢ F : D ⟶ ℝ \to (\forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D) \to \forall a \in ℝ F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F))$
84	83	imp	$⊢ (F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D)) \to \forall a \in ℝ F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F)$
85	84	adantl	$⊢ (φ \land (F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D))) \to \forall a \in ℝ F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F)$
86	85	3adantr1	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D))) \to \forall a \in ℝ F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F)$
87	78 86	jca	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D))) \to (F \in (ℝ ↑_{𝑝𝑚} ⋃ S) \land \forall a \in ℝ F^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom F))$
88	87 37	sylibr	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D))) \to F \in \{f \in (ℝ ↑_{𝑝𝑚} ⋃ S) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f)\}$
89	16	eqcomd	$⊢ φ \to \{f \in (ℝ ↑_{𝑝𝑚} ⋃ S) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f)\} = SMblFn (S)$
90	89	adantr	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D))) \to \{f \in (ℝ ↑_{𝑝𝑚} ⋃ S) \| \forall a \in ℝ f^{-1} [(−∞, a)] \in (S ↾_{𝑡} dom f)\} = SMblFn (S)$
91	88 90	eleqtrd	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D))) \to F \in SMblFn (S)$
92	91	ex	$⊢ φ \to ((D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D)) \to F \in SMblFn (S))$
93	57 92	impbid	$⊢ φ \to (F \in SMblFn (S) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) < a\} \in (S ↾_{𝑡} D)))$

Metamath Proof Explorer

Theorem issmflem

Proof