Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 preimageiingt.x ⊢ Ⅎ 𝑥 𝜑
2 preimageiingt.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
3 preimageiingt.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝑥 ∈ 𝐴 )
5 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐶 ∈ ℝ )
6 nnrecre ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ )
8 5 7 resubcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 − ( 1 / 𝑛 ) ) ∈ ℝ )
9 8 rexrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 − ( 1 / 𝑛 ) ) ∈ ℝ* )
10 9 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐶 − ( 1 / 𝑛 ) ) ∈ ℝ* )
11 3 rexrd ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
12 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝐶 ∈ ℝ* )
13 2 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝐵 ∈ ℝ* )
14 nnrp ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
15 rpreccl ⊢ ( 𝑛 ∈ ℝ+ → ( 1 / 𝑛 ) ∈ ℝ+ )
16 14 15 syl ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ+ )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ+ )
18 5 17 ltsubrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐶 )
19 18 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐶 )
20 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝐶 ≤ 𝐵 )
21 10 12 13 19 20 xrltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐶 − ( 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 iinrab ⊢ ( ℕ ≠ ∅ → ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } )
40 38 39 ax-mp ⊢ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 }
41 40 a1i ⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } )
42 9 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → ( 𝐶 − ( 1 / 𝑛 ) ) ∈ ℝ* )
43 2 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → 𝐵 ∈ ℝ* )
44 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 )
45 42 43 44 xrltled ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → ( 𝐶 − ( 1 / 𝑛 ) ) ≤ 𝐵 )
46 45 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 → ( 𝐶 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) )
47 46 ralimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 → ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) )
48 47 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) ≤ 𝐵 )
49 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ 𝐴 )
50 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵
51 49 50 nfan ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 )
52 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → 𝐶 ∈ ℝ )
53 2 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → 𝐵 ∈ ℝ* )
54 51 52 53 xrralrecnnge ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → ( 𝐶 ≤ 𝐵 ↔ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) )
55 48 54 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → 𝐶 ≤ 𝐵 )
56 55 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 → 𝐶 ≤ 𝐵 ) )
57 56 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 → 𝐶 ≤ 𝐵 ) ) )
58 1 57 ralrimi ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 → 𝐶 ≤ 𝐵 ) )
59 ss2rab ⊢ ( { 𝑥 ∈ 𝐴 ∣ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } ↔ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 → 𝐶 ≤ 𝐵 ) )
60 58 59 sylibr ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } )
61 41 60 eqsstrd ⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } )
62 37 61 eqssd ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } = ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } )