Metamath Proof Explorer

Theorem unidifsnne

Description: The other element of a pair is not the known element. (Contributed by Thierry Arnoux, 26-Aug-2017) Remove dependency on ax-reg . (Revised by Timothy J. O'Malley, 15-Oct-2026)

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 cardon 
 |-  ( card ` ( P \ { X } ) ) e. On
21 1on 
 |-  1o e. On
22 suc11 
 |-  ( ( ( card ` ( P \ { X } ) ) e. On /\ 1o e. On ) -> ( suc ( card ` ( P \ { X } ) ) = suc 1o <-> ( card ` ( P \ { X } ) ) = 1o ) )
23 20 21 22 mp2an 
 |-  ( suc ( card ` ( P \ { X } ) ) = suc 1o <-> ( card ` ( P \ { X } ) ) = 1o )
24 19 23 sylib 
 |-  ( ( X e. P /\ P ~~ 2o ) -> ( card ` ( P \ { X } ) ) = 1o )
25 10 24 breqtrd 
 |-  ( ( X e. P /\ P ~~ 2o ) -> ( P \ { X } ) ~~ 1o )
26 en1 
 |-  ( ( P \ { X } ) ~~ 1o <-> E. x ( P \ { X } ) = { x } )
27 25 26 sylib 
 |-  ( ( X e. P /\ P ~~ 2o ) -> E. x ( P \ { X } ) = { x } )
28 simplll 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> X e. P )
29 28 elexd 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> X e. _V )
30 simplr 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> ( P \ { X } ) = { x } )
31 sneqbg 
 |-  ( X e. P -> ( { X } = { x } <-> X = x ) )
32 31 biimpar 
 |-  ( ( X e. P /\ X = x ) -> { X } = { x } )
33 32 ad4ant14 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> { X } = { x } )
34 30 33 eqtr4d 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> ( P \ { X } ) = { X } )
35 34 ineq2d 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> ( { X } i^i ( P \ { X } ) ) = ( { X } i^i { X } ) )
36 disjdif 
 |-  ( { X } i^i ( P \ { X } ) ) = (/)
37 inidm 
 |-  ( { X } i^i { X } ) = { X }
38 35 36 37 3eqtr3g 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> (/) = { X } )
39 38 eqcomd 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> { X } = (/) )
40 snprc 
 |-  ( -. X e. _V <-> { X } = (/) )
41 39 40 sylibr 
 |-  ( ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) /\ X = x ) -> -. X e. _V )
42 29 41 pm2.65da 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> -. X = x )
43 42 neqned 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> X =/= x )
44 simpr 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> ( P \ { X } ) = { x } )
45 44 unieqd 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> U. ( P \ { X } ) = U. { x } )
46 unisnv 
 |-  U. { x } = x
47 45 46 eqtrdi 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> U. ( P \ { X } ) = x )
48 43 47 neeqtrrd 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> X =/= U. ( P \ { X } ) )
49 48 necomd 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> U. ( P \ { X } ) =/= X )
50 27 49 exlimddv 
 |-  ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { X } ) =/= X )