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 e. P /\ P ~~ 2o ) -> P = { X , U. ( P \ { X } ) } )

Proof

Step Hyp Ref Expression
1 2onn 
 |-  2o e. _om
2 nnfi 
 |-  ( 2o e. _om -> 2o e. Fin )
3 1 2 ax-mp 
 |-  2o e. Fin
4 enfi 
 |-  ( P ~~ 2o -> ( P e. Fin <-> 2o e. Fin ) )
5 3 4 mpbiri 
 |-  ( P ~~ 2o -> P e. Fin )
6 5 adantl 
 |-  ( ( X e. P /\ P ~~ 2o ) -> P e. Fin )
7 simpl 
 |-  ( ( X e. P /\ P ~~ 2o ) -> X e. P )
8 1onn 
 |-  1o e. _om
9 simpr 
 |-  ( ( X e. P /\ P ~~ 2o ) -> P ~~ 2o )
10 df-2o 
 |-  2o = suc 1o
11 9 10 breqtrdi 
 |-  ( ( X e. P /\ P ~~ 2o ) -> P ~~ suc 1o )
12 dif1ennn 
 |-  ( ( 1o e. _om /\ P ~~ suc 1o /\ X e. P ) -> ( P \ { X } ) ~~ 1o )
13 8 11 7 12 mp3an2i 
 |-  ( ( X e. P /\ P ~~ 2o ) -> ( P \ { X } ) ~~ 1o )
14 en1uniel 
 |-  ( ( P \ { X } ) ~~ 1o -> U. ( P \ { X } ) e. ( P \ { X } ) )
15 13 14 syl 
 |-  ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { X } ) e. ( P \ { X } ) )
16 eldifsn 
 |-  ( U. ( P \ { X } ) e. ( P \ { X } ) <-> ( U. ( P \ { X } ) e. P /\ U. ( P \ { X } ) =/= X ) )
17 15 16 sylib 
 |-  ( ( X e. P /\ P ~~ 2o ) -> ( U. ( P \ { X } ) e. P /\ U. ( P \ { X } ) =/= X ) )
18 17 simpld 
 |-  ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { X } ) e. P )
19 7 18 prssd 
 |-  ( ( X e. P /\ P ~~ 2o ) -> { X , U. ( P \ { X } ) } C_ P )
20 17 simprd 
 |-  ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { X } ) =/= X )
21 20 necomd 
 |-  ( ( X e. P /\ P ~~ 2o ) -> X =/= U. ( P \ { X } ) )
22 enpr2 
 |-  ( ( X e. P /\ U. ( P \ { X } ) e. P /\ X =/= U. ( P \ { X } ) ) -> { X , U. ( P \ { X } ) } ~~ 2o )
23 7 18 21 22 syl3anc 
 |-  ( ( X e. P /\ P ~~ 2o ) -> { X , U. ( P \ { X } ) } ~~ 2o )
24 ensym 
 |-  ( P ~~ 2o -> 2o ~~ P )
25 24 adantl 
 |-  ( ( X e. P /\ P ~~ 2o ) -> 2o ~~ P )
26 entr 
 |-  ( ( { X , U. ( P \ { X } ) } ~~ 2o /\ 2o ~~ P ) -> { X , U. ( P \ { X } ) } ~~ P )
27 23 25 26 syl2anc 
 |-  ( ( X e. P /\ P ~~ 2o ) -> { X , U. ( P \ { X } ) } ~~ P )
28 fisseneq 
 |-  ( ( P e. Fin /\ { X , U. ( P \ { X } ) } C_ P /\ { X , U. ( P \ { X } ) } ~~ P ) -> { X , U. ( P \ { X } ) } = P )
29 6 19 27 28 syl3anc 
 |-  ( ( X e. P /\ P ~~ 2o ) -> { X , U. ( P \ { X } ) } = P )
30 29 eqcomd 
 |-  ( ( X e. P /\ P ~~ 2o ) -> P = { X , U. ( P \ { X } ) } )