MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nneneq Structured version   Unicode version

Theorem nneneq 7764
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.)
Assertion
Ref Expression
nneneq  |-  ( ( A  e.  om  /\  B  e.  om )  ->  ( A  ~~  B  <->  A  =  B ) )

Proof of Theorem nneneq
Dummy variables  x  y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq1 4426 . . . . . 6  |-  ( x  =  (/)  ->  ( x 
~~  z  <->  (/)  ~~  z
) )
2 eqeq1 2426 . . . . . 6  |-  ( x  =  (/)  ->  ( x  =  z  <->  (/)  =  z ) )
31, 2imbi12d 321 . . . . 5  |-  ( x  =  (/)  ->  ( ( x  ~~  z  ->  x  =  z )  <->  (
(/)  ~~  z  ->  (/)  =  z ) ) )
43ralbidv 2861 . . . 4  |-  ( x  =  (/)  ->  ( A. z  e.  om  (
x  ~~  z  ->  x  =  z )  <->  A. z  e.  om  ( (/)  ~~  z  -> 
(/)  =  z ) ) )
5 breq1 4426 . . . . . 6  |-  ( x  =  y  ->  (
x  ~~  z  <->  y  ~~  z ) )
6 eqeq1 2426 . . . . . 6  |-  ( x  =  y  ->  (
x  =  z  <->  y  =  z ) )
75, 6imbi12d 321 . . . . 5  |-  ( x  =  y  ->  (
( x  ~~  z  ->  x  =  z )  <-> 
( y  ~~  z  ->  y  =  z ) ) )
87ralbidv 2861 . . . 4  |-  ( x  =  y  ->  ( A. z  e.  om  ( x  ~~  z  ->  x  =  z )  <->  A. z  e.  om  (
y  ~~  z  ->  y  =  z ) ) )
9 breq1 4426 . . . . . 6  |-  ( x  =  suc  y  -> 
( x  ~~  z  <->  suc  y  ~~  z ) )
10 eqeq1 2426 . . . . . 6  |-  ( x  =  suc  y  -> 
( x  =  z  <->  suc  y  =  z
) )
119, 10imbi12d 321 . . . . 5  |-  ( x  =  suc  y  -> 
( ( x  ~~  z  ->  x  =  z )  <->  ( suc  y  ~~  z  ->  suc  y  =  z ) ) )
1211ralbidv 2861 . . . 4  |-  ( x  =  suc  y  -> 
( A. z  e. 
om  ( x  ~~  z  ->  x  =  z )  <->  A. z  e.  om  ( suc  y  ~~  z  ->  suc  y  =  z ) ) )
13 breq1 4426 . . . . . 6  |-  ( x  =  A  ->  (
x  ~~  z  <->  A  ~~  z ) )
14 eqeq1 2426 . . . . . 6  |-  ( x  =  A  ->  (
x  =  z  <->  A  =  z ) )
1513, 14imbi12d 321 . . . . 5  |-  ( x  =  A  ->  (
( x  ~~  z  ->  x  =  z )  <-> 
( A  ~~  z  ->  A  =  z ) ) )
1615ralbidv 2861 . . . 4  |-  ( x  =  A  ->  ( A. z  e.  om  ( x  ~~  z  ->  x  =  z )  <->  A. z  e.  om  ( A  ~~  z  ->  A  =  z ) ) )
17 ensym 7628 . . . . . 6  |-  ( (/)  ~~  z  ->  z  ~~  (/) )
18 en0 7642 . . . . . . 7  |-  ( z 
~~  (/)  <->  z  =  (/) )
19 eqcom 2431 . . . . . . 7  |-  ( z  =  (/)  <->  (/)  =  z )
2018, 19bitri 252 . . . . . 6  |-  ( z 
~~  (/)  <->  (/)  =  z )
2117, 20sylib 199 . . . . 5  |-  ( (/)  ~~  z  ->  (/)  =  z )
2221rgenw 2783 . . . 4  |-  A. z  e.  om  ( (/)  ~~  z  -> 
(/)  =  z )
23 nn0suc 6731 . . . . . . 7  |-  ( w  e.  om  ->  (
w  =  (/)  \/  E. z  e.  om  w  =  suc  z ) )
24 en0 7642 . . . . . . . . . . . 12  |-  ( suc  y  ~~  (/)  <->  suc  y  =  (/) )
25 breq2 4427 . . . . . . . . . . . . 13  |-  ( w  =  (/)  ->  ( suc  y  ~~  w  <->  suc  y  ~~  (/) ) )
26 eqeq2 2437 . . . . . . . . . . . . 13  |-  ( w  =  (/)  ->  ( suc  y  =  w  <->  suc  y  =  (/) ) )
2725, 26bibi12d 322 . . . . . . . . . . . 12  |-  ( w  =  (/)  ->  ( ( suc  y  ~~  w  <->  suc  y  =  w )  <-> 
( suc  y  ~~  (/)  <->  suc  y  =  (/) ) ) )
2824, 27mpbiri 236 . . . . . . . . . . 11  |-  ( w  =  (/)  ->  ( suc  y  ~~  w  <->  suc  y  =  w ) )
2928biimpd 210 . . . . . . . . . 10  |-  ( w  =  (/)  ->  ( suc  y  ~~  w  ->  suc  y  =  w
) )
3029a1i 11 . . . . . . . . 9  |-  ( ( y  e.  om  /\  A. z  e.  om  (
y  ~~  z  ->  y  =  z ) )  ->  ( w  =  (/)  ->  ( suc  y  ~~  w  ->  suc  y  =  w ) ) )
31 nfv 1755 . . . . . . . . . . 11  |-  F/ z  y  e.  om
32 nfra1 2803 . . . . . . . . . . 11  |-  F/ z A. z  e.  om  ( y  ~~  z  ->  y  =  z )
3331, 32nfan 1988 . . . . . . . . . 10  |-  F/ z ( y  e.  om  /\ 
A. z  e.  om  ( y  ~~  z  ->  y  =  z ) )
34 nfv 1755 . . . . . . . . . 10  |-  F/ z ( suc  y  ~~  w  ->  suc  y  =  w )
35 rsp 2788 . . . . . . . . . . . . . 14  |-  ( A. z  e.  om  (
y  ~~  z  ->  y  =  z )  -> 
( z  e.  om  ->  ( y  ~~  z  ->  y  =  z ) ) )
36 vex 3083 . . . . . . . . . . . . . . . . . 18  |-  y  e. 
_V
37 vex 3083 . . . . . . . . . . . . . . . . . 18  |-  z  e. 
_V
3836, 37phplem4 7763 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  om  /\  z  e.  om )  ->  ( suc  y  ~~  suc  z  ->  y  ~~  z ) )
3938imim1d 78 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  om  /\  z  e.  om )  ->  ( ( y  ~~  z  ->  y  =  z )  ->  ( suc  y  ~~  suc  z  -> 
y  =  z ) ) )
4039ex 435 . . . . . . . . . . . . . . 15  |-  ( y  e.  om  ->  (
z  e.  om  ->  ( ( y  ~~  z  ->  y  =  z )  ->  ( suc  y  ~~  suc  z  ->  y  =  z ) ) ) )
4140a2d 29 . . . . . . . . . . . . . 14  |-  ( y  e.  om  ->  (
( z  e.  om  ->  ( y  ~~  z  ->  y  =  z ) )  ->  ( z  e.  om  ->  ( suc  y  ~~  suc  z  -> 
y  =  z ) ) ) )
4235, 41syl5 33 . . . . . . . . . . . . 13  |-  ( y  e.  om  ->  ( A. z  e.  om  ( y  ~~  z  ->  y  =  z )  ->  ( z  e. 
om  ->  ( suc  y  ~~  suc  z  ->  y  =  z ) ) ) )
4342imp 430 . . . . . . . . . . . 12  |-  ( ( y  e.  om  /\  A. z  e.  om  (
y  ~~  z  ->  y  =  z ) )  ->  ( z  e. 
om  ->  ( suc  y  ~~  suc  z  ->  y  =  z ) ) )
44 suceq 5507 . . . . . . . . . . . 12  |-  ( y  =  z  ->  suc  y  =  suc  z )
4543, 44syl8 72 . . . . . . . . . . 11  |-  ( ( y  e.  om  /\  A. z  e.  om  (
y  ~~  z  ->  y  =  z ) )  ->  ( z  e. 
om  ->  ( suc  y  ~~  suc  z  ->  suc  y  =  suc  z ) ) )
46 breq2 4427 . . . . . . . . . . . . 13  |-  ( w  =  suc  z  -> 
( suc  y  ~~  w 
<->  suc  y  ~~  suc  z ) )
47 eqeq2 2437 . . . . . . . . . . . . 13  |-  ( w  =  suc  z  -> 
( suc  y  =  w 
<->  suc  y  =  suc  z ) )
4846, 47imbi12d 321 . . . . . . . . . . . 12  |-  ( w  =  suc  z  -> 
( ( suc  y  ~~  w  ->  suc  y  =  w )  <->  ( suc  y  ~~  suc  z  ->  suc  y  =  suc  z ) ) )
4948biimprcd 228 . . . . . . . . . . 11  |-  ( ( suc  y  ~~  suc  z  ->  suc  y  =  suc  z )  ->  (
w  =  suc  z  ->  ( suc  y  ~~  w  ->  suc  y  =  w ) ) )
5045, 49syl6 34 . . . . . . . . . 10  |-  ( ( y  e.  om  /\  A. z  e.  om  (
y  ~~  z  ->  y  =  z ) )  ->  ( z  e. 
om  ->  ( w  =  suc  z  ->  ( suc  y  ~~  w  ->  suc  y  =  w
) ) ) )
5133, 34, 50rexlimd 2906 . . . . . . . . 9  |-  ( ( y  e.  om  /\  A. z  e.  om  (
y  ~~  z  ->  y  =  z ) )  ->  ( E. z  e.  om  w  =  suc  z  ->  ( suc  y  ~~  w  ->  suc  y  =  w ) ) )
5230, 51jaod 381 . . . . . . . 8  |-  ( ( 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
) ) )
5352ex 435 . . . . . . 7  |-  ( 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
) ) ) )
5423, 53syl7 70 . . . . . 6  |-  ( y  e.  om  ->  ( A. z  e.  om  ( y  ~~  z  ->  y  =  z )  ->  ( w  e. 
om  ->  ( suc  y  ~~  w  ->  suc  y  =  w ) ) ) )
5554ralrimdv 2838 . . . . 5  |-  ( y  e.  om  ->  ( A. z  e.  om  ( y  ~~  z  ->  y  =  z )  ->  A. w  e.  om  ( suc  y  ~~  w  ->  suc  y  =  w ) ) )
56 breq2 4427 . . . . . . 7  |-  ( w  =  z  ->  ( suc  y  ~~  w  <->  suc  y  ~~  z ) )
57 eqeq2 2437 . . . . . . 7  |-  ( w  =  z  ->  ( suc  y  =  w  <->  suc  y  =  z ) )
5856, 57imbi12d 321 . . . . . 6  |-  ( w  =  z  ->  (
( suc  y  ~~  w  ->  suc  y  =  w )  <->  ( suc  y  ~~  z  ->  suc  y  =  z )
) )
5958cbvralv 3054 . . . . 5  |-  ( A. w  e.  om  ( suc  y  ~~  w  ->  suc  y  =  w
)  <->  A. z  e.  om  ( suc  y  ~~  z  ->  suc  y  =  z ) )
6055, 59syl6ib 229 . . . 4  |-  ( y  e.  om  ->  ( A. z  e.  om  ( y  ~~  z  ->  y  =  z )  ->  A. z  e.  om  ( suc  y  ~~  z  ->  suc  y  =  z ) ) )
614, 8, 12, 16, 22, 60finds 6733 . . 3  |-  ( A  e.  om  ->  A. z  e.  om  ( A  ~~  z  ->  A  =  z ) )
62 breq2 4427 . . . . 5  |-  ( z  =  B  ->  ( A  ~~  z  <->  A  ~~  B ) )
63 eqeq2 2437 . . . . 5  |-  ( z  =  B  ->  ( A  =  z  <->  A  =  B ) )
6462, 63imbi12d 321 . . . 4  |-  ( z  =  B  ->  (
( A  ~~  z  ->  A  =  z )  <-> 
( A  ~~  B  ->  A  =  B ) ) )
6564rspcv 3178 . . 3  |-  ( B  e.  om  ->  ( A. z  e.  om  ( A  ~~  z  ->  A  =  z )  ->  ( A  ~~  B  ->  A  =  B ) ) )
6661, 65mpan9 471 . 2  |-  ( ( A  e.  om  /\  B  e.  om )  ->  ( A  ~~  B  ->  A  =  B ) )
67 eqeng 7613 . . 3  |-  ( A  e.  om  ->  ( A  =  B  ->  A 
~~  B ) )
6867adantr 466 . 2  |-  ( ( A  e.  om  /\  B  e.  om )  ->  ( A  =  B  ->  A  ~~  B
) )
6966, 68impbid 193 1  |-  ( ( A  e.  om  /\  B  e.  om )  ->  ( A  ~~  B  <->  A  =  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    = wceq 1437    e. wcel 1872   A.wral 2771   E.wrex 2772   (/)c0 3761   class class class wbr 4423   suc csuc 5444   omcom 6706    ~~ cen 7577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-om 6707  df-er 7374  df-en 7581
This theorem is referenced by:  php  7765  onomeneq  7771  nnsdomo  7776  fineqvlem  7795  dif1en  7813  findcard2  7820  cardnn  8405
  Copyright terms: Public domain W3C validator