Step | Hyp | Ref
| Expression |
1 | | sucprc 4408 |
. 2
⊢ (¬
𝐴 ∈ V → suc 𝐴 = 𝐴) |
2 | | elirr 4536 |
. . . 4
⊢ ¬
𝐴 ∈ 𝐴 |
3 | | nfv 1528 |
. . . . 5
⊢
Ⅎ𝑥 𝐴 ∈ 𝐴 |
4 | | eleq1 2240 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐴 ↔ 𝐴 ∈ 𝐴)) |
5 | 3, 4 | ceqsalg 2765 |
. . . 4
⊢ (𝐴 ∈ V → (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐴) ↔ 𝐴 ∈ 𝐴)) |
6 | 2, 5 | mtbiri 675 |
. . 3
⊢ (𝐴 ∈ V → ¬
∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐴)) |
7 | | velsn 3608 |
. . . . 5
⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
8 | | olc 711 |
. . . . . 6
⊢ (𝑥 ∈ {𝐴} → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐴})) |
9 | | elun 3276 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ∪ {𝐴}) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐴})) |
10 | | ssid 3175 |
. . . . . . . . 9
⊢ 𝐴 ⊆ 𝐴 |
11 | | df-suc 4367 |
. . . . . . . . . . 11
⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) |
12 | 11 | eqeq1i 2185 |
. . . . . . . . . 10
⊢ (suc
𝐴 = 𝐴 ↔ (𝐴 ∪ {𝐴}) = 𝐴) |
13 | | sseq1 3178 |
. . . . . . . . . 10
⊢ ((𝐴 ∪ {𝐴}) = 𝐴 → ((𝐴 ∪ {𝐴}) ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
14 | 12, 13 | sylbi 121 |
. . . . . . . . 9
⊢ (suc
𝐴 = 𝐴 → ((𝐴 ∪ {𝐴}) ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
15 | 10, 14 | mpbiri 168 |
. . . . . . . 8
⊢ (suc
𝐴 = 𝐴 → (𝐴 ∪ {𝐴}) ⊆ 𝐴) |
16 | 15 | sseld 3154 |
. . . . . . 7
⊢ (suc
𝐴 = 𝐴 → (𝑥 ∈ (𝐴 ∪ {𝐴}) → 𝑥 ∈ 𝐴)) |
17 | 9, 16 | biimtrrid 153 |
. . . . . 6
⊢ (suc
𝐴 = 𝐴 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐴}) → 𝑥 ∈ 𝐴)) |
18 | 8, 17 | syl5 32 |
. . . . 5
⊢ (suc
𝐴 = 𝐴 → (𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐴)) |
19 | 7, 18 | biimtrrid 153 |
. . . 4
⊢ (suc
𝐴 = 𝐴 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐴)) |
20 | 19 | alrimiv 1874 |
. . 3
⊢ (suc
𝐴 = 𝐴 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐴)) |
21 | 6, 20 | nsyl3 626 |
. 2
⊢ (suc
𝐴 = 𝐴 → ¬ 𝐴 ∈ V) |
22 | 1, 21 | impbii 126 |
1
⊢ (¬
𝐴 ∈ V ↔ suc 𝐴 = 𝐴) |