| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nn0min.4 | . . . . 5
⊢ (𝜑 → ∃𝑛 ∈ ℕ 𝜓) | 
| 2 | 1 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ∃𝑛 ∈ ℕ 𝜓) | 
| 3 |  | nfv 1914 | . . . . . . . . . 10
⊢
Ⅎ𝑚𝜑 | 
| 4 |  | nfra1 3284 | . . . . . . . . . 10
⊢
Ⅎ𝑚∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏) | 
| 5 | 3, 4 | nfan 1899 | . . . . . . . . 9
⊢
Ⅎ𝑚(𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) | 
| 6 |  | nfv 1914 | . . . . . . . . 9
⊢
Ⅎ𝑚 ¬
[𝑘 / 𝑛]𝜓 | 
| 7 | 5, 6 | nfim 1896 | . . . . . . . 8
⊢
Ⅎ𝑚((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ¬ [𝑘 / 𝑛]𝜓) | 
| 8 |  | dfsbcq2 3791 | . . . . . . . . . 10
⊢ (𝑘 = 1 → ([𝑘 / 𝑛]𝜓 ↔ [1 / 𝑛]𝜓)) | 
| 9 | 8 | notbid 318 | . . . . . . . . 9
⊢ (𝑘 = 1 → (¬ [𝑘 / 𝑛]𝜓 ↔ ¬ [1 / 𝑛]𝜓)) | 
| 10 | 9 | imbi2d 340 | . . . . . . . 8
⊢ (𝑘 = 1 → (((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ¬ [𝑘 / 𝑛]𝜓) ↔ ((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ¬ [1 / 𝑛]𝜓))) | 
| 11 |  | nfv 1914 | . . . . . . . . . . 11
⊢
Ⅎ𝑛𝜃 | 
| 12 |  | nn0min.1 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝜓 ↔ 𝜃)) | 
| 13 | 11, 12 | sbhypf 3544 | . . . . . . . . . 10
⊢ (𝑘 = 𝑚 → ([𝑘 / 𝑛]𝜓 ↔ 𝜃)) | 
| 14 | 13 | notbid 318 | . . . . . . . . 9
⊢ (𝑘 = 𝑚 → (¬ [𝑘 / 𝑛]𝜓 ↔ ¬ 𝜃)) | 
| 15 | 14 | imbi2d 340 | . . . . . . . 8
⊢ (𝑘 = 𝑚 → (((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ¬ [𝑘 / 𝑛]𝜓) ↔ ((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ¬ 𝜃))) | 
| 16 |  | nfv 1914 | . . . . . . . . . . 11
⊢
Ⅎ𝑛𝜏 | 
| 17 |  | nn0min.2 | . . . . . . . . . . 11
⊢ (𝑛 = (𝑚 + 1) → (𝜓 ↔ 𝜏)) | 
| 18 | 16, 17 | sbhypf 3544 | . . . . . . . . . 10
⊢ (𝑘 = (𝑚 + 1) → ([𝑘 / 𝑛]𝜓 ↔ 𝜏)) | 
| 19 | 18 | notbid 318 | . . . . . . . . 9
⊢ (𝑘 = (𝑚 + 1) → (¬ [𝑘 / 𝑛]𝜓 ↔ ¬ 𝜏)) | 
| 20 | 19 | imbi2d 340 | . . . . . . . 8
⊢ (𝑘 = (𝑚 + 1) → (((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ¬ [𝑘 / 𝑛]𝜓) ↔ ((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ¬ 𝜏))) | 
| 21 |  | sbequ12r 2252 | . . . . . . . . . 10
⊢ (𝑘 = 𝑛 → ([𝑘 / 𝑛]𝜓 ↔ 𝜓)) | 
| 22 | 21 | notbid 318 | . . . . . . . . 9
⊢ (𝑘 = 𝑛 → (¬ [𝑘 / 𝑛]𝜓 ↔ ¬ 𝜓)) | 
| 23 | 22 | imbi2d 340 | . . . . . . . 8
⊢ (𝑘 = 𝑛 → (((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ¬ [𝑘 / 𝑛]𝜓) ↔ ((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ¬ 𝜓))) | 
| 24 |  | nn0min.3 | . . . . . . . . 9
⊢ (𝜑 → ¬ 𝜒) | 
| 25 |  | 0nn0 12541 | . . . . . . . . . 10
⊢ 0 ∈
ℕ0 | 
| 26 | 11, 12 | sbiev 2314 | . . . . . . . . . . . . . 14
⊢ ([𝑚 / 𝑛]𝜓 ↔ 𝜃) | 
| 27 |  | nfv 1914 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛𝜒 | 
| 28 |  | nn0min.0 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 0 → (𝜓 ↔ 𝜒)) | 
| 29 | 27, 28 | sbhypf 3544 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 0 → ([𝑚 / 𝑛]𝜓 ↔ 𝜒)) | 
| 30 | 26, 29 | bitr3id 285 | . . . . . . . . . . . . 13
⊢ (𝑚 = 0 → (𝜃 ↔ 𝜒)) | 
| 31 | 30 | notbid 318 | . . . . . . . . . . . 12
⊢ (𝑚 = 0 → (¬ 𝜃 ↔ ¬ 𝜒)) | 
| 32 |  | oveq1 7438 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 = 0 → (𝑚 + 1) = (0 + 1)) | 
| 33 |  | 0p1e1 12388 | . . . . . . . . . . . . . . . 16
⊢ (0 + 1) =
1 | 
| 34 | 32, 33 | eqtrdi 2793 | . . . . . . . . . . . . . . 15
⊢ (𝑚 = 0 → (𝑚 + 1) = 1) | 
| 35 |  | 1nn 12277 | . . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ | 
| 36 |  | eleq1 2829 | . . . . . . . . . . . . . . . 16
⊢ ((𝑚 + 1) = 1 → ((𝑚 + 1) ∈ ℕ ↔ 1
∈ ℕ)) | 
| 37 | 35, 36 | mpbiri 258 | . . . . . . . . . . . . . . 15
⊢ ((𝑚 + 1) = 1 → (𝑚 + 1) ∈
ℕ) | 
| 38 | 17 | sbcieg 3828 | . . . . . . . . . . . . . . 15
⊢ ((𝑚 + 1) ∈ ℕ →
([(𝑚 + 1) / 𝑛]𝜓 ↔ 𝜏)) | 
| 39 | 34, 37, 38 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 0 → ([(𝑚 + 1) / 𝑛]𝜓 ↔ 𝜏)) | 
| 40 | 34 | sbceq1d 3793 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 0 → ([(𝑚 + 1) / 𝑛]𝜓 ↔ [1 / 𝑛]𝜓)) | 
| 41 | 39, 40 | bitr3d 281 | . . . . . . . . . . . . 13
⊢ (𝑚 = 0 → (𝜏 ↔ [1 / 𝑛]𝜓)) | 
| 42 | 41 | notbid 318 | . . . . . . . . . . . 12
⊢ (𝑚 = 0 → (¬ 𝜏 ↔ ¬ [1 / 𝑛]𝜓)) | 
| 43 | 31, 42 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑚 = 0 → ((¬ 𝜃 → ¬ 𝜏) ↔ (¬ 𝜒 → ¬ [1 / 𝑛]𝜓))) | 
| 44 | 43 | rspcv 3618 | . . . . . . . . . 10
⊢ (0 ∈
ℕ0 → (∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏) → (¬ 𝜒 → ¬ [1 / 𝑛]𝜓))) | 
| 45 | 25, 44 | ax-mp 5 | . . . . . . . . 9
⊢
(∀𝑚 ∈
ℕ0 (¬ 𝜃
→ ¬ 𝜏) → (¬
𝜒 → ¬ [1 /
𝑛]𝜓)) | 
| 46 | 24, 45 | mpan9 506 | . . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ¬ [1 / 𝑛]𝜓) | 
| 47 |  | cbvralsvw 3317 | . . . . . . . . . . 11
⊢
(∀𝑚 ∈
ℕ0 (¬ 𝜃
→ ¬ 𝜏) ↔
∀𝑘 ∈
ℕ0 [𝑘 /
𝑚](¬ 𝜃 → ¬ 𝜏)) | 
| 48 |  | nnnn0 12533 | . . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℕ0) | 
| 49 |  | sbequ12r 2252 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → ([𝑘 / 𝑚](¬ 𝜃 → ¬ 𝜏) ↔ (¬ 𝜃 → ¬ 𝜏))) | 
| 50 | 49 | rspcv 3618 | . . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ0
→ (∀𝑘 ∈
ℕ0 [𝑘 /
𝑚](¬ 𝜃 → ¬ 𝜏) → (¬ 𝜃 → ¬ 𝜏))) | 
| 51 | 48, 50 | syl 17 | . . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ →
(∀𝑘 ∈
ℕ0 [𝑘 /
𝑚](¬ 𝜃 → ¬ 𝜏) → (¬ 𝜃 → ¬ 𝜏))) | 
| 52 | 47, 51 | biimtrid 242 | . . . . . . . . . 10
⊢ (𝑚 ∈ ℕ →
(∀𝑚 ∈
ℕ0 (¬ 𝜃
→ ¬ 𝜏) → (¬
𝜃 → ¬ 𝜏))) | 
| 53 | 52 | adantld 490 | . . . . . . . . 9
⊢ (𝑚 ∈ ℕ → ((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → (¬ 𝜃 → ¬ 𝜏))) | 
| 54 | 53 | a2d 29 | . . . . . . . 8
⊢ (𝑚 ∈ ℕ → (((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ¬ 𝜃) → ((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ¬ 𝜏))) | 
| 55 | 7, 10, 15, 20, 23, 46, 54 | nnindf 32821 | . . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ¬ 𝜓)) | 
| 56 | 55 | rgen 3063 | . . . . . 6
⊢
∀𝑛 ∈
ℕ ((𝜑 ∧
∀𝑚 ∈
ℕ0 (¬ 𝜃
→ ¬ 𝜏)) → ¬
𝜓) | 
| 57 |  | r19.21v 3180 | . . . . . 6
⊢
(∀𝑛 ∈
ℕ ((𝜑 ∧
∀𝑚 ∈
ℕ0 (¬ 𝜃
→ ¬ 𝜏)) → ¬
𝜓) ↔ ((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ∀𝑛 ∈ ℕ ¬ 𝜓)) | 
| 58 | 56, 57 | mpbi 230 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ∀𝑛 ∈ ℕ ¬ 𝜓) | 
| 59 |  | ralnex 3072 | . . . . 5
⊢
(∀𝑛 ∈
ℕ ¬ 𝜓 ↔ ¬
∃𝑛 ∈ ℕ
𝜓) | 
| 60 | 58, 59 | sylib 218 | . . . 4
⊢ ((𝜑 ∧ ∀𝑚 ∈ ℕ0 (¬ 𝜃 → ¬ 𝜏)) → ¬ ∃𝑛 ∈ ℕ 𝜓) | 
| 61 | 2, 60 | pm2.65da 817 | . . 3
⊢ (𝜑 → ¬ ∀𝑚 ∈ ℕ0
(¬ 𝜃 → ¬ 𝜏)) | 
| 62 |  | imnan 399 | . . . 4
⊢ ((¬
𝜃 → ¬ 𝜏) ↔ ¬ (¬ 𝜃 ∧ 𝜏)) | 
| 63 | 62 | ralbii 3093 | . . 3
⊢
(∀𝑚 ∈
ℕ0 (¬ 𝜃
→ ¬ 𝜏) ↔
∀𝑚 ∈
ℕ0 ¬ (¬ 𝜃 ∧ 𝜏)) | 
| 64 | 61, 63 | sylnib 328 | . 2
⊢ (𝜑 → ¬ ∀𝑚 ∈ ℕ0
¬ (¬ 𝜃 ∧ 𝜏)) | 
| 65 |  | dfrex2 3073 | . 2
⊢
(∃𝑚 ∈
ℕ0 (¬ 𝜃
∧ 𝜏) ↔ ¬
∀𝑚 ∈
ℕ0 ¬ (¬ 𝜃 ∧ 𝜏)) | 
| 66 | 64, 65 | sylibr 234 | 1
⊢ (𝜑 → ∃𝑚 ∈ ℕ0 (¬ 𝜃 ∧ 𝜏)) |