Metamath Proof Explorer

Theorem dif1en

Description: If a set A is equinumerous to the successor of a natural number M , then A with an element removed is equinumerous to M . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Assertion dif1en 
|- ( ( M e. _om /\ A ~~ suc M /\ X e. A ) -> ( A \ { X } ) ~~ M )

Proof

Step Hyp Ref Expression
1 peano2 
 |-  ( M e. _om -> suc M e. _om )
2 breq2 
 |-  ( x = suc M -> ( A ~~ x <-> A ~~ suc M ) )
3 2 rspcev 
 |-  ( ( suc M e. _om /\ A ~~ suc M ) -> E. x e. _om A ~~ x )
4 isfi 
 |-  ( A e. Fin <-> E. x e. _om A ~~ x )
5 3 4 sylibr 
 |-  ( ( suc M e. _om /\ A ~~ suc M ) -> A e. Fin )
6 1 5 sylan 
 |-  ( ( M e. _om /\ A ~~ suc M ) -> A e. Fin )
7 diffi 
 |-  ( A e. Fin -> ( A \ { X } ) e. Fin )
8 isfi 
 |-  ( ( A \ { X } ) e. Fin <-> E. x e. _om ( A \ { X } ) ~~ x )
9 7 8 sylib 
 |-  ( A e. Fin -> E. x e. _om ( A \ { X } ) ~~ x )
10 6 9 syl 
 |-  ( ( M e. _om /\ A ~~ suc M ) -> E. x e. _om ( A \ { X } ) ~~ x )
11 10 3adant3 
 |-  ( ( M e. _om /\ A ~~ suc M /\ X e. A ) -> E. x e. _om ( A \ { X } ) ~~ x )
12 en2sn 
 |-  ( ( X e. A /\ x e. _V ) -> { X } ~~ { x } )
13 12 elvd 
 |-  ( X e. A -> { X } ~~ { x } )
14 nnord 
 |-  ( x e. _om -> Ord x )
15 orddisj 
 |-  ( Ord x -> ( x i^i { x } ) = (/) )
16 14 15 syl 
 |-  ( x e. _om -> ( x i^i { x } ) = (/) )
17 incom 
 |-  ( ( A \ { X } ) i^i { X } ) = ( { X } i^i ( A \ { X } ) )
18 disjdif 
 |-  ( { X } i^i ( A \ { X } ) ) = (/)
19 17 18 eqtri 
 |-  ( ( A \ { X } ) i^i { X } ) = (/)
20 unen 
 |-  ( ( ( ( A \ { X } ) ~~ x /\ { X } ~~ { x } ) /\ ( ( ( A \ { X } ) i^i { X } ) = (/) /\ ( x i^i { x } ) = (/) ) ) -> ( ( A \ { X } ) u. { X } ) ~~ ( x u. { x } ) )
21 20 an4s 
 |-  ( ( ( ( A \ { X } ) ~~ x /\ ( ( A \ { X } ) i^i { X } ) = (/) ) /\ ( { X } ~~ { x } /\ ( x i^i { x } ) = (/) ) ) -> ( ( A \ { X } ) u. { X } ) ~~ ( x u. { x } ) )
22 19 21 mpanl2 
 |-  ( ( ( A \ { X } ) ~~ x /\ ( { X } ~~ { x } /\ ( x i^i { x } ) = (/) ) ) -> ( ( A \ { X } ) u. { X } ) ~~ ( x u. { x } ) )
23 22 expcom 
 |-  ( ( { X } ~~ { x } /\ ( x i^i { x } ) = (/) ) -> ( ( A \ { X } ) ~~ x -> ( ( A \ { X } ) u. { X } ) ~~ ( x u. { x } ) ) )
24 13 16 23 syl2an 
 |-  ( ( X e. A /\ x e. _om ) -> ( ( A \ { X } ) ~~ x -> ( ( A \ { X } ) u. { X } ) ~~ ( x u. { x } ) ) )
25 24 3ad2antl3 
 |-  ( ( ( M e. _om /\ A ~~ suc M /\ X e. A ) /\ x e. _om ) -> ( ( A \ { X } ) ~~ x -> ( ( A \ { X } ) u. { X } ) ~~ ( x u. { x } ) ) )
26 difsnid 
 |-  ( X e. A -> ( ( A \ { X } ) u. { X } ) = A )
27 df-suc 
 |-  suc x = ( x u. { x } )
28 27 eqcomi 
 |-  ( x u. { x } ) = suc x
29 28 a1i 
 |-  ( X e. A -> ( x u. { x } ) = suc x )
