Proof of Theorem rexuz3
| Step | Hyp | Ref
| Expression |
| 1 | | ralel 3064 |
. . . 4
⊢
∀𝑘 ∈
𝑍 𝑘 ∈ 𝑍 |
| 2 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑗 = 𝑀 → (ℤ≥‘𝑗) =
(ℤ≥‘𝑀)) |
| 3 | | rexuz3.1 |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 4 | 2, 3 | eqtr4di 2795 |
. . . . . 6
⊢ (𝑗 = 𝑀 → (ℤ≥‘𝑗) = 𝑍) |
| 5 | 4 | raleqdv 3326 |
. . . . 5
⊢ (𝑗 = 𝑀 → (∀𝑘 ∈ (ℤ≥‘𝑗)𝑘 ∈ 𝑍 ↔ ∀𝑘 ∈ 𝑍 𝑘 ∈ 𝑍)) |
| 6 | 5 | rspcev 3622 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧
∀𝑘 ∈ 𝑍 𝑘 ∈ 𝑍) → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑘 ∈ 𝑍) |
| 7 | 1, 6 | mpan2 691 |
. . 3
⊢ (𝑀 ∈ ℤ →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)𝑘 ∈ 𝑍) |
| 8 | 7 | biantrurd 532 |
. 2
⊢ (𝑀 ∈ ℤ →
(∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)𝜑 ↔ (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑘 ∈ 𝑍 ∧ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑))) |
| 9 | 3 | uztrn2 12897 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
| 10 | 9 | a1d 25 |
. . . . . . . . 9
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝜑 → 𝑘 ∈ 𝑍)) |
| 11 | 10 | ancrd 551 |
. . . . . . . 8
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝜑 → (𝑘 ∈ 𝑍 ∧ 𝜑))) |
| 12 | 11 | ralimdva 3167 |
. . . . . . 7
⊢ (𝑗 ∈ 𝑍 → (∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ 𝑍 ∧ 𝜑))) |
| 13 | | eluzelz 12888 |
. . . . . . . 8
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ ℤ) |
| 14 | 13, 3 | eleq2s 2859 |
. . . . . . 7
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ) |
| 15 | 12, 14 | jctild 525 |
. . . . . 6
⊢ (𝑗 ∈ 𝑍 → (∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 → (𝑗 ∈ ℤ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ 𝑍 ∧ 𝜑)))) |
| 16 | 15 | imp 406 |
. . . . 5
⊢ ((𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑) → (𝑗 ∈ ℤ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ 𝑍 ∧ 𝜑))) |
| 17 | | uzid 12893 |
. . . . . . 7
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
| 18 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑘 ∈ 𝑍 ∧ 𝜑) → 𝑘 ∈ 𝑍) |
| 19 | 18 | ralimi 3083 |
. . . . . . 7
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ 𝑍 ∧ 𝜑) → ∀𝑘 ∈ (ℤ≥‘𝑗)𝑘 ∈ 𝑍) |
| 20 | | eleq1w 2824 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍)) |
| 21 | 20 | rspcva 3620 |
. . . . . . 7
⊢ ((𝑗 ∈
(ℤ≥‘𝑗) ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑘 ∈ 𝑍) → 𝑗 ∈ 𝑍) |
| 22 | 17, 19, 21 | syl2an 596 |
. . . . . 6
⊢ ((𝑗 ∈ ℤ ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ 𝑍 ∧ 𝜑)) → 𝑗 ∈ 𝑍) |
| 23 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑘 ∈ 𝑍 ∧ 𝜑) → 𝜑) |
| 24 | 23 | ralimi 3083 |
. . . . . . 7
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ 𝑍 ∧ 𝜑) → ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑) |
| 25 | 24 | adantl 481 |
. . . . . 6
⊢ ((𝑗 ∈ ℤ ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ 𝑍 ∧ 𝜑)) → ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑) |
| 26 | 22, 25 | jca 511 |
. . . . 5
⊢ ((𝑗 ∈ ℤ ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ 𝑍 ∧ 𝜑)) → (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑)) |
| 27 | 16, 26 | impbii 209 |
. . . 4
⊢ ((𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑) ↔ (𝑗 ∈ ℤ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ 𝑍 ∧ 𝜑))) |
| 28 | 27 | rexbii2 3090 |
. . 3
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)𝜑 ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ 𝑍 ∧ 𝜑)) |
| 29 | | rexanuz 15384 |
. . 3
⊢
(∃𝑗 ∈
ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ 𝑍 ∧ 𝜑) ↔ (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑘 ∈ 𝑍 ∧ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑)) |
| 30 | 28, 29 | bitr2i 276 |
. 2
⊢
((∃𝑗 ∈
ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)𝑘 ∈ 𝑍 ∧ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑) ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑) |
| 31 | 8, 30 | bitr2di 288 |
1
⊢ (𝑀 ∈ ℤ →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑 ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)𝜑)) |