issmfgt

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-open 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 (iii) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		issmfgt.s	$⊢ φ \to S \in SAlg$
2		issmfgt.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	3 5	restuni4	$⊢ (φ \land F \in SMblFn (S)) \to ⋃ (S ↾_{𝑡} D) = D$
11	10	eqcomd	$⊢ (φ \land F \in SMblFn (S)) \to D = ⋃ (S ↾_{𝑡} D)$
12	11	rabeqdv	$⊢ (φ \land F \in SMblFn (S)) \to \{y \in D \| b < F (y)\} = \{y \in ⋃ (S ↾_{𝑡} D) \| b < F (y)\}$
13	12	adantr	$⊢ ((φ \land F \in SMblFn (S)) \land b \in ℝ) \to \{y \in D \| b < F (y)\} = \{y \in ⋃ (S ↾_{𝑡} D) \| b < F (y)\}$
14		nfv	$⊢ Ⅎ y φ$
15		nfv	$⊢ Ⅎ y F \in SMblFn (S)$
16	14 15	nfan	$⊢ Ⅎ y (φ \land F \in SMblFn (S))$
17		nfv	$⊢ Ⅎ y b \in ℝ$
18	16 17	nfan	$⊢ Ⅎ y ((φ \land F \in SMblFn (S)) \land b \in ℝ)$
19		nfv	$⊢ Ⅎ c ((φ \land F \in SMblFn (S)) \land b \in ℝ)$
20	1	uniexd	$⊢ φ \to ⋃ S \in V$
21	20	adantr	$⊢ (φ \land D \subseteq ⋃ S) \to ⋃ S \in V$
22		simpr	$⊢ (φ \land D \subseteq ⋃ S) \to D \subseteq ⋃ S$
23	21 22	ssexd	$⊢ (φ \land D \subseteq ⋃ S) \to D \in V$
24	5 23	syldan	$⊢ (φ \land F \in SMblFn (S)) \to D \in V$
25		eqid	$⊢ S ↾_{𝑡} D = S ↾_{𝑡} D$
26	3 24 25	subsalsal	$⊢ (φ \land F \in SMblFn (S)) \to S ↾_{𝑡} D \in SAlg$
27	26	adantr	$⊢ ((φ \land F \in SMblFn (S)) \land b \in ℝ) \to S ↾_{𝑡} D \in SAlg$
28		eqid	$⊢ ⋃ (S ↾_{𝑡} D) = ⋃ (S ↾_{𝑡} D)$
29	6	adantr	$⊢ ((φ \land F \in SMblFn (S)) \land y \in ⋃ (S ↾_{𝑡} D)) \to F : D ⟶ ℝ$
30		simpr	$⊢ ((φ \land F \in SMblFn (S)) \land y \in ⋃ (S ↾_{𝑡} D)) \to y \in ⋃ (S ↾_{𝑡} D)$
31	10	adantr	$⊢ ((φ \land F \in SMblFn (S)) \land y \in ⋃ (S ↾_{𝑡} D)) \to ⋃ (S ↾_{𝑡} D) = D$
32	30 31	eleqtrd	$⊢ ((φ \land F \in SMblFn (S)) \land y \in ⋃ (S ↾_{𝑡} D)) \to y \in D$
33	29 32	ffvelrnd	$⊢ ((φ \land F \in SMblFn (S)) \land y \in ⋃ (S ↾_{𝑡} D)) \to F (y) \in ℝ$
34	33	rexrd	$⊢ ((φ \land F \in SMblFn (S)) \land y \in ⋃ (S ↾_{𝑡} D)) \to F (y) \in ℝ^{*}$
35	34	adantlr	$⊢ (((φ \land F \in SMblFn (S)) \land b \in ℝ) \land y \in ⋃ (S ↾_{𝑡} D)) \to F (y) \in ℝ^{*}$
36	3 2	issmfle	$⊢ (φ \land F \in SMblFn (S)) \to (F \in SMblFn (S) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall c \in ℝ \{y \in D \| F (y) \leq c\} \in (S ↾_{𝑡} D)))$
37	4 36	mpbid	$⊢ (φ \land F \in SMblFn (S)) \to (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall c \in ℝ \{y \in D \| F (y) \leq c\} \in (S ↾_{𝑡} D))$
38	37	simp3d	$⊢ (φ \land F \in SMblFn (S)) \to \forall c \in ℝ \{y \in D \| F (y) \leq c\} \in (S ↾_{𝑡} D)$
39	10	rabeqdv	$⊢ (φ \land F \in SMblFn (S)) \to \{y \in ⋃ (S ↾_{𝑡} D) \| F (y) \leq c\} = \{y \in D \| F (y) \leq c\}$
40	39	eleq1d	$⊢ (φ \land F \in SMblFn (S)) \to (\{y \in ⋃ (S ↾_{𝑡} D) \| F (y) \leq c\} \in (S ↾_{𝑡} D) \leftrightarrow \{y \in D \| F (y) \leq c\} \in (S ↾_{𝑡} D))$
41	40	ralbidv	$⊢ (φ \land F \in SMblFn (S)) \to (\forall c \in ℝ \{y \in ⋃ (S ↾_{𝑡} D) \| F (y) \leq c\} \in (S ↾_{𝑡} D) \leftrightarrow \forall c \in ℝ \{y \in D \| F (y) \leq c\} \in (S ↾_{𝑡} D))$
42	38 41	mpbird	$⊢ (φ \land F \in SMblFn (S)) \to \forall c \in ℝ \{y \in ⋃ (S ↾_{𝑡} D) \| F (y) \leq c\} \in (S ↾_{𝑡} D)$
43	42	adantr	$⊢ ((φ \land F \in SMblFn (S)) \land c \in ℝ) \to \forall c \in ℝ \{y \in ⋃ (S ↾_{𝑡} D) \| F (y) \leq c\} \in (S ↾_{𝑡} D)$
44		simpr	$⊢ ((φ \land F \in SMblFn (S)) \land c \in ℝ) \to c \in ℝ$
45		rspa	$⊢ (\forall c \in ℝ \{y \in ⋃ (S ↾_{𝑡} D) \| F (y) \leq c\} \in (S ↾_{𝑡} D) \land c \in ℝ) \to \{y \in ⋃ (S ↾_{𝑡} D) \| F (y) \leq c\} \in (S ↾_{𝑡} D)$
46	43 44 45	syl2anc	$⊢ ((φ \land F \in SMblFn (S)) \land c \in ℝ) \to \{y \in ⋃ (S ↾_{𝑡} D) \| F (y) \leq c\} \in (S ↾_{𝑡} D)$
47	46	adantlr	$⊢ (((φ \land F \in SMblFn (S)) \land b \in ℝ) \land c \in ℝ) \to \{y \in ⋃ (S ↾_{𝑡} D) \| F (y) \leq c\} \in (S ↾_{𝑡} D)$
48		simpr	$⊢ ((φ \land F \in SMblFn (S)) \land b \in ℝ) \to b \in ℝ$
49	18 19 27 28 35 47 48	salpreimalegt	$⊢ ((φ \land F \in SMblFn (S)) \land b \in ℝ) \to \{y \in ⋃ (S ↾_{𝑡} D) \| b < F (y)\} \in (S ↾_{𝑡} D)$
50	13 49	eqeltrd	$⊢ ((φ \land F \in SMblFn (S)) \land b \in ℝ) \to \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D)$
51	50	ex	$⊢ (φ \land F \in SMblFn (S)) \to (b \in ℝ \to \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D))$
52	9 51	ralrimi	$⊢ (φ \land F \in SMblFn (S)) \to \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D)$
53	5 6 52	3jca	$⊢ (φ \land F \in SMblFn (S)) \to (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D))$
54	53	ex	$⊢ φ \to (F \in SMblFn (S) \to (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D)))$
55		nfv	$⊢ Ⅎ y D \subseteq ⋃ S$
56		nfv	$⊢ Ⅎ y F : D ⟶ ℝ$
57		nfcv	$⊢ \underline{Ⅎ} y ℝ$
58		nfrab1	$⊢ \underline{Ⅎ} y \{y \in D \| b < F (y)\}$
59		nfcv	$⊢ \underline{Ⅎ} y (S ↾_{𝑡} D)$
60	58 59	nfel	$⊢ Ⅎ y \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D)$
61	57 60	nfralw	$⊢ Ⅎ y \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D)$
62	55 56 61	nf3an	$⊢ Ⅎ y (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D))$
63	14 62	nfan	$⊢ Ⅎ y (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D)))$
64		nfv	$⊢ Ⅎ b D \subseteq ⋃ S$
65		nfv	$⊢ Ⅎ b F : D ⟶ ℝ$
66		nfra1	$⊢ Ⅎ b \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D)$
67	64 65 66	nf3an	$⊢ Ⅎ b (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D))$
68	7 67	nfan	$⊢ Ⅎ b (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D)))$
69	1	adantr	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D))) \to S \in SAlg$
70		simpr1	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D))) \to D \subseteq ⋃ S$
71		simpr2	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D))) \to F : D ⟶ ℝ$
72		simpr3	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D))) \to \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D)$
73	63 68 69 2 70 71 72	issmfgtlem	$⊢ (φ \land (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D))) \to F \in SMblFn (S)$
74	73	ex	$⊢ φ \to ((D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D)) \to F \in SMblFn (S))$
75	54 74	impbid	$⊢ φ \to (F \in SMblFn (S) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D)))$
76		breq1	$⊢ b = a \to (b < F (y) \leftrightarrow a < F (y))$
77	76	rabbidv	$⊢ b = a \to \{y \in D \| b < F (y)\} = \{y \in D \| a < F (y)\}$
78		fveq2	$⊢ y = x \to F (y) = F (x)$
79	78	breq2d	$⊢ y = x \to (a < F (y) \leftrightarrow a < F (x))$
80	79	cbvrabv	$⊢ \{y \in D \| a < F (y)\} = \{x \in D \| a < F (x)\}$
81	80	a1i	$⊢ b = a \to \{y \in D \| a < F (y)\} = \{x \in D \| a < F (x)\}$
82	77 81	eqtrd	$⊢ b = a \to \{y \in D \| b < F (y)\} = \{x \in D \| a < F (x)\}$
83	82	eleq1d	$⊢ b = a \to (\{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D) \leftrightarrow \{x \in D \| a < F (x)\} \in (S ↾_{𝑡} D))$
84	83	cbvralvw	$⊢ \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D) \leftrightarrow \forall a \in ℝ \{x \in D \| a < F (x)\} \in (S ↾_{𝑡} D)$
85	84	3anbi3i	$⊢ (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D)) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| a < F (x)\} \in (S ↾_{𝑡} D))$
86	85	a1i	$⊢ φ \to ((D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall b \in ℝ \{y \in D \| b < F (y)\} \in (S ↾_{𝑡} D)) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| a < F (x)\} \in (S ↾_{𝑡} D)))$
87	75 86	bitrd	$⊢ φ \to (F \in SMblFn (S) \leftrightarrow (D \subseteq ⋃ S \land F : D ⟶ ℝ \land \forall a \in ℝ \{x \in D \| a < F (x)\} \in (S ↾_{𝑡} D)))$

Metamath Proof Explorer

Theorem issmfgt

Proof