Proof of Theorem en2eleq
Step | Hyp | Ref
| Expression |
1 | | 2onn 7607 |
. . . . . 6
⊢
2𝑜 ∈ ω |
2 | | nnfi 8038 |
. . . . . 6
⊢
(2𝑜 ∈ ω → 2𝑜
∈ Fin) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢
2𝑜 ∈ Fin |
4 | | enfi 8061 |
. . . . 5
⊢ (𝑃 ≈ 2𝑜
→ (𝑃 ∈ Fin ↔
2𝑜 ∈ Fin)) |
5 | 3, 4 | mpbiri 247 |
. . . 4
⊢ (𝑃 ≈ 2𝑜
→ 𝑃 ∈
Fin) |
6 | 5 | adantl 481 |
. . 3
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → 𝑃 ∈ Fin) |
7 | | simpl 472 |
. . . 4
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → 𝑋 ∈ 𝑃) |
8 | | 1onn 7606 |
. . . . . . . . 9
⊢
1𝑜 ∈ ω |
9 | 8 | a1i 11 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) →
1𝑜 ∈ ω) |
10 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → 𝑃 ≈
2𝑜) |
11 | | df-2o 7448 |
. . . . . . . . 9
⊢
2𝑜 = suc 1𝑜 |
12 | 10, 11 | syl6breq 4624 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → 𝑃 ≈ suc
1𝑜) |
13 | | dif1en 8078 |
. . . . . . . 8
⊢
((1𝑜 ∈ ω ∧ 𝑃 ≈ suc 1𝑜 ∧
𝑋 ∈ 𝑃) → (𝑃 ∖ {𝑋}) ≈
1𝑜) |
14 | 9, 12, 7, 13 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) →
(𝑃 ∖ {𝑋}) ≈
1𝑜) |
15 | | en1uniel 7914 |
. . . . . . 7
⊢ ((𝑃 ∖ {𝑋}) ≈ 1𝑜 →
∪ (𝑃 ∖ {𝑋}) ∈ (𝑃 ∖ {𝑋})) |
16 | 14, 15 | syl 17 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → ∪ (𝑃
∖ {𝑋}) ∈ (𝑃 ∖ {𝑋})) |
17 | | eldifsn 4260 |
. . . . . 6
⊢ (∪ (𝑃
∖ {𝑋}) ∈ (𝑃 ∖ {𝑋}) ↔ (∪
(𝑃 ∖ {𝑋}) ∈ 𝑃 ∧ ∪ (𝑃 ∖ {𝑋}) ≠ 𝑋)) |
18 | 16, 17 | sylib 207 |
. . . . 5
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) →
(∪ (𝑃 ∖ {𝑋}) ∈ 𝑃 ∧ ∪ (𝑃 ∖ {𝑋}) ≠ 𝑋)) |
19 | 18 | simpld 474 |
. . . 4
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → ∪ (𝑃
∖ {𝑋}) ∈ 𝑃) |
20 | | prssi 4293 |
. . . 4
⊢ ((𝑋 ∈ 𝑃 ∧ ∪ (𝑃 ∖ {𝑋}) ∈ 𝑃) → {𝑋, ∪ (𝑃 ∖ {𝑋})} ⊆ 𝑃) |
21 | 7, 19, 20 | syl2anc 691 |
. . 3
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) →
{𝑋, ∪ (𝑃
∖ {𝑋})} ⊆ 𝑃) |
22 | 18 | simprd 478 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → ∪ (𝑃
∖ {𝑋}) ≠ 𝑋) |
23 | 22 | necomd 2837 |
. . . . 5
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → 𝑋 ≠ ∪ (𝑃
∖ {𝑋})) |
24 | | pr2nelem 8710 |
. . . . 5
⊢ ((𝑋 ∈ 𝑃 ∧ ∪ (𝑃 ∖ {𝑋}) ∈ 𝑃 ∧ 𝑋 ≠ ∪ (𝑃 ∖ {𝑋})) → {𝑋, ∪ (𝑃 ∖ {𝑋})} ≈
2𝑜) |
25 | 7, 19, 23, 24 | syl3anc 1318 |
. . . 4
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) →
{𝑋, ∪ (𝑃
∖ {𝑋})} ≈
2𝑜) |
26 | | ensym 7891 |
. . . . 5
⊢ (𝑃 ≈ 2𝑜
→ 2𝑜 ≈ 𝑃) |
27 | 26 | adantl 481 |
. . . 4
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) →
2𝑜 ≈ 𝑃) |
28 | | entr 7894 |
. . . 4
⊢ (({𝑋, ∪
(𝑃 ∖ {𝑋})} ≈
2𝑜 ∧ 2𝑜 ≈ 𝑃) → {𝑋, ∪ (𝑃 ∖ {𝑋})} ≈ 𝑃) |
29 | 25, 27, 28 | syl2anc 691 |
. . 3
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) →
{𝑋, ∪ (𝑃
∖ {𝑋})} ≈ 𝑃) |
30 | | fisseneq 8056 |
. . 3
⊢ ((𝑃 ∈ Fin ∧ {𝑋, ∪
(𝑃 ∖ {𝑋})} ⊆ 𝑃 ∧ {𝑋, ∪ (𝑃 ∖ {𝑋})} ≈ 𝑃) → {𝑋, ∪ (𝑃 ∖ {𝑋})} = 𝑃) |
31 | 6, 21, 29, 30 | syl3anc 1318 |
. 2
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) →
{𝑋, ∪ (𝑃
∖ {𝑋})} = 𝑃) |
32 | 31 | eqcomd 2616 |
1
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → 𝑃 = {𝑋, ∪ (𝑃 ∖ {𝑋})}) |