Metamath Proof Explorer

Theorem rexdif1en

Description: If a set is equinumerous to a nonzero ordinal, then there exists an element in that set such that removing it leaves the set equinumerous to the predecessor of that ordinal. (Contributed by BTernaryTau, 26-Aug-2024) Generalize to all ordinals and avoid ax-un . (Revised by BTernaryTau, 5-Jan-2025)

Ref Expression
Assertion rexdif1en 
|- ( ( M e. On /\ A ~~ suc M ) -> E. x e. A ( A \ { x } ) ~~ M )

Proof

Step Hyp Ref Expression
1 encv 
 |-  ( A ~~ suc M -> ( A e. _V /\ suc M e. _V ) )
2 1 simpld 
 |-  ( A ~~ suc M -> A e. _V )
3 breng 
 |-  ( ( A e. _V /\ suc M e. _V ) -> ( A ~~ suc M <-> E. f f : A -1-1-onto-> suc M ) )
4 1 3 syl 
 |-  ( A ~~ suc M -> ( A ~~ suc M <-> E. f f : A -1-1-onto-> suc M ) )
5 4 ibi 
 |-  ( A ~~ suc M -> E. f f : A -1-1-onto-> suc M )
6 sucidg 
 |-  ( M e. On -> M e. suc M )
7 f1ocnvdm 
 |-  ( ( f : A -1-1-onto-> suc M /\ M e. suc M ) -> ( `' f ` M ) e. A )
8 7 ancoms 
 |-  ( ( M e. suc M /\ f : A -1-1-onto-> suc M ) -> ( `' f ` M ) e. A )
9 6 8 sylan 
 |-  ( ( M e. On /\ f : A -1-1-onto-> suc M ) -> ( `' f ` M ) e. A )
10 9 adantll 
 |-  ( ( ( A e. _V /\ M e. On ) /\ f : A -1-1-onto-> suc M ) -> ( `' f ` M ) e. A )
11 vex 
 |-  f e. _V
12 dif1enlem 
 |-  ( ( ( f e. _V /\ A e. _V /\ M e. On ) /\ f : A -1-1-onto-> suc M ) -> ( A \ { ( `' f ` M ) } ) ~~ M )
13 11 12 mp3anl1 
 |-  ( ( ( A e. _V /\ M e. On ) /\ f : A -1-1-onto-> suc M ) -> ( A \ { ( `' f ` M ) } ) ~~ M )
14 sneq 
 |-  ( x = ( `' f ` M ) -> { x } = { ( `' f ` M ) } )
15 14 difeq2d 
 |-  ( x = ( `' f ` M ) -> ( A \ { x } ) = ( A \ { ( `' f ` M ) } ) )
16 15 breq1d 
 |-  ( x = ( `' f ` M ) -> ( ( A \ { x } ) ~~ M <-> ( A \ { ( `' f ` M ) } ) ~~ M ) )
17 16 rspcev 
 |-  ( ( ( `' f ` M ) e. A /\ ( A \ { ( `' f ` M ) } ) ~~ M ) -> E. x e. A ( A \ { x } ) ~~ M )
18 10 13 17 syl2anc 
 |-  ( ( ( A e. _V /\ M e. On ) /\ f : A -1-1-onto-> suc M ) -> E. x e. A ( A \ { x } ) ~~ M )
19 18 ex 
 |-  ( ( A e. _V /\ M e. On ) -> ( f : A -1-1-onto-> suc M -> E. x e. A ( A \ { x } ) ~~ M ) )
20 19 exlimdv 
 |-  ( ( A e. _V /\ M e. On ) -> ( E. f f : A -1-1-onto-> suc M -> E. x e. A ( A \ { x } ) ~~ M ) )
21 5 20 syl5 
 |-  ( ( A e. _V /\ M e. On ) -> ( A ~~ suc M -> E. x e. A ( A \ { x } ) ~~ M ) )
22 2 21 sylan 
 |-  ( ( A ~~ suc M /\ M e. On ) -> ( A ~~ suc M -> E. x e. A ( A \ { x } ) ~~ M ) )
23 22 ancoms 
 |-  ( ( M e. On /\ A ~~ suc M ) -> ( A ~~ suc M -> E. x e. A ( A \ { x } ) ~~ M ) )
24 23 syldbl2 
 |-  ( ( M e. On /\ A ~~ suc M ) -> E. x e. A ( A \ { x } ) ~~ M )