Metamath Proof Explorer

Theorem unidifsnne

Description: The other element of a pair is not the known element. (Contributed by Thierry Arnoux, 26-Aug-2017)

Ref Expression
Assertion unidifsnne 
|- ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { X } ) =/= 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 diffi 
 |-  ( P e. Fin -> ( P \ { X } ) e. Fin )
8 6 7 syl 
 |-  ( ( X e. P /\ P ~~ 2o ) -> ( P \ { X } ) e. Fin )
9 8 cardidd 
 |-  ( ( X e. P /\ P ~~ 2o ) -> ( card ` ( P \ { X } ) ) ~~ ( P \ { X } ) )
10 9 ensymd 
 |-  ( ( X e. P /\ P ~~ 2o ) -> ( P \ { X } ) ~~ ( card ` ( P \ { X } ) ) )
11 simpl 
 |-  ( ( X e. P /\ P ~~ 2o ) -> X e. P )
12 dif1card 
 |-  ( ( P e. Fin /\ X e. P ) -> ( card ` P ) = suc ( card ` ( P \ { X } ) ) )
13 6 11 12 syl2anc 
 |-  ( ( X e. P /\ P ~~ 2o ) -> ( card ` P ) = suc ( card ` ( P \ { X } ) ) )
14 cardennn 
 |-  ( ( P ~~ 2o /\ 2o e. _om ) -> ( card ` P ) = 2o )
15 1 14 mpan2 
 |-  ( P ~~ 2o -> ( card ` P ) = 2o )
16 df-2o 
 |-  2o = suc 1o
17 15 16 eqtrdi 
 |-  ( P ~~ 2o -> ( card ` P ) = suc 1o )
18 17 adantl 
 |-  ( ( X e. P /\ P ~~ 2o ) -> ( card ` P ) = suc 1o )
19 13 18 eqtr3d 
 |-  ( ( X e. P /\ P ~~ 2o ) -> suc ( card ` ( P \ { X } ) ) = suc 1o )
20 suc11reg 
 |-  ( suc ( card ` ( P \ { X } ) ) = suc 1o <-> ( card ` ( P \ { X } ) ) = 1o )
21 19 20 sylib 
 |-  ( ( X e. P /\ P ~~ 2o ) -> ( card ` ( P \ { X } ) ) = 1o )
22 10 21 breqtrd 
 |-  ( ( X e. P /\ P ~~ 2o ) -> ( P \ { X } ) ~~ 1o )
23 en1 
 |-  ( ( P \ { X } ) ~~ 1o <-> E. x ( P \ { X } ) = { x } )
24 22 23 sylib 
 |-  ( ( X e. P /\ P ~~ 2o ) -> E. x ( P \ { X } ) = { x } )
25 simplll 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> X e. P )
26 25 elexd 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> X e. _V )
27 simplr 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> ( P \ { X } ) = { x } )
28 sneqbg 
 |-  ( X e. P -> ( { X } = { x } <-> X = x ) )
29 28 biimpar 
 |-  ( ( X e. P /\ X = x ) -> { X } = { x } )
30 29 ad4ant14 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> { X } = { x } )
31 27 30 eqtr4d 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> ( P \ { X } ) = { X } )
32 31 ineq2d 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> ( { X } i^i ( P \ { X } ) ) = ( { X } i^i { X } ) )
33 disjdif 
 |-  ( { X } i^i ( P \ { X } ) ) = (/)
34 inidm 
 |-  ( { X } i^i { X } ) = { X }
35 32 33 34 3eqtr3g 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> (/) = { X } )
36 35 eqcomd 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> { X } = (/) )
37 snprc 
 |-  ( -. X e. _V <-> { X } = (/) )
38 36 37 sylibr 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> -. X e. _V )
39 26 38 pm2.65da 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> -. X = x )
40 39 neqned 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> X =/= x )
41 simpr 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> ( P \ { X } ) = { x } )
42 41 unieqd 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> U. ( P \ { X } ) = U. { x } )
43 vex 
 |-  x e. _V
44 43 unisn 
 |-  U. { x } = x
45 42 44 eqtrdi 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> U. ( P \ { X } ) = x )
46 40 45 neeqtrrd 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> X =/= U. ( P \ { X } ) )
47 46 necomd 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> U. ( P \ { X } ) =/= X )
48 24 47 exlimddv 
 |-  ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { X } ) =/= X )