Theorem rexdif1en

Description: If a set is equinumerous to a nonzero finite 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)

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

Proof

Step	Hyp	Ref	Expression
1		bren	|- ( A ~~ suc M <-> E. f f : A -1-1-onto-> suc M )
2		19.42v	|- ( E. f ( M e. _om /\ f : A -1-1-onto-> suc M ) <-> ( M e. _om /\ E. f f : A -1-1-onto-> suc M ) )
3		sucidg	|- ( M e. _om -> M e. suc M )
4		f1ocnvdm	|- ( ( f : A -1-1-onto-> suc M /\ M e. suc M ) -> ( `' f ` M ) e. A )
5	4	ancoms	|- ( ( M e. suc M /\ f : A -1-1-onto-> suc M ) -> ( `' f ` M ) e. A )
6	3 5	sylan	|- ( ( M e. _om /\ f : A -1-1-onto-> suc M ) -> ( `' f ` M ) e. A )
7		vex	|- f e. _V
8		dif1enlem	|- ( ( f e. _V /\ M e. _om /\ f : A -1-1-onto-> suc M ) -> ( A \ { ( `' f ` M ) } ) ~~ M )
9	7 8	mp3an1	|- ( ( M e. _om /\ f : A -1-1-onto-> suc M ) -> ( A \ { ( `' f ` M ) } ) ~~ M )
10		sneq	|- ( x = ( `' f ` M ) -> { x } = { ( `' f ` M ) } )
11	10	difeq2d	|- ( x = ( `' f ` M ) -> ( A \ { x } ) = ( A \ { ( `' f ` M ) } ) )
12	11	breq1d	|- ( x = ( `' f ` M ) -> ( ( A \ { x } ) ~~ M <-> ( A \ { ( `' f ` M ) } ) ~~ M ) )
13	12	rspcev	|- ( ( ( `' f ` M ) e. A /\ ( A \ { ( `' f ` M ) } ) ~~ M ) -> E. x e. A ( A \ { x } ) ~~ M )
14	6 9 13	syl2anc	|- ( ( M e. _om /\ f : A -1-1-onto-> suc M ) -> E. x e. A ( A \ { x } ) ~~ M )
15	14	exlimiv	|- ( E. f ( M e. _om /\ f : A -1-1-onto-> suc M ) -> E. x e. A ( A \ { x } ) ~~ M )
16	2 15	sylbir	|- ( ( M e. _om /\ E. f f : A -1-1-onto-> suc M ) -> E. x e. A ( A \ { x } ) ~~ M )
17	1 16	sylan2b	|- ( ( M e. _om /\ A ~~ suc M ) -> E. x e. A ( A \ { x } ) ~~ M )