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 ⊢ Ⅎ x φ
preimageiingt.b ⊢ φ ∧ x ∈ A → B ∈ ℝ *
preimageiingt.c ⊢ φ → C ∈ ℝ
Assertion preimageiingt ⊢ φ → x ∈ A | C ≤ B = ⋂ n ∈ ℕ x ∈ A | C − 1 n < B

Proof

Step Hyp Ref Expression
1 preimageiingt.x ⊢ Ⅎ x φ
2 preimageiingt.b ⊢ φ ∧ x ∈ A → B ∈ ℝ *
3 preimageiingt.c ⊢ φ → C ∈ ℝ
4 simpllr ⊢ φ ∧ x ∈ A ∧ C ≤ B ∧ n ∈ ℕ → x ∈ A
5 3 adantr ⊢ φ ∧ n ∈ ℕ → C ∈ ℝ
6 nnrecre ⊢ n ∈ ℕ → 1 n ∈ ℝ
7 6 adantl ⊢ φ ∧ n ∈ ℕ → 1 n ∈ ℝ
8 5 7 resubcld ⊢ φ ∧ n ∈ ℕ → C − 1 n ∈ ℝ
9 8 rexrd ⊢ φ ∧ n ∈ ℕ → C − 1 n ∈ ℝ *
10 9 ad4ant14 ⊢ φ ∧ x ∈ A ∧ C ≤ B ∧ n ∈ ℕ → C − 1 n ∈ ℝ *
11 3 rexrd ⊢ φ → C ∈ ℝ *
12 11 ad3antrrr ⊢ φ ∧ x ∈ A ∧ C ≤ B ∧ n ∈ ℕ → C ∈ ℝ *
13 2 ad2antrr ⊢ φ ∧ x ∈ A ∧ C ≤ B ∧ n ∈ ℕ → B ∈ ℝ *
14 nnrecrp ⊢ n ∈ ℕ → 1 n ∈ ℝ +
15 14 adantl ⊢ φ ∧ n ∈ ℕ → 1 n ∈ ℝ +
16 5 15 ltsubrpd ⊢ φ ∧ n ∈ ℕ → C − 1 n < C
17 16 ad4ant14 ⊢ φ ∧ x ∈ A ∧ C ≤ B ∧ n ∈ ℕ → C − 1 n < C
18 simplr ⊢ φ ∧ x ∈ A ∧ C ≤ B ∧ n ∈ ℕ → C ≤ B
19 10 12 13 17 18 xrltletrd ⊢ φ ∧ x ∈ A ∧ C ≤ B ∧ n ∈ ℕ → C − 1 n < B
20 4 19 rabidd ⊢ φ ∧ x ∈ A ∧ C ≤ B ∧ n ∈ ℕ → x ∈ x ∈ A | C − 1 n < B
21 20 ralrimiva ⊢ φ ∧ x ∈ A ∧ C ≤ B → ∀ n ∈ ℕ x ∈ x ∈ A | C − 1 n < B
22 eliin ⊢ x ∈ V → x ∈ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B ↔ ∀ n ∈ ℕ x ∈ x ∈ A | C − 1 n < B
23 22 elv ⊢ x ∈ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B ↔ ∀ n ∈ ℕ x ∈ x ∈ A | C − 1 n < B
24 21 23 sylibr ⊢ φ ∧ x ∈ A ∧ C ≤ B → x ∈ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B
25 24 ex ⊢ φ ∧ x ∈ A → C ≤ B → x ∈ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B
26 1 25 ralrimia ⊢ φ → ∀ x ∈ A C ≤ B → x ∈ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B
27 nfcv ⊢ Ⅎ _ x ℕ
28 nfrab1 ⊢ Ⅎ _ x x ∈ A | C − 1 n < B
29 27 28 nfiin ⊢ Ⅎ _ x ⋂ n ∈ ℕ x ∈ A | C − 1 n < B
30 29 rabssf ⊢ x ∈ A | C ≤ B ⊆ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B ↔ ∀ x ∈ A C ≤ B → x ∈ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B
31 26 30 sylibr ⊢ φ → x ∈ A | C ≤ B ⊆ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B
32 nnn0 ⊢ ℕ ≠ ∅
33 iinrab ⊢ ℕ ≠ ∅ → ⋂ n ∈ ℕ x ∈ A | C − 1 n < B = x ∈ A | ∀ n ∈ ℕ C − 1 n < B
34 32 33 ax-mp ⊢ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B = x ∈ A | ∀ n ∈ ℕ C − 1 n < B
35 9 ad4ant13 ⊢ φ ∧ x ∈ A ∧ n ∈ ℕ ∧ C − 1 n < B → C − 1 n ∈ ℝ *
36 2 ad2antrr ⊢ φ ∧ x ∈ A ∧ n ∈ ℕ ∧ C − 1 n < B → B ∈ ℝ *
37 simpr ⊢ φ ∧ x ∈ A ∧ n ∈ ℕ ∧ C − 1 n < B → C − 1 n < B
38 35 36 37 xrltled ⊢ φ ∧ x ∈ A ∧ n ∈ ℕ ∧ C − 1 n < B → C − 1 n ≤ B
39 38 ex ⊢ φ ∧ x ∈ A ∧ n ∈ ℕ → C − 1 n < B → C − 1 n ≤ B
40 39 ralimdva ⊢ φ ∧ x ∈ A → ∀ n ∈ ℕ C − 1 n < B → ∀ n ∈ ℕ C − 1 n ≤ B
41 40 imp ⊢ φ ∧ x ∈ A ∧ ∀ n ∈ ℕ C − 1 n < B → ∀ n ∈ ℕ C − 1 n ≤ B
42 nfv ⊢ Ⅎ n φ ∧ x ∈ A
43 nfra1 ⊢ Ⅎ n ∀ n ∈ ℕ C − 1 n < B
44 42 43 nfan ⊢ Ⅎ n φ ∧ x ∈ A ∧ ∀ n ∈ ℕ C − 1 n < B
45 3 ad2antrr ⊢ φ ∧ x ∈ A ∧ ∀ n ∈ ℕ C − 1 n < B → C ∈ ℝ
46 2 adantr ⊢ φ ∧ x ∈ A ∧ ∀ n ∈ ℕ C − 1 n < B → B ∈ ℝ *
47 44 45 46 xrralrecnnge ⊢ φ ∧ x ∈ A ∧ ∀ n ∈ ℕ C − 1 n < B → C ≤ B ↔ ∀ n ∈ ℕ C − 1 n ≤ B
48 41 47 mpbird ⊢ φ ∧ x ∈ A ∧ ∀ n ∈ ℕ C − 1 n < B → C ≤ B
49 48 ex ⊢ φ ∧ x ∈ A → ∀ n ∈ ℕ C − 1 n < B → C ≤ B
50 1 49 ss2rabdf ⊢ φ → x ∈ A | ∀ n ∈ ℕ C − 1 n < B ⊆ x ∈ A | C ≤ B
51 34 50 eqsstrid ⊢ φ → ⋂ n ∈ ℕ x ∈ A | C − 1 n < B ⊆ x ∈ A | C ≤ B
52 31 51 eqssd ⊢ φ → x ∈ A | C ≤ B = ⋂ n ∈ ℕ x ∈ A | C − 1 n < B