Metamath Proof Explorer


Theorem en2other2

Description: Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Assertion en2other2
|- ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { U. ( P \ { X } ) } ) = X )

Proof

Step Hyp Ref Expression
1 en2eleq
 |-  ( ( X e. P /\ P ~~ 2o ) -> P = { X , U. ( P \ { X } ) } )
2 prcom
 |-  { X , U. ( P \ { X } ) } = { U. ( P \ { X } ) , X }
3 1 2 eqtrdi
 |-  ( ( X e. P /\ P ~~ 2o ) -> P = { U. ( P \ { X } ) , X } )
4 3 difeq1d
 |-  ( ( X e. P /\ P ~~ 2o ) -> ( P \ { U. ( P \ { X } ) } ) = ( { U. ( P \ { X } ) , X } \ { U. ( P \ { X } ) } ) )
5 difprsnss
 |-  ( { U. ( P \ { X } ) , X } \ { U. ( P \ { X } ) } ) C_ { X }
6 4 5 eqsstrdi
 |-  ( ( X e. P /\ P ~~ 2o ) -> ( P \ { U. ( P \ { X } ) } ) C_ { X } )
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 dif1en
 |-  ( ( 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 eldifsni
 |-  ( U. ( P \ { X } ) e. ( P \ { X } ) -> U. ( P \ { X } ) =/= X )
16 13 14 15 3syl
 |-  ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { X } ) =/= X )
17 16 necomd
 |-  ( ( X e. P /\ P ~~ 2o ) -> X =/= U. ( P \ { X } ) )
18 eldifsn
 |-  ( X e. ( P \ { U. ( P \ { X } ) } ) <-> ( X e. P /\ X =/= U. ( P \ { X } ) ) )
19 7 17 18 sylanbrc
 |-  ( ( X e. P /\ P ~~ 2o ) -> X e. ( P \ { U. ( P \ { X } ) } ) )
20 19 snssd
 |-  ( ( X e. P /\ P ~~ 2o ) -> { X } C_ ( P \ { U. ( P \ { X } ) } ) )
21 6 20 eqssd
 |-  ( ( X e. P /\ P ~~ 2o ) -> ( P \ { U. ( P \ { X } ) } ) = { X } )
22 21 unieqd
 |-  ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { U. ( P \ { X } ) } ) = U. { X } )
23 unisng
 |-  ( X e. P -> U. { X } = X )
24 23 adantr
 |-  ( ( X e. P /\ P ~~ 2o ) -> U. { X } = X )
25 22 24 eqtrd
 |-  ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { U. ( P \ { X } ) } ) = X )