issmfle

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 right-closed intervals unbounded below 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 (ii) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		issmfle.s	$⊢ φ \to S \in SAlg$
2		issmfle.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	$⊢ Ⅎ b φ$
8		nfv	$⊢ Ⅎ b F \in SMblFn (S)$
9	7 8	nfan	$⊢ Ⅎ b (φ \land F \in SMblFn (S))$
10		nfv	$⊢ Ⅎ y φ$
11		nfv	$⊢ Ⅎ y F \in SMblFn (S)$
12	10 11	nfan	$⊢ Ⅎ y (φ \land F \in SMblFn (S))$
13		nfv	$⊢ Ⅎ y b \in ℝ$
14	12 13	nfan	$⊢ Ⅎ y ((φ \land F \in SMblFn (S)) \land b \in ℝ)$
15		nfv	$⊢ Ⅎ c ((φ \land F \in SMblFn (S)) \land b \in ℝ)$
16	1	uniexd	$⊢ φ \to ⋃ S \in V$
17	16	adantr	$⊢ (φ \land D \subseteq ⋃ S) \to ⋃ S \in V$
18		simpr	$⊢ (φ \land D \subseteq ⋃ S) \to D \subseteq ⋃ S$
19	17 18	ssexd	$⊢ (φ \land D \subseteq ⋃ S) \to D \in V$
20	5 19	syldan	$⊢ (φ \land F \in SMblFn (S)) \to D \in V$
21		eqid	$⊢ S ↾_{𝑡} D = S ↾_{𝑡} D$
22	3 20 21	subsalsal	$⊢ (φ \land F \in SMblFn (S)) \to S ↾_{𝑡} D \in SAlg$
23	22	adantr	$⊢ ((φ \land F \in SMblFn (S)) \land b \in ℝ) \to S ↾_{𝑡} D \in SAlg$
24	6	frexr	$⊢ (φ \land F \in SMblFn (S)) \to F : D ⟶ ℝ^{*}$
25	24	adantr	$⊢ ((φ \land F \in SMblFn (S)) \land b \in ℝ) \to F : D ⟶ ℝ^{*}$
26	25	ffvelcdmda	$⊢ (((φ \land F \in SMblFn (S)) \land b \in ℝ) \land y \in D) \to F (y) \in ℝ^{*}$
27	3	adantr	$⊢ ((φ \land F \in SMblFn (S)) \land c \in ℝ) \to S \in SAlg$
28	4	adantr	$⊢ ((φ \land F \in SMblFn (S)) \land c \in ℝ) \to F \in SMblFn (S)$
29		simpr	$⊢ ((φ \land F \in SMblFn (S)) \land c \in ℝ) \to c \in ℝ$
30	27 28 2 29	smfpreimalt	$⊢ ((φ \land F \in SMblFn (S)) \land c \in ℝ) \to \{y \in D \| F (y) < c\} \in (S ↾_{𝑡} D)$
31	30	adantlr	$⊢ (((φ \land F \in SMblFn (S)) \land b \in ℝ) \land c \in ℝ) \to \{y \in D \| F (y) < c\} \in (S ↾_{𝑡} D)$
32		simpr	$⊢ ((φ \land F \in SMblFn (S)) \land b \in ℝ) \to b \in ℝ$
33	14 15 23 26 31 32	salpreimaltle	$⊢ ((φ \land F \in SMblFn (S)) \land b \in ℝ) \to \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)$
34	33	ex	$⊢ (φ \land F \in SMblFn (S)) \to (b \in ℝ \to \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D))$
35	9 34	ralrimi	$⊢ (φ \land F \in SMblFn (S)) \to \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)$
36	5 6 35	3jca	$⊢ (φ \land F \in SMblFn (S)) \to (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D))$
37	36	ex	$⊢ φ \to (F \in SMblFn (S) \to (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)))$
38		nfv	$⊢ Ⅎ y D \subseteq ⋃ S$
39		nfv	$⊢ Ⅎ y F : D ⟶ ℝ$
40		nfcv	$⊢ \underline{Ⅎ} y ℝ$
41		nfrab1	$⊢ \underline{Ⅎ} y \{y \in D \| F (y) \leq b\}$
42		nfcv	$⊢ \underline{Ⅎ} y (S ↾_{𝑡} D)$
43	41 42	nfel	$⊢ Ⅎ y \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)$
44	40 43	nfralw	$⊢ Ⅎ y \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)$
45	38 39 44	nf3an	$⊢ Ⅎ y (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D))$
46	10 45	nfan	$⊢ Ⅎ y (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)))$
47		nfv	$⊢ Ⅎ b D \subseteq ⋃ S$
48		nfv	$⊢ Ⅎ b F : D ⟶ ℝ$
49		nfra1	$⊢ Ⅎ b \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)$
50	47 48 49	nf3an	$⊢ Ⅎ b (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D))$
51	7 50	nfan	$⊢ Ⅎ b (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)))$
52	1	adantr	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D))) \to S \in SAlg$
53		simpr1	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D))) \to D \subseteq ⋃ S$
54		simpr2	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D))) \to F : D ⟶ ℝ$
55		rspa	$⊢ (\forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D) \land b \in ℝ) \to \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)$
56	55	3ad2antl3	$⊢ ((D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)) \land b \in ℝ) \to \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)$
57	56	adantll	$⊢ ((φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D))) \land b \in ℝ) \to \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)$
58	46 51 52 2 53 54 57	issmflelem	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D))) \to F \in SMblFn (S)$
59	58	ex	$⊢ φ \to ((D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)) \to F \in SMblFn (S))$
60	37 59	impbid	$⊢ φ \to (F \in SMblFn (S) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)))$
61		breq2	$⊢ b = a \to (F (y) \leq b \leftrightarrow F (y) \leq a)$
62	61	rabbidv	$⊢ b = a \to \{y \in D \| F (y) \leq b\} = \{y \in D \| F (y) \leq a\}$
63		fveq2	$⊢ y = x \to F (y) = F (x)$
64	63	breq1d	$⊢ y = x \to (F (y) \leq a \leftrightarrow F (x) \leq a)$
65	64	cbvrabv	$⊢ \{y \in D \| F (y) \leq a\} = \{x \in D \| F (x) \leq a\}$
66	65	a1i	$⊢ b = a \to \{y \in D \| F (y) \leq a\} = \{x \in D \| F (x) \leq a\}$
67	62 66	eqtrd	$⊢ b = a \to \{y \in D \| F (y) \leq b\} = \{x \in D \| F (x) \leq a\}$
68	67	eleq1d	$⊢ b = a \to (\{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D) \leftrightarrow \{x \in D \| F (x) \leq a\} \in (S ↾_{𝑡} D))$
69	68	cbvralvw	$⊢ \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D) \leftrightarrow \forall a \in ℝ \{x \in D \| F (x) \leq a\} \in (S ↾_{𝑡} D)$
70	69	3anbi3i	$⊢ (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) \leq a\} \in (S ↾_{𝑡} D))$
71	70	a1i	$⊢ φ \to ((D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| F (y) \leq b\} \in (S ↾_{𝑡} D)) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) \leq a\} \in (S ↾_{𝑡} D)))$
72	60 71	bitrd	$⊢ φ \to (F \in SMblFn (S) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| F (x) \leq a\} \in (S ↾_{𝑡} D)))$

Metamath Proof Explorer

Theorem issmfle

Proof