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 nnrp ⊢ n ∈ ℕ → n ∈ ℝ +
15 rpreccl ⊢ n ∈ ℝ + → 1 n ∈ ℝ +
16 14 15 syl ⊢ n ∈ ℕ → 1 n ∈ ℝ +
17 16 adantl ⊢ φ ∧ n ∈ ℕ → 1 n ∈ ℝ +
18 5 17 ltsubrpd ⊢ φ ∧ n ∈ ℕ → C − 1 n < C
19 18 ad4ant14 ⊢ φ ∧ x ∈ A ∧ C ≤ B ∧ n ∈ ℕ → C − 1 n < C
20 simplr ⊢ φ ∧ x ∈ A ∧ C ≤ B ∧ n ∈ ℕ → C ≤ B
21 10 12 13 19 20 xrltletrd ⊢ φ ∧ x ∈ A ∧ C ≤ B ∧ n ∈ ℕ → C − 1 n < B
22 4 21 jca ⊢ φ ∧ x ∈ A ∧ C ≤ B ∧ n ∈ ℕ → x ∈ A ∧ C − 1 n < B
23 rabid ⊢ x ∈ x ∈ A | C − 1 n < B ↔ x ∈ A ∧ C − 1 n < B
24 22 23 sylibr ⊢ φ ∧ x ∈ A ∧ C ≤ B ∧ n ∈ ℕ → x ∈ x ∈ A | C − 1 n < B
25 24 ralrimiva ⊢ φ ∧ x ∈ A ∧ C ≤ B → ∀ n ∈ ℕ x ∈ x ∈ A | C − 1 n < B
26 vex ⊢ x ∈ V
27 eliin ⊢ x ∈ V → x ∈ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B ↔ ∀ n ∈ ℕ x ∈ x ∈ A | C − 1 n < B
28 26 27 ax-mp ⊢ x ∈ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B ↔ ∀ n ∈ ℕ x ∈ x ∈ A | C − 1 n < B
29 25 28 sylibr ⊢ φ ∧ x ∈ A ∧ C ≤ B → x ∈ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B
30 29 ex ⊢ φ ∧ x ∈ A → C ≤ B → x ∈ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B
31 30 ex ⊢ φ → x ∈ A → C ≤ B → x ∈ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B
32 1 31 ralrimi ⊢ φ → ∀ x ∈ A C ≤ B → x ∈ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B
33 nfcv ⊢ Ⅎ _ x ℕ
34 nfrab1 ⊢ Ⅎ _ x x ∈ A | C − 1 n < B
35 33 34 nfiin ⊢ Ⅎ _ x ⋂ n ∈ ℕ x ∈ A | C − 1 n < B
36 35 rabssf ⊢ x ∈ A | C ≤ B ⊆ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B ↔ ∀ x ∈ A C ≤ B → x ∈ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B
37 32 36 sylibr ⊢ φ → x ∈ A | C ≤ B ⊆ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B
38 nnn0 ⊢ ℕ ≠ ∅
39 iinrab ⊢ ℕ ≠ ∅ → ⋂ n ∈ ℕ x ∈ A | C − 1 n < B = x ∈ A | ∀ n ∈ ℕ C − 1 n < B
40 38 39 ax-mp ⊢ ⋂ n ∈ ℕ x ∈ A | C − 1 n < B = x ∈ A | ∀ n ∈ ℕ C − 1 n < B
41 40 a1i ⊢ φ → ⋂ n ∈ ℕ x ∈ A | C − 1 n < B = x ∈ A | ∀ n ∈ ℕ C − 1 n < B
42 9 ad4ant13 ⊢ φ ∧ x ∈ A ∧ n ∈ ℕ ∧ C − 1 n < B → C − 1 n ∈ ℝ *
43 2 ad2antrr ⊢ φ ∧ x ∈ A ∧ n ∈ ℕ ∧ C − 1 n < B → B ∈ ℝ *
44 simpr ⊢ φ ∧ x ∈ A ∧ n ∈ ℕ ∧ C − 1 n < B → C − 1 n < B
45 42 43 44 xrltled ⊢ φ ∧ x ∈ A ∧ n ∈ ℕ ∧ C − 1 n < B → C − 1 n ≤ B
46 45 ex ⊢ φ ∧ x ∈ A ∧ n ∈ ℕ → C − 1 n < B → C − 1 n ≤ B
47 46 ralimdva ⊢ φ ∧ x ∈ A → ∀ n ∈ ℕ C − 1 n < B → ∀ n ∈ ℕ C − 1 n ≤ B
48 47 imp ⊢ φ ∧ x ∈ A ∧ ∀ n ∈ ℕ C − 1 n < B → ∀ n ∈ ℕ C − 1 n ≤ B
49 nfv ⊢ Ⅎ n φ ∧ x ∈ A
50 nfra1 ⊢ Ⅎ n ∀ n ∈ ℕ C − 1 n < B
51 49 50 nfan ⊢ Ⅎ n φ ∧ x ∈ A ∧ ∀ n ∈ ℕ C − 1 n < B
52 3 ad2antrr ⊢ φ ∧ x ∈ A ∧ ∀ n ∈ ℕ C − 1 n < B → C ∈ ℝ
53 2 adantr ⊢ φ ∧ x ∈ A ∧ ∀ n ∈ ℕ C − 1 n < B → B ∈ ℝ *
54 51 52 53 xrralrecnnge ⊢ φ ∧ x ∈ A ∧ ∀ n ∈ ℕ C − 1 n < B → C ≤ B ↔ ∀ n ∈ ℕ C − 1 n ≤ B
55 48 54 mpbird ⊢ φ ∧ x ∈ A ∧ ∀ n ∈ ℕ C − 1 n < B → C ≤ B
56 55 ex ⊢ φ ∧ x ∈ A → ∀ n ∈ ℕ C − 1 n < B → C ≤ B
57 56 ex ⊢ φ → x ∈ A → ∀ n ∈ ℕ C − 1 n < B → C ≤ B
58 1 57 ralrimi ⊢ φ → ∀ x ∈ A ∀ n ∈ ℕ C − 1 n < B → C ≤ B
59 ss2rab ⊢ x ∈ A | ∀ n ∈ ℕ C − 1 n < B ⊆ x ∈ A | C ≤ B ↔ ∀ x ∈ A ∀ n ∈ ℕ C − 1 n < B → C ≤ B
60 58 59 sylibr ⊢ φ → x ∈ A | ∀ n ∈ ℕ C − 1 n < B ⊆ x ∈ A | C ≤ B
61 41 60 eqsstrd ⊢ φ → ⋂ n ∈ ℕ x ∈ A | C − 1 n < B ⊆ x ∈ A | C ≤ B
62 37 61 eqssd ⊢ φ → x ∈ A | C ≤ B = ⋂ n ∈ ℕ x ∈ A | C − 1 n < B