preimaleiinlt

Description: A preimage of a left-open, right-closed, unbounded below interval, expressed as an indexed intersection of preimages of open, unbound below intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	preimaleiinlt.x	$⊢ Ⅎ x φ$
	preimaleiinlt.b	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
	preimaleiinlt.c	$⊢ φ \to C \in ℝ$
Assertion	preimaleiinlt	$⊢ φ \to \{x \in A \| B \leq C\} = ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\}$

Proof

Step	Hyp	Ref	Expression
1		preimaleiinlt.x	$⊢ Ⅎ x φ$
2		preimaleiinlt.b	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
3		preimaleiinlt.c	$⊢ φ \to C \in ℝ$
4		simpllr	$⊢ (((φ \land x \in A) \land B \leq C) \land n \in ℕ) \to x \in A$
5	2	ad2antrr	$⊢ (((φ \land x \in A) \land B \leq C) \land n \in ℕ) \to B \in ℝ^{*}$
6	3	ad3antrrr	$⊢ (((φ \land x \in A) \land B \leq C) \land n \in ℕ) \to C \in ℝ$
7	6	rexrd	$⊢ (((φ \land x \in A) \land B \leq C) \land n \in ℕ) \to C \in ℝ^{*}$
8	3	adantr	$⊢ (φ \land n \in ℕ) \to C \in ℝ$
9		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
10	9	adantl	$⊢ (φ \land n \in ℕ) \to \frac{1}{n} \in ℝ$
11	8 10	readdcld	$⊢ (φ \land n \in ℕ) \to C + (\frac{1}{n}) \in ℝ$
12	11	ad4ant14	$⊢ (((φ \land x \in A) \land B \leq C) \land n \in ℕ) \to C + (\frac{1}{n}) \in ℝ$
13	12	rexrd	$⊢ (((φ \land x \in A) \land B \leq C) \land n \in ℕ) \to C + (\frac{1}{n}) \in ℝ^{*}$
14		simplr	$⊢ (((φ \land x \in A) \land B \leq C) \land n \in ℕ) \to B \leq C$
15		nnrecrp	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ^{+}$
16	15	adantl	$⊢ (φ \land n \in ℕ) \to \frac{1}{n} \in ℝ^{+}$
17	8 16	ltaddrpd	$⊢ (φ \land n \in ℕ) \to C < C + (\frac{1}{n})$
18	17	ad4ant14	$⊢ (((φ \land x \in A) \land B \leq C) \land n \in ℕ) \to C < C + (\frac{1}{n})$
19	5 7 13 14 18	xrlelttrd	$⊢ (((φ \land x \in A) \land B \leq C) \land n \in ℕ) \to B < C + (\frac{1}{n})$
20	4 19	rabidd	$⊢ (((φ \land x \in A) \land B \leq C) \land n \in ℕ) \to x \in \{x \in A \| B < C + (\frac{1}{n})\}$
21	20	ralrimiva	$⊢ ((φ \land x \in A) \land B \leq C) \to \forall n \in ℕ x \in \{x \in A \| B < C + (\frac{1}{n})\}$
22		eliin	$⊢ x \in V \to (x \in ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\} \leftrightarrow \forall n \in ℕ x \in \{x \in A \| B < C + (\frac{1}{n})\})$
23	22	elv	$⊢ x \in ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\} \leftrightarrow \forall n \in ℕ x \in \{x \in A \| B < C + (\frac{1}{n})\}$
24	21 23	sylibr	$⊢ ((φ \land x \in A) \land B \leq C) \to x \in ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\}$
25	24	ex	$⊢ (φ \land x \in A) \to (B \leq C \to x \in ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\})$
26	1 25	ralrimia	$⊢ φ \to \forall x \in A (B \leq C \to x \in ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\})$
27		nfcv	$⊢ \underline{Ⅎ} x ℕ$
28		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| B < C + (\frac{1}{n})\}$
29	27 28	nfiin	$⊢ \underline{Ⅎ} x ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\}$
30	29	rabssf	$⊢ \{x \in A \| B \leq C\} \subseteq ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\} \leftrightarrow \forall x \in A (B \leq C \to x \in ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\})$
31	26 30	sylibr	$⊢ φ \to \{x \in A \| B \leq C\} \subseteq ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\}$
32		nnn0	$⊢ ℕ \neq \emptyset$
33		iinrab	$⊢ ℕ \neq \emptyset \to ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\} = \{x \in A \| \forall n \in ℕ B < C + (\frac{1}{n})\}$
34	32 33	mp1i	$⊢ φ \to ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\} = \{x \in A \| \forall n \in ℕ B < C + (\frac{1}{n})\}$
35	2	ad2antrr	$⊢ (((φ \land x \in A) \land n \in ℕ) \land B < C + (\frac{1}{n})) \to B \in ℝ^{*}$
36	11	ad4ant13	$⊢ (((φ \land x \in A) \land n \in ℕ) \land B < C + (\frac{1}{n})) \to C + (\frac{1}{n}) \in ℝ$
37	36	rexrd	$⊢ (((φ \land x \in A) \land n \in ℕ) \land B < C + (\frac{1}{n})) \to C + (\frac{1}{n}) \in ℝ^{*}$
38		simpr	$⊢ (((φ \land x \in A) \land n \in ℕ) \land B < C + (\frac{1}{n})) \to B < C + (\frac{1}{n})$
39	35 37 38	xrltled	$⊢ (((φ \land x \in A) \land n \in ℕ) \land B < C + (\frac{1}{n})) \to B \leq C + (\frac{1}{n})$
40	39	ex	$⊢ ((φ \land x \in A) \land n \in ℕ) \to (B < C + (\frac{1}{n}) \to B \leq C + (\frac{1}{n}))$
41	40	ralimdva	$⊢ (φ \land x \in A) \to (\forall n \in ℕ B < C + (\frac{1}{n}) \to \forall n \in ℕ B \leq C + (\frac{1}{n}))$
42	41	imp	$⊢ ((φ \land x \in A) \land \forall n \in ℕ B < C + (\frac{1}{n})) \to \forall n \in ℕ B \leq C + (\frac{1}{n})$
43		nfv	$⊢ Ⅎ n (φ \land x \in A)$
44		nfra1	$⊢ Ⅎ n \forall n \in ℕ B < C + (\frac{1}{n})$
45	43 44	nfan	$⊢ Ⅎ n ((φ \land x \in A) \land \forall n \in ℕ B < C + (\frac{1}{n}))$
46	2	adantr	$⊢ ((φ \land x \in A) \land \forall n \in ℕ B < C + (\frac{1}{n})) \to B \in ℝ^{*}$
47	3	ad2antrr	$⊢ ((φ \land x \in A) \land \forall n \in ℕ B < C + (\frac{1}{n})) \to C \in ℝ$
48	45 46 47	xrralrecnnle	$⊢ ((φ \land x \in A) \land \forall n \in ℕ B < C + (\frac{1}{n})) \to (B \leq C \leftrightarrow \forall n \in ℕ B \leq C + (\frac{1}{n}))$
49	42 48	mpbird	$⊢ ((φ \land x \in A) \land \forall n \in ℕ B < C + (\frac{1}{n})) \to B \leq C$
50	49	ex	$⊢ (φ \land x \in A) \to (\forall n \in ℕ B < C + (\frac{1}{n}) \to B \leq C)$
51	1 50	ss2rabdf	$⊢ φ \to \{x \in A \| \forall n \in ℕ B < C + (\frac{1}{n})\} \subseteq \{x \in A \| B \leq C\}$
52	34 51	eqsstrd	$⊢ φ \to ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\} \subseteq \{x \in A \| B \leq C\}$
53	31 52	eqssd	$⊢ φ \to \{x \in A \| B \leq C\} = ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\}$

Metamath Proof Explorer

Theorem preimaleiinlt

Proof