Step | Hyp | Ref
| Expression |
1 | | 0cnsuc 4401 |
. . . . . 6
⊢ (y +c 1c) ≠
0c |
2 | | df-ne 2518 |
. . . . . 6
⊢ ((y +c 1c) ≠
0c ↔ ¬ (y
+c 1c) =
0c) |
3 | 1, 2 | mpbi 199 |
. . . . 5
⊢ ¬ (y +c 1c) =
0c |
4 | | iffalse 3669 |
. . . . . . . . . . 11
⊢ (¬ y ∈ Nn → if(y ∈ Nn , (y +c 1c),
y) = y) |
5 | 4 | eqeq2d 2364 |
. . . . . . . . . 10
⊢ (¬ y ∈ Nn → (0c = if(y ∈ Nn , (y
+c 1c), y) ↔ 0c = y)) |
6 | 5 | biimpac 472 |
. . . . . . . . 9
⊢
((0c = if(y ∈ Nn , (y +c 1c),
y) ∧ ¬
y ∈ Nn ) → 0c = y) |
7 | | peano1 4402 |
. . . . . . . . 9
⊢
0c ∈ Nn |
8 | 6, 7 | syl6eqelr 2442 |
. . . . . . . 8
⊢
((0c = if(y ∈ Nn , (y +c 1c),
y) ∧ ¬
y ∈ Nn ) → y ∈ Nn
) |
9 | 8 | ex 423 |
. . . . . . 7
⊢
(0c = if(y ∈ Nn , (y +c 1c),
y) → (¬ y ∈ Nn → y ∈ Nn
)) |
10 | 9 | pm2.18d 103 |
. . . . . 6
⊢
(0c = if(y ∈ Nn , (y +c 1c),
y) → y ∈ Nn ) |
11 | | iftrue 3668 |
. . . . . . . . 9
⊢ (y ∈ Nn → if(y ∈ Nn , (y +c 1c),
y) = (y
+c 1c)) |
12 | 11 | eqeq2d 2364 |
. . . . . . . 8
⊢ (y ∈ Nn → (0c = if(y ∈ Nn , (y
+c 1c), y) ↔ 0c = (y +c
1c))) |
13 | | eqcom 2355 |
. . . . . . . 8
⊢
(0c = (y
+c 1c) ↔ (y +c 1c) =
0c) |
14 | 12, 13 | syl6bb 252 |
. . . . . . 7
⊢ (y ∈ Nn → (0c = if(y ∈ Nn , (y
+c 1c), y) ↔ (y
+c 1c) =
0c)) |
15 | 14 | biimpd 198 |
. . . . . 6
⊢ (y ∈ Nn → (0c = if(y ∈ Nn , (y
+c 1c), y) → (y
+c 1c) =
0c)) |
16 | 10, 15 | mpcom 32 |
. . . . 5
⊢
(0c = if(y ∈ Nn , (y +c 1c),
y) → (y +c 1c) =
0c) |
17 | 3, 16 | mto 167 |
. . . 4
⊢ ¬
0c = if(y ∈ Nn , (y +c 1c),
y) |
18 | 17 | a1i 10 |
. . 3
⊢ (y ∈ A → ¬ 0c = if(y ∈ Nn , (y
+c 1c), y)) |
19 | 18 | nrex 2716 |
. 2
⊢ ¬ ∃y ∈ A
0c = if(y ∈ Nn , (y +c 1c),
y) |
20 | | 0cex 4392 |
. . 3
⊢
0c ∈
V |
21 | | eqeq1 2359 |
. . . 4
⊢ (x = 0c → (x = if(y ∈ Nn , (y +c 1c),
y) ↔ 0c =
if(y ∈
Nn , (y
+c 1c), y))) |
22 | 21 | rexbidv 2635 |
. . 3
⊢ (x = 0c → (∃y ∈ A x = if(y ∈ Nn , (y +c 1c),
y) ↔ ∃y ∈ A
0c = if(y ∈ Nn , (y +c 1c),
y))) |
23 | | df-phi 4565 |
. . 3
⊢ Phi A = {x ∣ ∃y ∈ A x = if(y ∈ Nn , (y +c 1c),
y)} |
24 | 20, 22, 23 | elab2 2988 |
. 2
⊢
(0c ∈ Phi A ↔ ∃y ∈ A
0c = if(y ∈ Nn , (y +c 1c),
y)) |
25 | 19, 24 | mtbir 290 |
1
⊢ ¬
0c ∈
Phi A |