issmfge

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 left-closed intervals unbounded above are in the subspace sigma-algebra induced by its domain. The domain of F is required to be b subset of the underlying set of S . Definition 121C of Fremlin1 p. 36, and Proposition 121B (iv) of Fremlin1 p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		issmfge.s	$⊢ φ \to S \in SAlg$
2		issmfge.d	$⊢ D = dom F$
3	1	adantr	$⊢ (φ \land F \in SMblFn (S)) \to S \in SAlg$
4		simpr	$⊢ (φ \land F \in SMblFn (S)) \to F \in SMblFn (S)$
5	3 4 2	smfdmss	$⊢ (φ \land F \in SMblFn (S)) \to D \subseteq ⋃ S$
6	3 4 2	smff	$⊢ (φ \land F \in SMblFn (S)) \to F : D ⟶ ℝ$
7		nfv	$⊢ Ⅎ y φ$
8		nfv	$⊢ Ⅎ y F \in SMblFn (S)$
9	7 8	nfan	$⊢ Ⅎ y (φ \land F \in SMblFn (S))$
10		nfv	$⊢ Ⅎ y b \in ℝ$
11	9 10	nfan	$⊢ Ⅎ y ((φ \land F \in SMblFn (S)) \land b \in ℝ)$
12		nfv	$⊢ Ⅎ c ((φ \land F \in SMblFn (S)) \land b \in ℝ)$
13	1	uniexd	$⊢ φ \to ⋃ S \in V$
14	13	adantr	$⊢ (φ \land D \subseteq ⋃ S) \to ⋃ S \in V$
15		simpr	$⊢ (φ \land D \subseteq ⋃ S) \to D \subseteq ⋃ S$
16	14 15	ssexd	$⊢ (φ \land D \subseteq ⋃ S) \to D \in V$
17	5 16	syldan	$⊢ (φ \land F \in SMblFn (S)) \to D \in V$
18		eqid	$⊢ S ↾_{𝑡} D = S ↾_{𝑡} D$
19	3 17 18	subsalsal	$⊢ (φ \land F \in SMblFn (S)) \to S ↾_{𝑡} D \in SAlg$
20	19	adantr	$⊢ ((φ \land F \in SMblFn (S)) \land b \in ℝ) \to S ↾_{𝑡} D \in SAlg$
21	6	ffvelrnda	$⊢ ((φ \land F \in SMblFn (S)) \land y \in D) \to F (y) \in ℝ$
22	21	rexrd	$⊢ ((φ \land F \in SMblFn (S)) \land y \in D) \to F (y) \in ℝ^{*}$
23	22	adantlr	$⊢ (((φ \land F \in SMblFn (S)) \land b \in ℝ) \land y \in D) \to F (y) \in ℝ^{*}$
24	3	adantr	$⊢ ((φ \land F \in SMblFn (S)) \land c \in ℝ) \to S \in SAlg$
25	4	adantr	$⊢ ((φ \land F \in SMblFn (S)) \land c \in ℝ) \to F \in SMblFn (S)$
26		simpr	$⊢ ((φ \land F \in SMblFn (S)) \land c \in ℝ) \to c \in ℝ$
27	24 25 2 26	smfpreimagt	$⊢ ((φ \land F \in SMblFn (S)) \land c \in ℝ) \to \{y \in D \| c < F (y)\} \in (S ↾_{𝑡} D)$
28	27	adantlr	$⊢ (((φ \land F \in SMblFn (S)) \land b \in ℝ) \land c \in ℝ) \to \{y \in D \| c < F (y)\} \in (S ↾_{𝑡} D)$
29		simpr	$⊢ ((φ \land F \in SMblFn (S)) \land b \in ℝ) \to b \in ℝ$
30	11 12 20 23 28 29	salpreimagtge	$⊢ ((φ \land F \in SMblFn (S)) \land b \in ℝ) \to \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D)$
31	30	ralrimiva	$⊢ (φ \land F \in SMblFn (S)) \to \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D)$
32	5 6 31	3jca	$⊢ (φ \land F \in SMblFn (S)) \to (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D))$
33	32	ex	$⊢ φ \to (F \in SMblFn (S) \to (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D)))$
34		nfv	$⊢ Ⅎ y D \subseteq ⋃ S$
35		nfv	$⊢ Ⅎ y F : D ⟶ ℝ$
36		nfcv	$⊢ \underline{Ⅎ} y ℝ$
37		nfrab1	$⊢ \underline{Ⅎ} y \{y \in D \| b \leq F (y)\}$
38		nfcv	$⊢ \underline{Ⅎ} y (S ↾_{𝑡} D)$
39	37 38	nfel	$⊢ Ⅎ y \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D)$
40	36 39	nfralw	$⊢ Ⅎ y \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D)$
41	34 35 40	nf3an	$⊢ Ⅎ y (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D))$
42	7 41	nfan	$⊢ Ⅎ y (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D)))$
43		nfv	$⊢ Ⅎ b φ$
44		nfv	$⊢ Ⅎ b D \subseteq ⋃ S$
45		nfv	$⊢ Ⅎ b F : D ⟶ ℝ$
46		nfra1	$⊢ Ⅎ b \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D)$
47	44 45 46	nf3an	$⊢ Ⅎ b (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D))$
48	43 47	nfan	$⊢ Ⅎ b (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D)))$
49	1	adantr	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D))) \to S \in SAlg$
50		simpr1	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D))) \to D \subseteq ⋃ S$
51		simpr2	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D))) \to F : D ⟶ ℝ$
52		simpr3	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D))) \to \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D)$
53	42 48 49 2 50 51 52	issmfgelem	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D))) \to F \in SMblFn (S)$
54	53	ex	$⊢ φ \to ((D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D)) \to F \in SMblFn (S))$
55	33 54	impbid	$⊢ φ \to (F \in SMblFn (S) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D)))$
56		breq1	$⊢ b = a \to (b \leq F (y) \leftrightarrow a \leq F (y))$
57	56	rabbidv	$⊢ b = a \to \{y \in D \| b \leq F (y)\} = \{y \in D \| a \leq F (y)\}$
58		fveq2	$⊢ y = x \to F (y) = F (x)$
59	58	breq2d	$⊢ y = x \to (a \leq F (y) \leftrightarrow a \leq F (x))$
60	59	cbvrabv	$⊢ \{y \in D \| a \leq F (y)\} = \{x \in D \| a \leq F (x)\}$
61	60	a1i	$⊢ b = a \to \{y \in D \| a \leq F (y)\} = \{x \in D \| a \leq F (x)\}$
62	57 61	eqtrd	$⊢ b = a \to \{y \in D \| b \leq F (y)\} = \{x \in D \| a \leq F (x)\}$
63	62	eleq1d	$⊢ b = a \to (\{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D) \leftrightarrow \{x \in D \| a \leq F (x)\} \in (S ↾_{𝑡} D))$
64	63	cbvralvw	$⊢ \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D) \leftrightarrow \forall a \in ℝ \{x \in D \| a \leq F (x)\} \in (S ↾_{𝑡} D)$
65	64	3anbi3i	$⊢ (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D)) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| a \leq F (x)\} \in (S ↾_{𝑡} D))$
66	65	a1i	$⊢ φ \to ((D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b \leq F (y)\} \in (S ↾_{𝑡} D)) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| a \leq F (x)\} \in (S ↾_{𝑡} D)))$
67	55 66	bitrd	$⊢ φ \to (F \in SMblFn (S) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| a \leq F (x)\} \in (S ↾_{𝑡} D)))$

Metamath Proof Explorer

Theorem issmfge

Proof