Proof of Theorem preimageiingt
| Step | Hyp | Ref
| Expression |
| 1 | | preimageiingt.x |
. . . 4
⊢
Ⅎ𝑥𝜑 |
| 2 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ 𝐴) |
| 3 | | preimageiingt.c |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ ℝ) |
| 4 | 3 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 ∈ ℝ) |
| 5 | | nnrecre 12308 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
| 6 | 5 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈
ℝ) |
| 7 | 4, 6 | resubcld 11691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶 − (1 / 𝑛)) ∈ ℝ) |
| 8 | 7 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶 − (1 / 𝑛)) ∈
ℝ*) |
| 9 | 8 | ad4ant14 752 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → (𝐶 − (1 / 𝑛)) ∈
ℝ*) |
| 10 | 3 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
| 11 | 10 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝐶 ∈
ℝ*) |
| 12 | | preimageiingt.b |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈
ℝ*) |
| 13 | 12 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝐵 ∈
ℝ*) |
| 14 | | nnrp 13046 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
| 15 | | rpreccl 13061 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℝ+
→ (1 / 𝑛) ∈
ℝ+) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ+) |
| 17 | 16 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈
ℝ+) |
| 18 | 4, 17 | ltsubrpd 13109 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶 − (1 / 𝑛)) < 𝐶) |
| 19 | 18 | ad4ant14 752 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → (𝐶 − (1 / 𝑛)) < 𝐶) |
| 20 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝐶 ≤ 𝐵) |
| 21 | 9, 11, 13, 19, 20 | xrltletrd 13203 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → (𝐶 − (1 / 𝑛)) < 𝐵) |
| 22 | 2, 21 | jca 511 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐴 ∧ (𝐶 − (1 / 𝑛)) < 𝐵)) |
| 23 | | rabid 3458 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} ↔ (𝑥 ∈ 𝐴 ∧ (𝐶 − (1 / 𝑛)) < 𝐵)) |
| 24 | 22, 23 | sylibr 234 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵}) |
| 25 | 24 | ralrimiva 3146 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) → ∀𝑛 ∈ ℕ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵}) |
| 26 | | vex 3484 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
| 27 | | eliin 4996 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (𝑥 ∈ ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} ↔ ∀𝑛 ∈ ℕ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵})) |
| 28 | 26, 27 | ax-mp 5 |
. . . . . . 7
⊢ (𝑥 ∈ ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} ↔ ∀𝑛 ∈ ℕ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵}) |
| 29 | 25, 28 | sylibr 234 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝐶 ≤ 𝐵) → 𝑥 ∈ ∩
𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵}) |
| 30 | 29 | ex 412 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ≤ 𝐵 → 𝑥 ∈ ∩
𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵})) |
| 31 | 30 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝐶 ≤ 𝐵 → 𝑥 ∈ ∩
𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵}))) |
| 32 | 1, 31 | ralrimi 3257 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐶 ≤ 𝐵 → 𝑥 ∈ ∩
𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵})) |
| 33 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑥ℕ |
| 34 | | nfrab1 3457 |
. . . . 5
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} |
| 35 | 33, 34 | nfiin 5024 |
. . . 4
⊢
Ⅎ𝑥∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} |
| 36 | 35 | rabssf 45124 |
. . 3
⊢ ({𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵} ⊆ ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} ↔ ∀𝑥 ∈ 𝐴 (𝐶 ≤ 𝐵 → 𝑥 ∈ ∩
𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵})) |
| 37 | 32, 36 | sylibr 234 |
. 2
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵} ⊆ ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵}) |
| 38 | | nnn0 45389 |
. . . . 5
⊢ ℕ
≠ ∅ |
| 39 | | iinrab 5069 |
. . . . 5
⊢ (ℕ
≠ ∅ → ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} = {𝑥 ∈ 𝐴 ∣ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵}) |
| 40 | 38, 39 | ax-mp 5 |
. . . 4
⊢ ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} = {𝑥 ∈ 𝐴 ∣ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵} |
| 41 | 40 | a1i 11 |
. . 3
⊢ (𝜑 → ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} = {𝑥 ∈ 𝐴 ∣ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵}) |
| 42 | 8 | ad4ant13 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) ∧ (𝐶 − (1 / 𝑛)) < 𝐵) → (𝐶 − (1 / 𝑛)) ∈
ℝ*) |
| 43 | 12 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) ∧ (𝐶 − (1 / 𝑛)) < 𝐵) → 𝐵 ∈
ℝ*) |
| 44 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) ∧ (𝐶 − (1 / 𝑛)) < 𝐵) → (𝐶 − (1 / 𝑛)) < 𝐵) |
| 45 | 42, 43, 44 | xrltled 13192 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) ∧ (𝐶 − (1 / 𝑛)) < 𝐵) → (𝐶 − (1 / 𝑛)) ≤ 𝐵) |
| 46 | 45 | ex 412 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑛 ∈ ℕ) → ((𝐶 − (1 / 𝑛)) < 𝐵 → (𝐶 − (1 / 𝑛)) ≤ 𝐵)) |
| 47 | 46 | ralimdva 3167 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵 → ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) ≤ 𝐵)) |
| 48 | 47 | imp 406 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵) → ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) ≤ 𝐵) |
| 49 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ 𝐴) |
| 50 | | nfra1 3284 |
. . . . . . . . . 10
⊢
Ⅎ𝑛∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵 |
| 51 | 49, 50 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑛((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵) |
| 52 | 3 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵) → 𝐶 ∈ ℝ) |
| 53 | 12 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵) → 𝐵 ∈
ℝ*) |
| 54 | 51, 52, 53 | xrralrecnnge 45401 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵) → (𝐶 ≤ 𝐵 ↔ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) ≤ 𝐵)) |
| 55 | 48, 54 | mpbird 257 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵) → 𝐶 ≤ 𝐵) |
| 56 | 55 | ex 412 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵 → 𝐶 ≤ 𝐵)) |
| 57 | 56 | ex 412 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵 → 𝐶 ≤ 𝐵))) |
| 58 | 1, 57 | ralrimi 3257 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵 → 𝐶 ≤ 𝐵)) |
| 59 | | ss2rab 4071 |
. . . 4
⊢ ({𝑥 ∈ 𝐴 ∣ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵} ⊆ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵} ↔ ∀𝑥 ∈ 𝐴 (∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵 → 𝐶 ≤ 𝐵)) |
| 60 | 58, 59 | sylibr 234 |
. . 3
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ∀𝑛 ∈ ℕ (𝐶 − (1 / 𝑛)) < 𝐵} ⊆ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) |
| 61 | 41, 60 | eqsstrd 4018 |
. 2
⊢ (𝜑 → ∩ 𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵} ⊆ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) |
| 62 | 37, 61 | eqssd 4001 |
1
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵} = ∩
𝑛 ∈ ℕ {𝑥 ∈ 𝐴 ∣ (𝐶 − (1 / 𝑛)) < 𝐵}) |