Step | Hyp | Ref
| Expression |
1 | | noel 3222 |
. 2
⊢ ¬
∅ ∈ ∅ |
2 | | df-suc 4074 |
. . . . . 6
⊢ suc
y = (y
∪ {y}) |
3 | 2 | eleq2i 2101 |
. . . . 5
⊢ (suc
y ∈ suc
y ↔ suc y ∈ (y ∪ {y})) |
4 | | elun 3078 |
. . . . . 6
⊢ (suc
y ∈
(y ∪ {y}) ↔ (suc y ∈ y ∨ suc y ∈ {y})) |
5 | | bj-nntrans 9411 |
. . . . . . . 8
⊢ (y ∈ 𝜔
→ (suc y ∈ y → suc
y ⊆ y)) |
6 | | sucssel 4127 |
. . . . . . . 8
⊢ (y ∈ 𝜔
→ (suc y ⊆ y → y ∈ y)) |
7 | 5, 6 | syld 40 |
. . . . . . 7
⊢ (y ∈ 𝜔
→ (suc y ∈ y →
y ∈
y)) |
8 | | vex 2554 |
. . . . . . . . . 10
⊢ y ∈
V |
9 | 8 | sucid 4120 |
. . . . . . . . 9
⊢ y ∈ suc y |
10 | | elsni 3391 |
. . . . . . . . 9
⊢ (suc
y ∈
{y} → suc y = y) |
11 | 9, 10 | syl5eleq 2123 |
. . . . . . . 8
⊢ (suc
y ∈
{y} → y ∈ y) |
12 | 11 | a1i 9 |
. . . . . . 7
⊢ (y ∈ 𝜔
→ (suc y ∈ {y} →
y ∈
y)) |
13 | 7, 12 | jaod 636 |
. . . . . 6
⊢ (y ∈ 𝜔
→ ((suc y ∈ y ∨ suc y ∈ {y}) →
y ∈
y)) |
14 | 4, 13 | syl5bi 141 |
. . . . 5
⊢ (y ∈ 𝜔
→ (suc y ∈ (y ∪
{y}) → y ∈ y)) |
15 | 3, 14 | syl5bi 141 |
. . . 4
⊢ (y ∈ 𝜔
→ (suc y ∈ suc y →
y ∈
y)) |
16 | 15 | con3d 560 |
. . 3
⊢ (y ∈ 𝜔
→ (¬ y ∈ y →
¬ suc y ∈ suc y)) |
17 | 16 | rgen 2368 |
. 2
⊢ ∀y ∈ 𝜔 (¬ y ∈ y → ¬ suc y ∈ suc y) |
18 | | ax-bdel 9276 |
. . . 4
⊢
BOUNDED x ∈ x |
19 | 18 | ax-bdn 9272 |
. . 3
⊢
BOUNDED ¬ x ∈ x |
20 | | nfv 1418 |
. . 3
⊢
Ⅎx ¬ ∅ ∈ ∅ |
21 | | nfv 1418 |
. . 3
⊢
Ⅎx ¬ y ∈ y |
22 | | nfv 1418 |
. . 3
⊢
Ⅎx ¬ suc y ∈ suc y |
23 | | eleq1 2097 |
. . . . . 6
⊢ (x = ∅ → (x ∈ x ↔ ∅ ∈
x)) |
24 | | eleq2 2098 |
. . . . . 6
⊢ (x = ∅ → (∅ ∈ x ↔
∅ ∈ ∅)) |
25 | 23, 24 | bitrd 177 |
. . . . 5
⊢ (x = ∅ → (x ∈ x ↔ ∅ ∈
∅)) |
26 | 25 | notbid 591 |
. . . 4
⊢ (x = ∅ → (¬ x ∈ x ↔ ¬ ∅ ∈ ∅)) |
27 | 26 | biimprd 147 |
. . 3
⊢ (x = ∅ → (¬ ∅ ∈ ∅ → ¬ x ∈ x)) |
28 | | elequ1 1597 |
. . . . . 6
⊢ (x = y →
(x ∈
x ↔ y ∈ x)) |
29 | | elequ2 1598 |
. . . . . 6
⊢ (x = y →
(y ∈
x ↔ y ∈ y)) |
30 | 28, 29 | bitrd 177 |
. . . . 5
⊢ (x = y →
(x ∈
x ↔ y ∈ y)) |
31 | 30 | notbid 591 |
. . . 4
⊢ (x = y →
(¬ x ∈ x ↔
¬ y ∈
y)) |
32 | 31 | biimpd 132 |
. . 3
⊢ (x = y →
(¬ x ∈ x →
¬ y ∈
y)) |
33 | | eleq1 2097 |
. . . . . 6
⊢ (x = suc y →
(x ∈
x ↔ suc y ∈ x)) |
34 | | eleq2 2098 |
. . . . . 6
⊢ (x = suc y →
(suc y ∈
x ↔ suc y ∈ suc y)) |
35 | 33, 34 | bitrd 177 |
. . . . 5
⊢ (x = suc y →
(x ∈
x ↔ suc y ∈ suc y)) |
36 | 35 | notbid 591 |
. . . 4
⊢ (x = suc y →
(¬ x ∈ x ↔
¬ suc y ∈ suc y)) |
37 | 36 | biimprd 147 |
. . 3
⊢ (x = suc y →
(¬ suc y ∈ suc y →
¬ x ∈
x)) |
38 | | nfcv 2175 |
. . 3
⊢
ℲxA |
39 | | nfv 1418 |
. . 3
⊢
Ⅎx ¬ A ∈ A |
40 | | eleq1 2097 |
. . . . . 6
⊢ (x = A →
(x ∈
x ↔ A ∈ x)) |
41 | | eleq2 2098 |
. . . . . 6
⊢ (x = A →
(A ∈
x ↔ A ∈ A)) |
42 | 40, 41 | bitrd 177 |
. . . . 5
⊢ (x = A →
(x ∈
x ↔ A ∈ A)) |
43 | 42 | notbid 591 |
. . . 4
⊢ (x = A →
(¬ x ∈ x ↔
¬ A ∈
A)) |
44 | 43 | biimpd 132 |
. . 3
⊢ (x = A →
(¬ x ∈ x →
¬ A ∈
A)) |
45 | 19, 20, 21, 22, 27, 32, 37, 38, 39, 44 | bj-bdfindisg 9408 |
. 2
⊢ ((¬
∅ ∈ ∅ ∧ ∀y ∈ 𝜔
(¬ y ∈ y →
¬ suc y ∈ suc y))
→ (A ∈ 𝜔 → ¬ A ∈ A)) |
46 | 1, 17, 45 | mp2an 402 |
1
⊢ (A ∈ 𝜔
→ ¬ A ∈ A) |