| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2onn 8681 | . . . . . . . . . 10
⊢
2o ∈ ω | 
| 2 |  | nnfi 9208 | . . . . . . . . . 10
⊢
(2o ∈ ω → 2o ∈
Fin) | 
| 3 | 1, 2 | ax-mp 5 | . . . . . . . . 9
⊢
2o ∈ Fin | 
| 4 |  | enfi 9228 | . . . . . . . . 9
⊢ (𝑃 ≈ 2o →
(𝑃 ∈ Fin ↔
2o ∈ Fin)) | 
| 5 | 3, 4 | mpbiri 258 | . . . . . . . 8
⊢ (𝑃 ≈ 2o →
𝑃 ∈
Fin) | 
| 6 | 5 | adantl 481 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → 𝑃 ∈ Fin) | 
| 7 |  | diffi 9216 | . . . . . . 7
⊢ (𝑃 ∈ Fin → (𝑃 ∖ {𝑋}) ∈ Fin) | 
| 8 | 6, 7 | syl 17 | . . . . . 6
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → (𝑃 ∖ {𝑋}) ∈ Fin) | 
| 9 | 8 | cardidd 10590 | . . . . 5
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) →
(card‘(𝑃 ∖
{𝑋})) ≈ (𝑃 ∖ {𝑋})) | 
| 10 | 9 | ensymd 9046 | . . . 4
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → (𝑃 ∖ {𝑋}) ≈ (card‘(𝑃 ∖ {𝑋}))) | 
| 11 |  | simpl 482 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → 𝑋 ∈ 𝑃) | 
| 12 |  | dif1card 10051 | . . . . . . 7
⊢ ((𝑃 ∈ Fin ∧ 𝑋 ∈ 𝑃) → (card‘𝑃) = suc (card‘(𝑃 ∖ {𝑋}))) | 
| 13 | 6, 11, 12 | syl2anc 584 | . . . . . 6
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) →
(card‘𝑃) = suc
(card‘(𝑃 ∖
{𝑋}))) | 
| 14 |  | cardennn 10024 | . . . . . . . . 9
⊢ ((𝑃 ≈ 2o ∧
2o ∈ ω) → (card‘𝑃) = 2o) | 
| 15 | 1, 14 | mpan2 691 | . . . . . . . 8
⊢ (𝑃 ≈ 2o →
(card‘𝑃) =
2o) | 
| 16 |  | df-2o 8508 | . . . . . . . 8
⊢
2o = suc 1o | 
| 17 | 15, 16 | eqtrdi 2792 | . . . . . . 7
⊢ (𝑃 ≈ 2o →
(card‘𝑃) = suc
1o) | 
| 18 | 17 | adantl 481 | . . . . . 6
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) →
(card‘𝑃) = suc
1o) | 
| 19 | 13, 18 | eqtr3d 2778 | . . . . 5
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → suc
(card‘(𝑃 ∖
{𝑋})) = suc
1o) | 
| 20 |  | suc11reg 9660 | . . . . 5
⊢ (suc
(card‘(𝑃 ∖
{𝑋})) = suc 1o
↔ (card‘(𝑃
∖ {𝑋})) =
1o) | 
| 21 | 19, 20 | sylib 218 | . . . 4
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) →
(card‘(𝑃 ∖
{𝑋})) =
1o) | 
| 22 | 10, 21 | breqtrd 5168 | . . 3
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → (𝑃 ∖ {𝑋}) ≈ 1o) | 
| 23 |  | en1 9065 | . . 3
⊢ ((𝑃 ∖ {𝑋}) ≈ 1o ↔ ∃𝑥(𝑃 ∖ {𝑋}) = {𝑥}) | 
| 24 | 22, 23 | sylib 218 | . 2
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∃𝑥(𝑃 ∖ {𝑋}) = {𝑥}) | 
| 25 |  | simplll 774 | . . . . . . 7
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → 𝑋 ∈ 𝑃) | 
| 26 | 25 | elexd 3503 | . . . . . 6
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → 𝑋 ∈ V) | 
| 27 |  | simplr 768 | . . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → (𝑃 ∖ {𝑋}) = {𝑥}) | 
| 28 |  | sneqbg 4842 | . . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝑃 → ({𝑋} = {𝑥} ↔ 𝑋 = 𝑥)) | 
| 29 | 28 | biimpar 477 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑋 = 𝑥) → {𝑋} = {𝑥}) | 
| 30 | 29 | ad4ant14 752 | . . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → {𝑋} = {𝑥}) | 
| 31 | 27, 30 | eqtr4d 2779 | . . . . . . . . . 10
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → (𝑃 ∖ {𝑋}) = {𝑋}) | 
| 32 | 31 | ineq2d 4219 | . . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → ({𝑋} ∩ (𝑃 ∖ {𝑋})) = ({𝑋} ∩ {𝑋})) | 
| 33 |  | disjdif 4471 | . . . . . . . . 9
⊢ ({𝑋} ∩ (𝑃 ∖ {𝑋})) = ∅ | 
| 34 |  | inidm 4226 | . . . . . . . . 9
⊢ ({𝑋} ∩ {𝑋}) = {𝑋} | 
| 35 | 32, 33, 34 | 3eqtr3g 2799 | . . . . . . . 8
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → ∅ = {𝑋}) | 
| 36 | 35 | eqcomd 2742 | . . . . . . 7
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → {𝑋} = ∅) | 
| 37 |  | snprc 4716 | . . . . . . 7
⊢ (¬
𝑋 ∈ V ↔ {𝑋} = ∅) | 
| 38 | 36, 37 | sylibr 234 | . . . . . 6
⊢ ((((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) ∧ 𝑋 = 𝑥) → ¬ 𝑋 ∈ V) | 
| 39 | 26, 38 | pm2.65da 816 | . . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) → ¬ 𝑋 = 𝑥) | 
| 40 | 39 | neqned 2946 | . . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) → 𝑋 ≠ 𝑥) | 
| 41 |  | simpr 484 | . . . . . 6
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) → (𝑃 ∖ {𝑋}) = {𝑥}) | 
| 42 | 41 | unieqd 4919 | . . . . 5
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) → ∪ (𝑃 ∖ {𝑋}) = ∪ {𝑥}) | 
| 43 |  | unisnv 4926 | . . . . 5
⊢ ∪ {𝑥}
= 𝑥 | 
| 44 | 42, 43 | eqtrdi 2792 | . . . 4
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) → ∪ (𝑃 ∖ {𝑋}) = 𝑥) | 
| 45 | 40, 44 | neeqtrrd 3014 | . . 3
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) → 𝑋 ≠ ∪ (𝑃 ∖ {𝑋})) | 
| 46 | 45 | necomd 2995 | . 2
⊢ (((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) ∧ (𝑃 ∖ {𝑋}) = {𝑥}) → ∪ (𝑃 ∖ {𝑋}) ≠ 𝑋) | 
| 47 | 24, 46 | exlimddv 1934 | 1
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∪ (𝑃
∖ {𝑋}) ≠ 𝑋) |