Theorem 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	⊢ Ⅎ 𝑥 𝜑
	preimaleiinlt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
	preimaleiinlt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
Assertion	preimaleiinlt	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } = ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		preimaleiinlt.x	⊢ Ⅎ 𝑥 𝜑
2		preimaleiinlt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
3		preimaleiinlt.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ 𝐴 )
5	2	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑛 ∈ ℕ ) → 𝐵 ∈ ℝ* )
6	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑛 ∈ ℕ ) → 𝐶 ∈ ℝ )
7	6	rexrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑛 ∈ ℕ ) → 𝐶 ∈ ℝ* )
8	3	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐶 ∈ ℝ )
9		nnrecre	⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ )
11	8 10	readdcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ )
12	11	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ )
13	12	rexrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ* )
14		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑛 ∈ ℕ ) → 𝐵 ≤ 𝐶 )
15		nnrecrp	⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ+ )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ+ )
17	8 16	ltaddrpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐶 < ( 𝐶 + ( 1 / 𝑛 ) ) )
18	17	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑛 ∈ ℕ ) → 𝐶 < ( 𝐶 + ( 1 / 𝑛 ) ) )
19	5 7 13 14 18	xrlelttrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑛 ∈ ℕ ) → 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) )
20	4 19	rabidd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
21	20	ralrimiva	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) → ∀ 𝑛 ∈ ℕ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
22		eliin	⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ↔ ∀ 𝑛 ∈ ℕ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ) )
23	22	elv	⊢ ( 𝑥 ∈ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ↔ ∀ 𝑛 ∈ ℕ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
24	21 23	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) → 𝑥 ∈ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
25	24	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ≤ 𝐶 → 𝑥 ∈ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ) )
26	1 25	ralrimia	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≤ 𝐶 → 𝑥 ∈ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ) )
27		nfcv	⊢ Ⅎ 𝑥 ℕ
28		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) }
29	27 28	nfiin	⊢ Ⅎ 𝑥 ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) }
30	29	rabssf	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } ⊆ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≤ 𝐶 → 𝑥 ∈ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ) )
31	26 30	sylibr	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } ⊆ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
32		nnn0	⊢ ℕ ≠ ∅
33		iinrab	⊢ ( ℕ ≠ ∅ → ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
34	32 33	mp1i	⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
35	2	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → 𝐵 ∈ ℝ* )
36	11	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ )
37	36	rexrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ* )
38		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) )
39	35 37 38	xrltled	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → 𝐵 ≤ ( 𝐶 + ( 1 / 𝑛 ) ) )
40	39	ex	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) → 𝐵 ≤ ( 𝐶 + ( 1 / 𝑛 ) ) ) )
41	40	ralimdva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) → ∀ 𝑛 ∈ ℕ 𝐵 ≤ ( 𝐶 + ( 1 / 𝑛 ) ) ) )
42	41	imp	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → ∀ 𝑛 ∈ ℕ 𝐵 ≤ ( 𝐶 + ( 1 / 𝑛 ) ) )
43		nfv	⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ 𝐴 )
44		nfra1	⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) )
45	43 44	nfan	⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) )
46	2	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → 𝐵 ∈ ℝ* )
47	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → 𝐶 ∈ ℝ )
48	45 46 47	xrralrecnnle	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → ( 𝐵 ≤ 𝐶 ↔ ∀ 𝑛 ∈ ℕ 𝐵 ≤ ( 𝐶 + ( 1 / 𝑛 ) ) ) )
49	42 48	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → 𝐵 ≤ 𝐶 )
50	49	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) → 𝐵 ≤ 𝐶 ) )
51	1 50	ss2rabdf	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } )
52	34 51	eqsstrd	⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } )
53	31 52	eqssd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } = ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )