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 ( ( 𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o ) → 𝑃 = { 𝑋 , ∪ ( 𝑃 ∖ { 𝑋 } ) } )

Proof

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