# 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$