This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) Avoid ax-pow . (Revised by BTernaryTau, 11-Nov-2024)

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 0fi 
 |-  (/) e. Fin
18 ensymfib 
 |-  ( (/) e. Fin -> ( (/) ~~ z <-> z ~~ (/) ) )
19 17 18 ax-mp 
 |-  ( (/) ~~ z <-> z ~~ (/) )
20 en0 
 |-  ( z ~~ (/) <-> z = (/) )
21 eqcom 
 |-  ( z = (/) <-> (/) = z )
22 20 21 bitri 
 |-  ( z ~~ (/) <-> (/) = z )
23 19 22 sylbb 
 |-  ( (/) ~~ z -> (/) = z )
24 23 rgenw 
 |-  A. z e. _om ( (/) ~~ z -> (/) = z )
25 nn0suc 
 |-  ( w e. _om -> ( w = (/) \/ E. z e. _om w = suc z ) )
26 en0 
 |-  ( suc y ~~ (/) <-> suc y = (/) )
27 breq2 
 |-  ( w = (/) -> ( suc y ~~ w <-> suc y ~~ (/) ) )
28 eqeq2 
 |-  ( w = (/) -> ( suc y = w <-> suc y = (/) ) )
29 27 28 bibi12d 
 |-  ( w = (/) -> ( ( suc y ~~ w <-> suc y = w ) <-> ( suc y ~~ (/) <-> suc y = (/) ) ) )
30 26 29 mpbiri 
 |-  ( w = (/) -> ( suc y ~~ w <-> suc y = w ) )
31 30 biimpd 
 |-  ( w = (/) -> ( suc y ~~ w -> suc y = w ) )
32 31 a1i 
 |-  ( ( y e. _om /\ A. z e. _om ( y ~~ z -> y = z ) ) -> ( w = (/) -> ( suc y ~~ w -> suc y = w ) ) )
33 nfv 
 |-  F/ z y e. _om
34 nfra1 
 |-  F/ z A. z e. _om ( y ~~ z -> y = z )
35 33 34 nfan 
 |-  F/ z ( y e. _om /\ A. z e. _om ( y ~~ z -> y = z ) )
36 nfv 
 |-  F/ z ( suc y ~~ w -> suc y = w )
37 vex 
 |-  y e. _V
38 37 phplem2 
 |-  ( ( y e. _om /\ z e. _om ) -> ( suc y ~~ suc z -> y ~~ z ) )
39 38 imim1d 
 |-  ( ( y e. _om /\ z e. _om ) -> ( ( y ~~ z -> y = z ) -> ( suc y ~~ suc z -> y = z ) ) )
40 39 ex 
 |-  ( y e. _om -> ( z e. _om -> ( ( y ~~ z -> y = z ) -> ( suc y ~~ suc z -> y = z ) ) ) )
41 40 a2d 
 |-  ( y e. _om -> ( ( z e. _om -> ( y ~~ z -> y = z ) ) -> ( z e. _om -> ( suc y ~~ suc z -> y = z ) ) ) )
42 rsp 
 |-  ( A. z e. _om ( y ~~ z -> y = z ) -> ( z e. _om -> ( y ~~ z -> y = z ) ) )
43 41 42 impel 
 |-  ( ( y e. _om /\ A. z e. _om ( y ~~ z -> y = z ) ) -> ( z e. _om -> ( suc y ~~ suc z -> y = z ) ) )
44 suceq 
 |-  ( y = z -> suc y = suc z )
45 43 44 syl8 
 |-  ( ( y e. _om /\ A. z e. _om ( y ~~ z -> y = z ) ) -> ( z e. _om -> ( suc y ~~ suc z -> suc y = suc z ) ) )
46 breq2 
 |-  ( w = suc z -> ( suc y ~~ w <-> suc y ~~ suc z ) )
47 eqeq2 
 |-  ( w = suc z -> ( suc y = w <-> suc y = suc z ) )
48 46 47 imbi12d 
 |-  ( w = suc z -> ( ( suc y ~~ w -> suc y = w ) <-> ( suc y ~~ suc z -> suc y = suc z ) ) )
49 48 biimprcd 
 |-  ( ( suc y ~~ suc z -> suc y = suc z ) -> ( w = suc z -> ( suc y ~~ w -> suc y = w ) ) )
50 45 49 syl6 
 |-  ( ( y e. _om /\ A. z e. _om ( y ~~ z -> y = z ) ) -> ( z e. _om -> ( w = suc z -> ( suc y ~~ w -> suc y = w ) ) ) )
51 35 36 50 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 ) ) )
52 32 51 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 ) ) )
53 52 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 ) ) ) )
54 25 53 syl7 
 |-  ( y e. _om -> ( A. z e. _om ( y ~~ z -> y = z ) -> ( w e. _om -> ( suc y ~~ w -> suc y = w ) ) ) )
55 54 ralrimdv 
 |-  ( y e. _om -> ( A. z e. _om ( y ~~ z -> y = z ) -> A. w e. _om ( suc y ~~ w -> suc y = w ) ) )
56 breq2 
 |-  ( w = z -> ( suc y ~~ w <-> suc y ~~ z ) )
57 eqeq2 
 |-  ( w = z -> ( suc y = w <-> suc y = z ) )
58 56 57 imbi12d 
 |-  ( w = z -> ( ( suc y ~~ w -> suc y = w ) <-> ( suc y ~~ z -> suc y = z ) ) )
59 58 cbvralvw 
 |-  ( A. w e. _om ( suc y ~~ w -> suc y = w ) <-> A. z e. _om ( suc y ~~ z -> suc y = z ) )
60 55 59 imbitrdi 
 |-  ( y e. _om -> ( A. z e. _om ( y ~~ z -> y = z ) -> A. z e. _om ( suc y ~~ z -> suc y = z ) ) )
61 4 8 12 16 24 60 finds 
 |-  ( A e. _om -> A. z e. _om ( A ~~ z -> A = z ) )
62 breq2 
 |-  ( z = B -> ( A ~~ z <-> A ~~ B ) )
63 eqeq2 
 |-  ( z = B -> ( A = z <-> A = B ) )
64 62 63 imbi12d 
 |-  ( z = B -> ( ( A ~~ z -> A = z ) <-> ( A ~~ B -> A = B ) ) )
65 64 rspcv 
 |-  ( B e. _om -> ( A. z e. _om ( A ~~ z -> A = z ) -> ( A ~~ B -> A = B ) ) )
66 61 65 mpan9 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A ~~ B -> A = B ) )
67 enrefnn 
 |-  ( A e. _om -> A ~~ A )
68 breq2 
 |-  ( A = B -> ( A ~~ A <-> A ~~ B ) )
69 67 68 syl5ibcom 
 |-  ( A e. _om -> ( A = B -> A ~~ B ) )
70 69 adantr 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A = B -> A ~~ B ) )
71 66 70 impbid 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A ~~ B <-> A = B ) )