This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 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 )