salpreimaltle

Description: If all the preimages of right-open, unbounded below intervals, belong to a sigma-algebra, then all the preimages of right-closed, unbounded below intervals, belong to the sigma-algebra. (i) implies (ii) in Proposition 121B of Fremlin1 p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	salpreimaltle.x	$⊢ Ⅎ x φ$
	salpreimaltle.a	$⊢ Ⅎ a φ$
	salpreimaltle.s	$⊢ φ \to S \in SAlg$
	salpreimaltle.b	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
	salpreimaltle.p	$⊢ (φ \land a \in ℝ) \to \{x \in A \| B < a\} \in S$
	salpreimaltle.c	$⊢ φ \to C \in ℝ$
Assertion	salpreimaltle	$⊢ φ \to \{x \in A \| B \leq C\} \in S$

Proof

Step	Hyp	Ref	Expression
1		salpreimaltle.x	$⊢ Ⅎ x φ$
2		salpreimaltle.a	$⊢ Ⅎ a φ$
3		salpreimaltle.s	$⊢ φ \to S \in SAlg$
4		salpreimaltle.b	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
5		salpreimaltle.p	$⊢ (φ \land a \in ℝ) \to \{x \in A \| B < a\} \in S$
6		salpreimaltle.c	$⊢ φ \to C \in ℝ$
7	1 4 6	preimaleiinlt	$⊢ φ \to \{x \in A \| B \leq C\} = ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\}$
8		nnct	$⊢ ℕ ≼ ω$
9	8	a1i	$⊢ φ \to ℕ ≼ ω$
10		nnn0	$⊢ ℕ \neq \emptyset$
11	10	a1i	$⊢ φ \to ℕ \neq \emptyset$
12		simpl	$⊢ (φ \land n \in ℕ) \to φ$
13		simpl	$⊢ (C \in ℝ \land n \in ℕ) \to C \in ℝ$
14		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
15	14	adantl	$⊢ (C \in ℝ \land n \in ℕ) \to \frac{1}{n} \in ℝ$
16	13 15	readdcld	$⊢ (C \in ℝ \land n \in ℕ) \to C + (\frac{1}{n}) \in ℝ$
17	6 16	sylan	$⊢ (φ \land n \in ℕ) \to C + (\frac{1}{n}) \in ℝ$
18		nfv	$⊢ Ⅎ a C + (\frac{1}{n}) \in ℝ$
19	2 18	nfan	$⊢ Ⅎ a (φ \land C + (\frac{1}{n}) \in ℝ)$
20		nfv	$⊢ Ⅎ a \{x \in A \| B < C + (\frac{1}{n})\} \in S$
21	19 20	nfim	$⊢ Ⅎ a ((φ \land C + (\frac{1}{n}) \in ℝ) \to \{x \in A \| B < C + (\frac{1}{n})\} \in S)$
22		ovex	$⊢ C + (\frac{1}{n}) \in V$
23		eleq1	$⊢ a = C + (\frac{1}{n}) \to (a \in ℝ \leftrightarrow C + (\frac{1}{n}) \in ℝ)$
24	23	anbi2d	$⊢ a = C + (\frac{1}{n}) \to ((φ \land a \in ℝ) \leftrightarrow (φ \land C + (\frac{1}{n}) \in ℝ))$
25		breq2	$⊢ a = C + (\frac{1}{n}) \to (B < a \leftrightarrow B < C + (\frac{1}{n}))$
26	25	rabbidv	$⊢ a = C + (\frac{1}{n}) \to \{x \in A \| B < a\} = \{x \in A \| B < C + (\frac{1}{n})\}$
27	26	eleq1d	$⊢ a = C + (\frac{1}{n}) \to (\{x \in A \| B < a\} \in S \leftrightarrow \{x \in A \| B < C + (\frac{1}{n})\} \in S)$
28	24 27	imbi12d	$⊢ a = C + (\frac{1}{n}) \to (((φ \land a \in ℝ) \to \{x \in A \| B < a\} \in S) \leftrightarrow ((φ \land C + (\frac{1}{n}) \in ℝ) \to \{x \in A \| B < C + (\frac{1}{n})\} \in S))$
29	21 22 28 5	vtoclf	$⊢ (φ \land C + (\frac{1}{n}) \in ℝ) \to \{x \in A \| B < C + (\frac{1}{n})\} \in S$
30	12 17 29	syl2anc	$⊢ (φ \land n \in ℕ) \to \{x \in A \| B < C + (\frac{1}{n})\} \in S$
31	3 9 11 30	saliincl	$⊢ φ \to ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\} \in S$
32	7 31	eqeltrd	$⊢ φ \to \{x \in A \| B \leq C\} \in S$

Metamath Proof Explorer

Theorem salpreimaltle

Proof