Metamath Proof Explorer

Theorem unidifsnel

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

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

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 simpr 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> ( P \ { X } ) = { x } )
26 25 unieqd 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> U. ( P \ { X } ) = U. { x } )
27 vex 
 |-  x e. _V
28 27 unisn 
 |-  U. { x } = x
29 26 28 eqtrdi 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> U. ( P \ { X } ) = x )
30 difssd 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> ( P \ { X } ) C_ P )
31 25 30 eqsstrrd 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> { x } C_ P )
32 vsnid 
 |-  x e. { x }
33 ssel2 
 |-  ( ( { x } C_ P /\ x e. { x } ) -> x e. P )
34 31 32 33 sylancl 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> x e. P )
35 29 34 eqeltrd 
 |-  ( ( ( X e. P /\ P ~~ 2o ) /\ ( P \ { X } ) = { x } ) -> U. ( P \ { X } ) e. P )
36 24 35 exlimddv 
 |-  ( ( X e. P /\ P ~~ 2o ) -> U. ( P \ { X } ) e. P )