Proof of Theorem en2other2
Step | Hyp | Ref
| Expression |
1 | | en2eleq 8831 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → 𝑃 = {𝑋, ∪ (𝑃 ∖ {𝑋})}) |
2 | | prcom 4267 |
. . . . . . 7
⊢ {𝑋, ∪
(𝑃 ∖ {𝑋})} = {∪ (𝑃
∖ {𝑋}), 𝑋} |
3 | 1, 2 | syl6eq 2672 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → 𝑃 = {∪
(𝑃 ∖ {𝑋}), 𝑋}) |
4 | 3 | difeq1d 3727 |
. . . . 5
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) →
(𝑃 ∖ {∪ (𝑃
∖ {𝑋})}) = ({∪ (𝑃
∖ {𝑋}), 𝑋} ∖ {∪ (𝑃
∖ {𝑋})})) |
5 | | difprsnss 4329 |
. . . . 5
⊢ ({∪ (𝑃
∖ {𝑋}), 𝑋} ∖ {∪ (𝑃
∖ {𝑋})}) ⊆
{𝑋} |
6 | 4, 5 | syl6eqss 3655 |
. . . 4
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) →
(𝑃 ∖ {∪ (𝑃
∖ {𝑋})}) ⊆
{𝑋}) |
7 | | simpl 473 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → 𝑋 ∈ 𝑃) |
8 | | 1onn 7719 |
. . . . . . . . . 10
⊢
1𝑜 ∈ ω |
9 | 8 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) →
1𝑜 ∈ ω) |
10 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → 𝑃 ≈
2𝑜) |
11 | | df-2o 7561 |
. . . . . . . . . 10
⊢
2𝑜 = suc 1𝑜 |
12 | 10, 11 | syl6breq 4694 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → 𝑃 ≈ suc
1𝑜) |
13 | | dif1en 8193 |
. . . . . . . . 9
⊢
((1𝑜 ∈ ω ∧ 𝑃 ≈ suc 1𝑜 ∧
𝑋 ∈ 𝑃) → (𝑃 ∖ {𝑋}) ≈
1𝑜) |
14 | 9, 12, 7, 13 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) →
(𝑃 ∖ {𝑋}) ≈
1𝑜) |
15 | | en1uniel 8028 |
. . . . . . . 8
⊢ ((𝑃 ∖ {𝑋}) ≈ 1𝑜 →
∪ (𝑃 ∖ {𝑋}) ∈ (𝑃 ∖ {𝑋})) |
16 | | eldifsni 4320 |
. . . . . . . 8
⊢ (∪ (𝑃
∖ {𝑋}) ∈ (𝑃 ∖ {𝑋}) → ∪
(𝑃 ∖ {𝑋}) ≠ 𝑋) |
17 | 14, 15, 16 | 3syl 18 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → ∪ (𝑃
∖ {𝑋}) ≠ 𝑋) |
18 | 17 | necomd 2849 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → 𝑋 ≠ ∪ (𝑃
∖ {𝑋})) |
19 | | eldifsn 4317 |
. . . . . 6
⊢ (𝑋 ∈ (𝑃 ∖ {∪
(𝑃 ∖ {𝑋})}) ↔ (𝑋 ∈ 𝑃 ∧ 𝑋 ≠ ∪ (𝑃 ∖ {𝑋}))) |
20 | 7, 18, 19 | sylanbrc 698 |
. . . . 5
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → 𝑋 ∈ (𝑃 ∖ {∪
(𝑃 ∖ {𝑋})})) |
21 | 20 | snssd 4340 |
. . . 4
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) →
{𝑋} ⊆ (𝑃 ∖ {∪ (𝑃
∖ {𝑋})})) |
22 | 6, 21 | eqssd 3620 |
. . 3
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) →
(𝑃 ∖ {∪ (𝑃
∖ {𝑋})}) = {𝑋}) |
23 | 22 | unieqd 4446 |
. 2
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → ∪ (𝑃
∖ {∪ (𝑃 ∖ {𝑋})}) = ∪ {𝑋}) |
24 | | unisng 4452 |
. . 3
⊢ (𝑋 ∈ 𝑃 → ∪ {𝑋} = 𝑋) |
25 | 24 | adantr 481 |
. 2
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → ∪ {𝑋}
= 𝑋) |
26 | 23, 25 | eqtrd 2656 |
1
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2𝑜) → ∪ (𝑃
∖ {∪ (𝑃 ∖ {𝑋})}) = 𝑋) |