Step | Hyp | Ref
| Expression |
1 | | noel 3411 |
. 2
⊢ ¬
∅ ∈ ∅ |
2 | | df-suc 4346 |
. . . . . 6
⊢ suc 𝑦 = (𝑦 ∪ {𝑦}) |
3 | 2 | eleq2i 2231 |
. . . . 5
⊢ (suc
𝑦 ∈ suc 𝑦 ↔ suc 𝑦 ∈ (𝑦 ∪ {𝑦})) |
4 | | elun 3261 |
. . . . . 6
⊢ (suc
𝑦 ∈ (𝑦 ∪ {𝑦}) ↔ (suc 𝑦 ∈ 𝑦 ∨ suc 𝑦 ∈ {𝑦})) |
5 | | bj-nntrans 13726 |
. . . . . . . 8
⊢ (𝑦 ∈ ω → (suc
𝑦 ∈ 𝑦 → suc 𝑦 ⊆ 𝑦)) |
6 | | sucssel 4399 |
. . . . . . . 8
⊢ (𝑦 ∈ ω → (suc
𝑦 ⊆ 𝑦 → 𝑦 ∈ 𝑦)) |
7 | 5, 6 | syld 45 |
. . . . . . 7
⊢ (𝑦 ∈ ω → (suc
𝑦 ∈ 𝑦 → 𝑦 ∈ 𝑦)) |
8 | | vex 2727 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
9 | 8 | sucid 4392 |
. . . . . . . . 9
⊢ 𝑦 ∈ suc 𝑦 |
10 | | elsni 3591 |
. . . . . . . . 9
⊢ (suc
𝑦 ∈ {𝑦} → suc 𝑦 = 𝑦) |
11 | 9, 10 | eleqtrid 2253 |
. . . . . . . 8
⊢ (suc
𝑦 ∈ {𝑦} → 𝑦 ∈ 𝑦) |
12 | 11 | a1i 9 |
. . . . . . 7
⊢ (𝑦 ∈ ω → (suc
𝑦 ∈ {𝑦} → 𝑦 ∈ 𝑦)) |
13 | 7, 12 | jaod 707 |
. . . . . 6
⊢ (𝑦 ∈ ω → ((suc
𝑦 ∈ 𝑦 ∨ suc 𝑦 ∈ {𝑦}) → 𝑦 ∈ 𝑦)) |
14 | 4, 13 | syl5bi 151 |
. . . . 5
⊢ (𝑦 ∈ ω → (suc
𝑦 ∈ (𝑦 ∪ {𝑦}) → 𝑦 ∈ 𝑦)) |
15 | 3, 14 | syl5bi 151 |
. . . 4
⊢ (𝑦 ∈ ω → (suc
𝑦 ∈ suc 𝑦 → 𝑦 ∈ 𝑦)) |
16 | 15 | con3d 621 |
. . 3
⊢ (𝑦 ∈ ω → (¬
𝑦 ∈ 𝑦 → ¬ suc 𝑦 ∈ suc 𝑦)) |
17 | 16 | rgen 2517 |
. 2
⊢
∀𝑦 ∈
ω (¬ 𝑦 ∈
𝑦 → ¬ suc 𝑦 ∈ suc 𝑦) |
18 | | ax-bdel 13596 |
. . . 4
⊢
BOUNDED 𝑥 ∈ 𝑥 |
19 | 18 | ax-bdn 13592 |
. . 3
⊢
BOUNDED ¬ 𝑥 ∈ 𝑥 |
20 | | nfv 1515 |
. . 3
⊢
Ⅎ𝑥 ¬
∅ ∈ ∅ |
21 | | nfv 1515 |
. . 3
⊢
Ⅎ𝑥 ¬ 𝑦 ∈ 𝑦 |
22 | | nfv 1515 |
. . 3
⊢
Ⅎ𝑥 ¬ suc
𝑦 ∈ suc 𝑦 |
23 | | eleq1 2227 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 ∈ 𝑥 ↔ ∅ ∈ 𝑥)) |
24 | | eleq2 2228 |
. . . . . 6
⊢ (𝑥 = ∅ → (∅
∈ 𝑥 ↔ ∅
∈ ∅)) |
25 | 23, 24 | bitrd 187 |
. . . . 5
⊢ (𝑥 = ∅ → (𝑥 ∈ 𝑥 ↔ ∅ ∈
∅)) |
26 | 25 | notbid 657 |
. . . 4
⊢ (𝑥 = ∅ → (¬ 𝑥 ∈ 𝑥 ↔ ¬ ∅ ∈
∅)) |
27 | 26 | biimprd 157 |
. . 3
⊢ (𝑥 = ∅ → (¬ ∅
∈ ∅ → ¬ 𝑥 ∈ 𝑥)) |
28 | | elequ1 2139 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
29 | | elequ2 2140 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦)) |
30 | 28, 29 | bitrd 187 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦)) |
31 | 30 | notbid 657 |
. . . 4
⊢ (𝑥 = 𝑦 → (¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝑦 ∈ 𝑦)) |
32 | 31 | biimpd 143 |
. . 3
⊢ (𝑥 = 𝑦 → (¬ 𝑥 ∈ 𝑥 → ¬ 𝑦 ∈ 𝑦)) |
33 | | eleq1 2227 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ 𝑥 ↔ suc 𝑦 ∈ 𝑥)) |
34 | | eleq2 2228 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (suc 𝑦 ∈ 𝑥 ↔ suc 𝑦 ∈ suc 𝑦)) |
35 | 33, 34 | bitrd 187 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ 𝑥 ↔ suc 𝑦 ∈ suc 𝑦)) |
36 | 35 | notbid 657 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (¬ 𝑥 ∈ 𝑥 ↔ ¬ suc 𝑦 ∈ suc 𝑦)) |
37 | 36 | biimprd 157 |
. . 3
⊢ (𝑥 = suc 𝑦 → (¬ suc 𝑦 ∈ suc 𝑦 → ¬ 𝑥 ∈ 𝑥)) |
38 | | nfcv 2306 |
. . 3
⊢
Ⅎ𝑥𝐴 |
39 | | nfv 1515 |
. . 3
⊢
Ⅎ𝑥 ¬ 𝐴 ∈ 𝐴 |
40 | | eleq1 2227 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥)) |
41 | | eleq2 2228 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐴)) |
42 | 40, 41 | bitrd 187 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑥 ↔ 𝐴 ∈ 𝐴)) |
43 | 42 | notbid 657 |
. . . 4
⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝐴 ∈ 𝐴)) |
44 | 43 | biimpd 143 |
. . 3
⊢ (𝑥 = 𝐴 → (¬ 𝑥 ∈ 𝑥 → ¬ 𝐴 ∈ 𝐴)) |
45 | 19, 20, 21, 22, 27, 32, 37, 38, 39, 44 | bj-bdfindisg 13723 |
. 2
⊢ ((¬
∅ ∈ ∅ ∧ ∀𝑦 ∈ ω (¬ 𝑦 ∈ 𝑦 → ¬ suc 𝑦 ∈ suc 𝑦)) → (𝐴 ∈ ω → ¬ 𝐴 ∈ 𝐴)) |
46 | 1, 17, 45 | mp2an 423 |
1
⊢ (𝐴 ∈ ω → ¬
𝐴 ∈ 𝐴) |