Metamath Proof Explorer

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 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
16 rpreccl ⊢ ( 𝑛 ∈ ℝ+ → ( 1 / 𝑛 ) ∈ ℝ+ )
17 15 16 syl ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ+ )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ+ )
19 8 18 ltaddrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐶 < ( 𝐶 + ( 1 / 𝑛 ) ) )
20 19 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑛 ∈ ℕ ) → 𝐶 < ( 𝐶 + ( 1 / 𝑛 ) ) )
21 5 7 13 14 20 xrlelttrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑛 ∈ ℕ ) → 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) )
22 4 21 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑥 ∈ 𝐴 ∧ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) )
23 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) )
24 22 23 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
25 24 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) → ∀ 𝑛 ∈ ℕ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
26 vex ⊢ 𝑥 ∈ V
27 eliin ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ↔ ∀ 𝑛 ∈ ℕ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ) )
28 26 27 ax-mp ⊢ ( 𝑥 ∈ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ↔ ∀ 𝑛 ∈ ℕ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
29 25 28 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐵 ≤ 𝐶 ) → 𝑥 ∈ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
30 29 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ≤ 𝐶 → 𝑥 ∈ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ) )
31 30 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝐵 ≤ 𝐶 → 𝑥 ∈ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ) ) )
32 1 31 ralrimi ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≤ 𝐶 → 𝑥 ∈ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ) )
33 nfcv ⊢ Ⅎ 𝑥 ℕ
34 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) }
35 33 34 nfiin ⊢ Ⅎ 𝑥 ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) }
36 35 rabssf ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } ⊆ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≤ 𝐶 → 𝑥 ∈ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ) )
37 32 36 sylibr ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } ⊆ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
38 nnn0 ⊢ ℕ ≠ ∅
39 38 a1i ⊢ ( 𝜑 → ℕ ≠ ∅ )
40 iinrab ⊢ ( ℕ ≠ ∅ → ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
41 39 40 syl ⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )
42 2 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → 𝐵 ∈ ℝ* )
43 11 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ )
44 43 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → ( 𝐶 + ( 1 / 𝑛 ) ) ∈ ℝ* )
45 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) )
46 42 44 45 xrltled ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → 𝐵 ≤ ( 𝐶 + ( 1 / 𝑛 ) ) )
47 46 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) → 𝐵 ≤ ( 𝐶 + ( 1 / 𝑛 ) ) ) )
48 47 ralimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) → ∀ 𝑛 ∈ ℕ 𝐵 ≤ ( 𝐶 + ( 1 / 𝑛 ) ) ) )
49 48 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → ∀ 𝑛 ∈ ℕ 𝐵 ≤ ( 𝐶 + ( 1 / 𝑛 ) ) )
50 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ 𝐴 )
51 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) )
52 50 51 nfan ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) )
53 2 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → 𝐵 ∈ ℝ* )
54 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → 𝐶 ∈ ℝ )
55 52 53 54 xrralrecnnle ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → ( 𝐵 ≤ 𝐶 ↔ ∀ 𝑛 ∈ ℕ 𝐵 ≤ ( 𝐶 + ( 1 / 𝑛 ) ) ) )
56 49 55 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) ) → 𝐵 ≤ 𝐶 )
57 56 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) → 𝐵 ≤ 𝐶 ) )
58 57 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) → 𝐵 ≤ 𝐶 ) ) )
59 1 58 ralrimi ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) → 𝐵 ≤ 𝐶 ) )
60 ss2rab ⊢ ( { 𝑥 ∈ 𝐴 ∣ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } ↔ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) → 𝐵 ≤ 𝐶 ) )
61 59 60 sylibr ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑛 ∈ ℕ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } )
62 41 61 eqsstrd ⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } )
63 37 62 eqssd ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶 } = ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ 𝐵 < ( 𝐶 + ( 1 / 𝑛 ) ) } )