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		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
16		rpreccl	$⊢ n \in ℝ^{+} \to \frac{1}{n} \in ℝ^{+}$
17	15 16	syl	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ^{+}$
18	17	adantl	$⊢ (φ \land n \in ℕ) \to \frac{1}{n} \in ℝ^{+}$
19	8 18	ltaddrpd	$⊢ (φ \land n \in ℕ) \to C < C + (\frac{1}{n})$
20	19	ad4ant14	$⊢ (((φ \land x \in A) \land B \leq C) \land n \in ℕ) \to C < C + (\frac{1}{n})$
21	5 7 13 14 20	xrlelttrd	$⊢ (((φ \land x \in A) \land B \leq C) \land n \in ℕ) \to B < C + (\frac{1}{n})$
22	4 21	jca	$⊢ (((φ \land x \in A) \land B \leq C) \land n \in ℕ) \to (x \in A \land B < C + (\frac{1}{n}))$
23		rabid	$⊢ x \in \{x \in A \| B < C + (\frac{1}{n})\} \leftrightarrow (x \in A \land B < C + (\frac{1}{n}))$
24	22 23	sylibr	$⊢ (((φ \land x \in A) \land B \leq C) \land n \in ℕ) \to x \in \{x \in A \| B < C + (\frac{1}{n})\}$
25	24	ralrimiva	$⊢ ((φ \land x \in A) \land B \leq C) \to \forall n \in ℕ x \in \{x \in A \| B < C + (\frac{1}{n})\}$
26		vex	$⊢ x \in V$
27		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})\})$
28	26 27	ax-mp	$⊢ 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})\}$
29	25 28	sylibr	$⊢ ((φ \land x \in A) \land B \leq C) \to x \in ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\}$
30	29	ex	$⊢ (φ \land x \in A) \to (B \leq C \to x \in ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\})$
31	30	ex	$⊢ φ \to (x \in A \to (B \leq C \to x \in ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\}))$
32	1 31	ralrimi	$⊢ φ \to \forall x \in A (B \leq C \to x \in ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\})$
33		nfcv	$⊢ \underline{Ⅎ} x ℕ$
34		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| B < C + (\frac{1}{n})\}$
35	33 34	nfiin	$⊢ \underline{Ⅎ} x ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\}$
36	35	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})\})$
37	32 36	sylibr	$⊢ φ \to \{x \in A \| B \leq C\} \subseteq ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\}$
38		nnn0	$⊢ ℕ \neq \emptyset$
39	38	a1i	$⊢ φ \to ℕ \neq \emptyset$
40		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})\}$
41	39 40	syl	$⊢ φ \to ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\} = \{x \in A \| \forall n \in ℕ B < C + (\frac{1}{n})\}$
42	2	ad2antrr	$⊢ (((φ \land x \in A) \land n \in ℕ) \land B < C + (\frac{1}{n})) \to B \in ℝ^{*}$
43	11	ad4ant13	$⊢ (((φ \land x \in A) \land n \in ℕ) \land B < C + (\frac{1}{n})) \to C + (\frac{1}{n}) \in ℝ$
44	43	rexrd	$⊢ (((φ \land x \in A) \land n \in ℕ) \land B < C + (\frac{1}{n})) \to C + (\frac{1}{n}) \in ℝ^{*}$
45		simpr	$⊢ (((φ \land x \in A) \land n \in ℕ) \land B < C + (\frac{1}{n})) \to B < C + (\frac{1}{n})$
46	42 44 45	xrltled	$⊢ (((φ \land x \in A) \land n \in ℕ) \land B < C + (\frac{1}{n})) \to B \leq C + (\frac{1}{n})$
47	46	ex	$⊢ ((φ \land x \in A) \land n \in ℕ) \to (B < C + (\frac{1}{n}) \to B \leq C + (\frac{1}{n}))$
48	47	ralimdva	$⊢ (φ \land x \in A) \to (\forall n \in ℕ B < C + (\frac{1}{n}) \to \forall n \in ℕ B \leq C + (\frac{1}{n}))$
49	48	imp	$⊢ ((φ \land x \in A) \land \forall n \in ℕ B < C + (\frac{1}{n})) \to \forall n \in ℕ B \leq C + (\frac{1}{n})$
50		nfv	$⊢ Ⅎ n (φ \land x \in A)$
51		nfra1	$⊢ Ⅎ n \forall n \in ℕ B < C + (\frac{1}{n})$
52	50 51	nfan	$⊢ Ⅎ n ((φ \land x \in A) \land \forall n \in ℕ B < C + (\frac{1}{n}))$
53	2	adantr	$⊢ ((φ \land x \in A) \land \forall n \in ℕ B < C + (\frac{1}{n})) \to B \in ℝ^{*}$
54	3	ad2antrr	$⊢ ((φ \land x \in A) \land \forall n \in ℕ B < C + (\frac{1}{n})) \to C \in ℝ$
55	52 53 54	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}))$
56	49 55	mpbird	$⊢ ((φ \land x \in A) \land \forall n \in ℕ B < C + (\frac{1}{n})) \to B \leq C$
57	56	ex	$⊢ (φ \land x \in A) \to (\forall n \in ℕ B < C + (\frac{1}{n}) \to B \leq C)$
58	57	ex	$⊢ φ \to (x \in A \to (\forall n \in ℕ B < C + (\frac{1}{n}) \to B \leq C))$
59	1 58	ralrimi	$⊢ φ \to \forall x \in A (\forall n \in ℕ B < C + (\frac{1}{n}) \to B \leq C)$
60		ss2rab	$⊢ \{x \in A \| \forall n \in ℕ B < C + (\frac{1}{n})\} \subseteq \{x \in A \| B \leq C\} \leftrightarrow \forall x \in A (\forall n \in ℕ B < C + (\frac{1}{n}) \to B \leq C)$
61	59 60	sylibr	$⊢ φ \to \{x \in A \| \forall n \in ℕ B < C + (\frac{1}{n})\} \subseteq \{x \in A \| B \leq C\}$
62	41 61	eqsstrd	$⊢ φ \to ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\} \subseteq \{x \in A \| B \leq C\}$
63	37 62	eqssd	$⊢ φ \to \{x \in A \| B \leq C\} = ⋂_{n \in ℕ} \{x \in A \| B < C + (\frac{1}{n})\}$

Metamath Proof Explorer

Theorem preimaleiinlt

Proof