Metamath Proof Explorer


Theorem dif1enALT

Description: Alternate proof of dif1en with fewer symbols using ax-pow . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Stefan O'Rear, 16-Aug-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dif1enALT
|- ( ( 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 )