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 ω A suc M X A A X M

Proof

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