Metamath Proof Explorer

Theorem nneneq

Description: Two equinumerous natural numbers are equal. Proposition 10.20 of TakeutiZaring p. 90 and its converse. Also compare Corollary 6E of Enderton p. 136. (Contributed by NM, 28-May-1998)

Ref Expression
Assertion nneneq 
|- ( ( A e. _om /\ B e. _om ) -> ( A ~~ B <-> A = B ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( x = (/) -> ( x ~~ z <-> (/) ~~ z ) )
2 eqeq1 
 |-  ( x = (/) -> ( x = z <-> (/) = z ) )
3 1 2 imbi12d 
 |-  ( x = (/) -> ( ( x ~~ z -> x = z ) <-> ( (/) ~~ z -> (/) = z ) ) )
4 3 ralbidv 
 |-  ( x = (/) -> ( A. z e. _om ( x ~~ z -> x = z ) <-> A. z e. _om ( (/) ~~ z -> (/) = z ) ) )
5 breq1 
 |-  ( x = y -> ( x ~~ z <-> y ~~ z ) )
6 eqeq1 
 |-  ( x = y -> ( x = z <-> y = z ) )
7 5 6 imbi12d 
 |-  ( x = y -> ( ( x ~~ z -> x = z ) <-> ( y ~~ z -> y = z ) ) )
8 7 ralbidv 
 |-  ( x = y -> ( A. z e. _om ( x ~~ z -> x = z ) <-> A. z e. _om ( y ~~ z -> y = z ) ) )
9 breq1 
 |-  ( x = suc y -> ( x ~~ z <-> suc y ~~ z ) )
10 eqeq1 
 |-  ( x = suc y -> ( x = z <-> suc y = z ) )
11 9 10 imbi12d 
 |-  ( x = suc y -> ( ( x ~~ z -> x = z ) <-> ( suc y ~~ z -> suc y = z ) ) )
12 11 ralbidv 
 |-  ( x = suc y -> ( A. z e. _om ( x ~~ z -> x = z ) <-> A. z e. _om ( suc y ~~ z -> suc y = z ) ) )
13 breq1 
 |-  ( x = A -> ( x ~~ z <-> A ~~ z ) )
14 eqeq1 
 |-  ( x = A -> ( x = z <-> A = z ) )
15 13 14 imbi12d 
 |-  ( x = A -> ( ( x ~~ z -> x = z ) <-> ( A ~~ z -> A = z ) ) )
16 15 ralbidv 
 |-  ( x = A -> ( A. z e. _om ( x ~~ z -> x = z ) <-> A. z e. _om ( A ~~ z -> A = z ) ) )
17 ensym 
 |-  ( (/) ~~ z -> z ~~ (/) )
18 en0 
 |-  ( z ~~ (/) <-> z = (/) )
19 eqcom 
 |-  ( z = (/) <-> (/) = z )
20 18 19 bitri 
 |-  ( z ~~ (/) <-> (/) = z )
21 17 20 sylib 
 |-  ( (/) ~~ z -> (/) = z )
22 21 rgenw 
 |-  A. z e. _om ( (/) ~~ z -> (/) = z )
23 nn0suc 
 |-  ( w e. _om -> ( w = (/) \/ E. z e. _om w = suc z ) )
24 en0 
 |-  ( suc y ~~ (/) <-> suc y = (/) )
25 breq2 
 |-  ( w = (/) -> ( suc y ~~ w <-> suc y ~~ (/) ) )
26 eqeq2 
 |-  ( w = (/) -> ( suc y = w <-> suc y = (/) ) )
27 25 26 bibi12d 
 |-  ( w = (/) -> ( ( suc y ~~ w <-> suc y = w ) <-> ( suc y ~~ (/) <-> suc y = (/) ) ) )
28 24 27 mpbiri 
 |-  ( w = (/) -> ( suc y ~~ w <-> suc y = w ) )
29 28 biimpd 
 |-  ( w = (/) -> ( suc y ~~ w -> suc y = w ) )
30 29 a1i 
 |-  ( ( y e. _om /\ A. z e. _om ( y ~~ z -> y = z ) ) -> ( w = (/) -> ( suc y ~~ w -> suc y = w ) ) )
31 nfv 
 |-  F/ z y e. _om
32 nfra1 
 |-  F/ z A. z e. _om ( y ~~ z -> y = z )
33 31 32 nfan 
 |-  F/ z ( y e. _om /\ A. z e. _om ( y ~~ z -> y = z ) )
34 nfv 
 |-  F/ z ( suc y ~~ w -> suc y = w )
35 vex 
 |-  y e. _V
36 vex 
 |-  z e. _V
37 35 36 phplem4 
 |-  ( ( y e. _om /\ z e. _om ) -> ( suc y ~~ suc z -> y ~~ z ) )
38 37 imim1d 
 |-  ( ( y e. _om /\ z e. _om ) -> ( ( y ~~ z -> y = z ) -> ( suc y ~~ suc z -> y = z ) ) )
39 38 ex 
 |-  ( y e. _om -> ( z e. _om -> ( ( y ~~ z -> y = z ) -> ( suc y ~~ suc z -> y = z ) ) ) )
40 39 a2d 
 |-  ( y e. _om -> ( ( z e. _om -> ( y ~~ z -> y = z ) ) -> ( z e. _om -> ( suc y ~~ suc z -> y = z ) ) ) )
41 rsp 
 |-  ( A. z e. _om ( y ~~ z -> y = z ) -> ( z e. _om -> ( y ~~ z -> y = z ) ) )
42 40 41 impel 
 |-  ( ( y e. _om /\ A. z e. _om ( y ~~ z -> y = z ) ) -> ( z e. _om -> ( suc y ~~ suc z -> y = z ) ) )
43 suceq 
 |-  ( y = z -> suc y = suc z )
44 42 43 syl8 
 |-  ( ( y e. _om /\ A. z e. _om ( y ~~ z -> y = z ) ) -> ( z e. _om -> ( suc y ~~ suc z -> suc y = suc z ) ) )
45 breq2 
 |-  ( w = suc z -> ( suc y ~~ w <-> suc y ~~ suc z ) )
46 eqeq2 
 |-  ( w = suc z -> ( suc y = w <-> suc y = suc z ) )
47 45 46 imbi12d 
 |-  ( w = suc z -> ( ( suc y ~~ w -> suc y = w ) <-> ( suc y ~~ suc z -> suc y = suc z ) ) )
48 47 biimprcd 
 |-  ( ( suc y ~~ suc z -> suc y = suc z ) -> ( w = suc z -> ( suc y ~~ w -> suc y = w ) ) )
49 44 48 syl6 
 |-  ( ( y e. _om /\ A. z e. _om ( y ~~ z -> y = z ) ) -> ( z e. _om -> ( w = suc z -> ( suc y ~~ w -> suc y = w ) ) ) )
50 33 34 49 rexlimd 
 |-  ( ( y e. _om /\ A. z e. _om ( y ~~ z -> y = z ) ) -> ( E. z e. _om w = suc z -> ( suc y ~~ w -> suc y = w ) ) )
51 30 50 jaod 
 |-  ( ( y e. _om /\ A. z e. _om ( y ~~ z -> y = z ) ) -> ( ( w = (/) \/ E. z e. _om w = suc z ) -> ( suc y ~~ w -> suc y = w ) ) )
52 51 ex 
 |-  ( y e. _om -> ( A. z e. _om ( y ~~ z -> y = z ) -> ( ( w = (/) \/ E. z e. _om w = suc z ) -> ( suc y ~~ w -> suc y = w ) ) ) )
53 23 52 syl7 
 |-  ( y e. _om -> ( A. z e. _om ( y ~~ z -> y = z ) -> ( w e. _om -> ( suc y ~~ w -> suc y = w ) ) ) )
54 53 ralrimdv 
 |-  ( y e. _om -> ( A. z e. _om ( y ~~ z -> y = z ) -> A. w e. _om ( suc y ~~ w -> suc y = w ) ) )
55 breq2 
 |-  ( w = z -> ( suc y ~~ w <-> suc y ~~ z ) )
56 eqeq2 
 |-  ( w = z -> ( suc y = w <-> suc y = z ) )
57 55 56 imbi12d 
 |-  ( w = z -> ( ( suc y ~~ w -> suc y = w ) <-> ( suc y ~~ z -> suc y = z ) ) )
58 57 cbvralvw 
 |-  ( A. w e. _om ( suc y ~~ w -> suc y = w ) <-> A. z e. _om ( suc y ~~ z -> suc y = z ) )
59 54 58 syl6ib 
 |-  ( y e. _om -> ( A. z e. _om ( y ~~ z -> y = z ) -> A. z e. _om ( suc y ~~ z -> suc y = z ) ) )
60 4 8 12 16 22 59 finds 
 |-  ( A e. _om -> A. z e. _om ( A ~~ z -> A = z ) )
61 breq2 
 |-  ( z = B -> ( A ~~ z <-> A ~~ B ) )
62 eqeq2 
 |-  ( z = B -> ( A = z <-> A = B ) )
63 61 62 imbi12d 
 |-  ( z = B -> ( ( A ~~ z -> A = z ) <-> ( A ~~ B -> A = B ) ) )
64 63 rspcv 
 |-  ( B e. _om -> ( A. z e. _om ( A ~~ z -> A = z ) -> ( A ~~ B -> A = B ) ) )
65 60 64 mpan9 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A ~~ B -> A = B ) )
66 eqeng 
 |-  ( A e. _om -> ( A = B -> A ~~ B ) )
67 66 adantr 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A = B -> A ~~ B ) )
68 65 67 impbid 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A ~~ B <-> A = B ) )