MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uztrn2 Structured version   Visualization version   GIF version

Theorem uztrn2 11918
Description: Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013.)
Hypothesis
Ref Expression
uztrn2.1 𝑍 = (ℤ𝐾)
Assertion
Ref Expression
uztrn2 ((𝑁𝑍𝑀 ∈ (ℤ𝑁)) → 𝑀𝑍)

Proof of Theorem uztrn2
StepHypRef Expression
1 uztrn2.1 . . . 4 𝑍 = (ℤ𝐾)
21eleq2i 2877 . . 3 (𝑁𝑍𝑁 ∈ (ℤ𝐾))
3 uztrn 11917 . . . 4 ((𝑀 ∈ (ℤ𝑁) ∧ 𝑁 ∈ (ℤ𝐾)) → 𝑀 ∈ (ℤ𝐾))
43ancoms 448 . . 3 ((𝑁 ∈ (ℤ𝐾) ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑀 ∈ (ℤ𝐾))
52, 4sylanb 572 . 2 ((𝑁𝑍𝑀 ∈ (ℤ𝑁)) → 𝑀 ∈ (ℤ𝐾))
65, 1syl6eleqr 2896 1 ((𝑁𝑍𝑀 ∈ (ℤ𝑁)) → 𝑀𝑍)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wcel 2156  cfv 6097  cuz 11900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-cnex 10273  ax-resscn 10274  ax-pre-lttri 10291  ax-pre-lttrn 10292
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-ov 6873  df-er 7975  df-en 8189  df-dom 8190  df-sdom 8191  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-neg 10550  df-z 11640  df-uz 11901
This theorem is referenced by:  eluznn0  11972  eluznn  11973  elfzuz2  12565  rexuz3  14307  r19.29uz  14309  r19.2uz  14310  clim2  14454  clim2c  14455  clim0c  14457  rlimclim1  14495  2clim  14522  climabs0  14535  climcn1  14541  climcn2  14542  climsqz  14590  climsqz2  14591  clim2ser  14604  clim2ser2  14605  climub  14611  climsup  14619  caurcvg2  14627  serf0  14630  iseraltlem1  14631  iseralt  14634  cvgcmp  14766  cvgcmpce  14768  isumsup2  14796  mertenslem1  14833  clim2div  14838  ntrivcvgfvn0  14848  ntrivcvgmullem  14850  fprodeq0  14922  lmbrf  21274  lmss  21312  lmres  21314  txlm  21661  uzrest  21910  lmmcvg  23267  lmmbrf  23268  iscau4  23285  iscauf  23286  caucfil  23289  iscmet3lem3  23296  iscmet3lem1  23297  lmle  23307  lmclim  23309  mbflimsup  23643  ulm2  24349  ulmcaulem  24358  ulmcau  24359  ulmss  24361  ulmdvlem1  24364  ulmdvlem3  24366  mtest  24368  itgulm  24372  logfaclbnd  25157  bposlem6  25224  caures  33862  caushft  33863  dvgrat  39005  cvgdvgrat  39006  climinf  40312  clim2f  40342  clim2cf  40356  clim0cf  40360  clim2f2  40376  fnlimfvre  40380  allbutfifvre  40381  limsupvaluz2  40444  limsupreuzmpt  40445  supcnvlimsup  40446  climuzlem  40449  climisp  40452  climrescn  40454  climxrrelem  40455  climxrre  40456  limsupgtlem  40483  liminfreuzlem  40508  liminfltlem  40510  liminflimsupclim  40513  xlimmnfvlem2  40533  xlimmnfv  40534  xlimpnfvlem2  40537  xlimpnfv  40538  xlimmnfmpt  40543  xlimpnfmpt  40544  climxlim2lem  40545  meaiuninc3v  41174  smflimlem1  41455  smflimlem2  41456  smflimlem3  41457  smflimmpt  41492  smflimsuplem4  41505  smflimsuplem7  41508  smflimsupmpt  41511  smfliminfmpt  41514
  Copyright terms: Public domain W3C validator