30 26 29 breq12d 
 |-  ( X e. A -> ( ( ( A \ { X } ) u. { X } ) ~~ ( x u. { x } ) <-> A ~~ suc x ) )
31 30 3ad2ant3 
 |-  ( ( M e. _om /\ A ~~ suc M /\ X e. A ) -> ( ( ( A \ { X } ) u. { X } ) ~~ ( x u. { x } ) <-> A ~~ suc x ) )
32 31 adantr 
 |-  ( ( ( M e. _om /\ A ~~ suc M /\ X e. A ) /\ x e. _om ) -> ( ( ( A \ { X } ) u. { X } ) ~~ ( x u. { x } ) <-> A ~~ suc x ) )
33 ensym 
 |-  ( A ~~ suc M -> suc M ~~ A )
34 entr 
 |-  ( ( suc M ~~ A /\ A ~~ suc x ) -> suc M ~~ suc x )
35 peano2 
 |-  ( x e. _om -> suc x e. _om )
36 nneneq 
 |-  ( ( suc M e. _om /\ suc x e. _om ) -> ( suc M ~~ suc x <-> suc M = suc x ) )
37 35 36 sylan2 
 |-  ( ( suc M e. _om /\ x e. _om ) -> ( suc M ~~ suc x <-> suc M = suc x ) )
38 34 37 syl5ib 
 |-  ( ( suc M e. _om /\ x e. _om ) -> ( ( suc M ~~ A /\ A ~~ suc x ) -> suc M = suc x ) )
39 38 expd 
 |-  ( ( suc M e. _om /\ x e. _om ) -> ( suc M ~~ A -> ( A ~~ suc x -> suc M = suc x ) ) )
40 33 39 syl5 
 |-  ( ( suc M e. _om /\ x e. _om ) -> ( A ~~ suc M -> ( A ~~ suc x -> suc M = suc x ) ) )
41 1 40 sylan 
 |-  ( ( M e. _om /\ x e. _om ) -> ( A ~~ suc M -> ( A ~~ suc x -> suc M = suc x ) ) )
42 41 imp 
 |-  ( ( ( M e. _om /\ x e. _om ) /\ A ~~ suc M ) -> ( A ~~ suc x -> suc M = suc x ) )
43 42 an32s 
 |-  ( ( ( M e. _om /\ A ~~ suc M ) /\ x e. _om ) -> ( A ~~ suc x -> suc M = suc x ) )
44 43 3adantl3 
 |-  ( ( ( M e. _om /\ A ~~ suc M /\ X e. A ) /\ x e. _om ) -> ( A ~~ suc x -> suc M = suc x ) )
45 32 44 sylbid 
 |-  ( ( ( M e. _om /\ A ~~ suc M /\ X e. A ) /\ x e. _om ) -> ( ( ( A \ { X } ) u. { X } ) ~~ ( x u. { x } ) -> suc M = suc x ) )
46 peano4 
 |-  ( ( M e. _om /\ x e. _om ) -> ( suc M = suc x <-> M = x ) )
47 46 biimpd 
 |-  ( ( M e. _om /\ x e. _om ) -> ( suc M = suc x -> M = x ) )
48 47 3ad2antl1 
 |-  ( ( ( M e. _om /\ A ~~ suc M /\ X e. A ) /\ x e. _om ) -> ( suc M = suc x -> M = x ) )
49 25 45 48 3syld 
 |-  ( ( ( M e. _om /\ A ~~ suc M /\ X e. A ) /\ x e. _om ) -> ( ( A \ { X } ) ~~ x -> M = x ) )
50 breq2 
 |-  ( M = x -> ( ( A \ { X } ) ~~ M <-> ( A \ { X } ) ~~ x ) )
51 50 biimprcd 
 |-  ( ( A \ { X } ) ~~ x -> ( M = x -> ( A \ { X } ) ~~ M ) )
52 49 51 sylcom 
 |-  ( ( ( M e. _om /\ A ~~ suc M /\ X e. A ) /\ x e. _om ) -> ( ( A \ { X } ) ~~ x -> ( A \ { X } ) ~~ M ) )
53 52 rexlimdva 
 |-  ( ( M e. _om /\ A ~~ suc M /\ X e. A ) -> ( E. x e. _om ( A \ { X } ) ~~ x -> ( A \ { X } ) ~~ M ) )
54 11 53 mpd 
 |-  ( ( M e. _om /\ A ~~ suc M /\ X e. A ) -> ( A \ { X } ) ~~ M )