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 nnrecrp ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ+ )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ+ )
16 5 15 ltsubrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐶 )
17 16 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐶 )
18 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝐶 ≤ 𝐵 )
19 10 12 13 17 18 xrltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐶 ≤ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐶 − ( 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 ax-mp ⊢ ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 }
35 9 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → ( 𝐶 − ( 1 / 𝑛 ) ) ∈ ℝ* )
36 2 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → 𝐵 ∈ ℝ* )
37 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 )
38 35 36 37 xrltled ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → ( 𝐶 − ( 1 / 𝑛 ) ) ≤ 𝐵 )
39 38 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 → ( 𝐶 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) )
40 39 ralimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 → ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) )
41 40 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) ≤ 𝐵 )
42 nfv ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑥 ∈ 𝐴 )
43 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵
44 42 43 nfan ⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 )
45 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → 𝐶 ∈ ℝ )
46 2 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → 𝐵 ∈ ℝ* )
47 44 45 46 xrralrecnnge ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → ( 𝐶 ≤ 𝐵 ↔ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) ≤ 𝐵 ) )
48 41 47 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 ) → 𝐶 ≤ 𝐵 )
49 48 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 → 𝐶 ≤ 𝐵 ) )
50 1 49 ss2rabdf ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑛 ∈ ℕ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } )
51 34 50 eqsstrid ⊢ ( 𝜑 → ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } )
52 31 51 eqssd ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵 } = ∩ 𝑛 ∈ ℕ { 𝑥 ∈ 𝐴 ∣ ( 𝐶 − ( 1 / 𝑛 ) ) < 𝐵 } )