Proof of Theorem preimageiingt
Step | Hyp | Ref
| Expression |
1 | | preimageiingt.x |
. . . 4
⊢
Ⅎ𝑥𝜑 |
2 | | simpllr 795 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ 𝐴) |
3 | | preimageiingt.c |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ ℝ) |
4 | 3 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 ∈ ℝ) |
5 | | nnrecre 10934 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
6 | 5 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈
ℝ) |
7 | 4, 6 | resubcld 10337 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶 − (1 / 𝑛)) ∈ ℝ) |
8 | 7 | rexrd 9968 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶 − (1 / 𝑛)) ∈
ℝ*) |
9 | 8 | ad4ant14 1285 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → (𝐶 − (1 / 𝑛)) ∈
ℝ*) |
10 | 3 | rexrd 9968 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
11 | 10 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝐶 ∈
ℝ*) |
12 | | preimageiingt.b |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈
ℝ*) |
13 | 12 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝐵 ∈
ℝ*) |
14 | | nnrp 11718 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
15 | | rpreccl 11733 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℝ+
→ (1 / 𝑛) ∈
ℝ+) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ+) |
17 | 16 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈
ℝ+) |
18 | 4, 17 | ltsubrpd 11780 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶 − (1 / 𝑛)) < 𝐶) |
19 | 18 | ad4ant14 1285 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → (𝐶 − (1 / 𝑛)) < 𝐶) |
20 | | simplr 788 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝐶 ≤ 𝐵) |
21 | 9, 11, 13, 19, 20 | xrltletrd 11868 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → (𝐶 − (1 / 𝑛)) < 𝐵) |
22 | 2, 21 | jca 553 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐴 ∧ (𝐶 − (1 / 𝑛)) < 𝐵)) |
23 | | rabid 3095 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} ↔ (𝑥 ∈ 𝐴 ∧ (𝐶 − (1 / 𝑛)) < 𝐵)) |
24 | 22, 23 | sylibr 223 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵}) |
25 | 24 | ralrimiva 2949 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) → ∀𝑛 ∈ ℕ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵}) |
26 | | vex 3176 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
27 | | eliin 4461 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (𝑥 ∈ ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} ↔ ∀𝑛 ∈ ℕ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵})) |
28 | 26, 27 | ax-mp 5 |
. . . . . . 7
⊢ (𝑥 ∈ ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} ↔ ∀𝑛 ∈ ℕ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵}) |
29 | 25, 28 | sylibr 223 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) → 𝑥 ∈ ∩
𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵}) |
30 | 29 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ≤ 𝐵 → 𝑥 ∈ ∩
𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵})) |
31 | 30 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝐶 ≤ 𝐵 → 𝑥 ∈ ∩
𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵}))) |
32 | 1, 31 | ralrimi 2940 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐶 ≤ 𝐵 → 𝑥 ∈ ∩
𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵})) |
33 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑥ℕ |
34 | | nfrab1 3099 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} |
35 | 33, 34 | nfiin 4485 |
. . . 4
⊢
Ⅎ𝑥∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} |
36 | 35 | rabssf 38334 |
. . 3
⊢ ({𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵} ⊆ ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} ↔ ∀𝑥 ∈ 𝐴 (𝐶 ≤ 𝐵 → 𝑥 ∈ ∩
𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵})) |
37 | 32, 36 | sylibr 223 |
. 2
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵} ⊆ ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵}) |
38 | | nnn0 38536 |
. . . . 5
⊢ ℕ
≠ ∅ |
39 | | iinrab 4518 |
. . . . 5
⊢ (ℕ
≠ ∅ → ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} = {𝑥 ∈ 𝐴 ∣ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵}) |
40 | 38, 39 | ax-mp 5 |
. . . 4
⊢ ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} = {𝑥 ∈ 𝐴 ∣ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵} |
41 | 40 | a1i 11 |
. . 3
⊢ (𝜑 → ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} = {𝑥 ∈ 𝐴 ∣ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵}) |
42 | 8 | ad4ant13 1284 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) ∧ (𝐶 − (1 / 𝑛)) < 𝐵) → (𝐶 − (1 / 𝑛)) ∈
ℝ*) |
43 | 12 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) ∧ (𝐶 − (1 / 𝑛)) < 𝐵) → 𝐵 ∈
ℝ*) |
44 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) ∧ (𝐶 − (1 / 𝑛)) < 𝐵) → (𝐶 − (1 / 𝑛)) < 𝐵) |
45 | 42, 43, 44 | xrltled 38427 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) ∧ (𝐶 − (1 / 𝑛)) < 𝐵) → (𝐶 − (1 / 𝑛)) ≤ 𝐵) |
46 | 45 | ex 449 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) → ((𝐶 − (1 / 𝑛)) < 𝐵 → (𝐶 − (1 / 𝑛)) ≤ 𝐵)) |
47 | 46 | ralimdva 2945 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵 → ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) ≤ 𝐵)) |
48 | 47 | imp 444 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵) → ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) ≤ 𝐵) |
49 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ 𝐴) |
50 | | nfra1 2925 |
. . . . . . . . . 10
⊢
Ⅎ𝑛∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵 |
51 | 49, 50 | nfan 1816 |
. . . . . . . . 9
⊢
Ⅎ𝑛((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵) |
52 | 3 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵) → 𝐶 ∈ ℝ) |
53 | 12 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵) → 𝐵 ∈
ℝ*) |
54 | 51, 52, 53 | xrralrecnnge 38554 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵) → (𝐶 ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) ≤ 𝐵)) |
55 | 48, 54 | mpbird 246 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵) → 𝐶 ≤ 𝐵) |
56 | 55 | ex 449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵 → 𝐶 ≤ 𝐵)) |
57 | 56 | ex 449 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵 → 𝐶 ≤ 𝐵))) |
58 | 1, 57 | ralrimi 2940 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵 → 𝐶 ≤ 𝐵)) |
59 | | ss2rab 3641 |
. . . 4
⊢ ({𝑥 ∈ 𝐴 ∣ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵} ⊆ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵} ↔ ∀𝑥 ∈ 𝐴 (∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵 → 𝐶 ≤ 𝐵)) |
60 | 58, 59 | sylibr 223 |
. . 3
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵} ⊆ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) |
61 | 41, 60 | eqsstrd 3602 |
. 2
⊢ (𝜑 → ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} ⊆ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) |
62 | 37, 61 | eqssd 3585 |
1
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵} = ∩
𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵}) |