preimageiingt

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

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

Proof

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

Metamath Proof Explorer

Theorem preimageiingt

Proof