Metamath Proof Explorer

Theorem en2eleq

Description: Express a set of pair cardinality as the unordered pair of a given element and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Assertion en2eleq ⊢ X ∈ P ∧ P ≈ 2 𝑜 → P = X ⋃ P ∖ X

Proof

Step Hyp Ref Expression
1 2onn ⊢ 2 𝑜 ∈ ω
2 nnfi ⊢ 2 𝑜 ∈ ω → 2 𝑜 ∈ Fin
3 1 2 ax-mp ⊢ 2 𝑜 ∈ Fin
4 enfi ⊢ P ≈ 2 𝑜 → P ∈ Fin ↔ 2 𝑜 ∈ Fin
5 3 4 mpbiri ⊢ P ≈ 2 𝑜 → P ∈ Fin
6 5 adantl ⊢ X ∈ P ∧ P ≈ 2 𝑜 → P ∈ Fin
7 simpl ⊢ X ∈ P ∧ P ≈ 2 𝑜 → X ∈ P
8 1onn ⊢ 1 𝑜 ∈ ω
9 simpr ⊢ X ∈ P ∧ P ≈ 2 𝑜 → P ≈ 2 𝑜
10 df-2o ⊢ 2 𝑜 = suc ⁡ 1 𝑜
11 9 10 breqtrdi ⊢ X ∈ P ∧ P ≈ 2 𝑜 → P ≈ suc ⁡ 1 𝑜
12 dif1en ⊢ 1 𝑜 ∈ ω ∧ P ≈ suc ⁡ 1 𝑜 ∧ X ∈ P → P ∖ X ≈ 1 𝑜
13 8 11 7 12 mp3an2i ⊢ X ∈ P ∧ P ≈ 2 𝑜 → P ∖ X ≈ 1 𝑜
14 en1uniel ⊢ P ∖ X ≈ 1 𝑜 → ⋃ P ∖ X ∈ P ∖ X
15 13 14 syl ⊢ X ∈ P ∧ P ≈ 2 𝑜 → ⋃ P ∖ X ∈ P ∖ X
16 eldifsn ⊢ ⋃ P ∖ X ∈ P ∖ X ↔ ⋃ P ∖ X ∈ P ∧ ⋃ P ∖ X ≠ X
17 15 16 sylib ⊢ X ∈ P ∧ P ≈ 2 𝑜 → ⋃ P ∖ X ∈ P ∧ ⋃ P ∖ X ≠ X
18 17 simpld ⊢ X ∈ P ∧ P ≈ 2 𝑜 → ⋃ P ∖ X ∈ P
19 7 18 prssd ⊢ X ∈ P ∧ P ≈ 2 𝑜 → X ⋃ P ∖ X ⊆ P
20 17 simprd ⊢ X ∈ P ∧ P ≈ 2 𝑜 → ⋃ P ∖ X ≠ X
21 20 necomd ⊢ X ∈ P ∧ P ≈ 2 𝑜 → X ≠ ⋃ P ∖ X
22 pr2nelem ⊢ X ∈ P ∧ ⋃ P ∖ X ∈ P ∧ X ≠ ⋃ P ∖ X → X ⋃ P ∖ X ≈ 2 𝑜
23 7 18 21 22 syl3anc ⊢ X ∈ P ∧ P ≈ 2 𝑜 → X ⋃ P ∖ X ≈ 2 𝑜
24 ensym ⊢ P ≈ 2 𝑜 → 2 𝑜 ≈ P
25 24 adantl ⊢ X ∈ P ∧ P ≈ 2 𝑜 → 2 𝑜 ≈ P
26 entr ⊢ X ⋃ P ∖ X ≈ 2 𝑜 ∧ 2 𝑜 ≈ P → X ⋃ P ∖ X ≈ P
27 23 25 26 syl2anc ⊢ X ∈ P ∧ P ≈ 2 𝑜 → X ⋃ P ∖ X ≈ P
28 fisseneq ⊢ P ∈ Fin ∧ X ⋃ P ∖ X ⊆ P ∧ X ⋃ P ∖ X ≈ P → X ⋃ P ∖ X = P
29 6 19 27 28 syl3anc ⊢ X ∈ P ∧ P ≈ 2 𝑜 → X ⋃ P ∖ X = P
30 29 eqcomd ⊢ X ∈ P ∧ P ≈ 2 𝑜 → P = X ⋃ P ∖ X