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

Theorem uztrn2 11539
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 2679 . . 3 (𝑁𝑍𝑁 ∈ (ℤ𝐾))
3 uztrn 11538 . . . 4 ((𝑀 ∈ (ℤ𝑁) ∧ 𝑁 ∈ (ℤ𝐾)) → 𝑀 ∈ (ℤ𝐾))
43ancoms 467 . . 3 ((𝑁 ∈ (ℤ𝐾) ∧ 𝑀 ∈ (ℤ𝑁)) → 𝑀 ∈ (ℤ𝐾))
52, 4sylanb 487 . 2 ((𝑁𝑍𝑀 ∈ (ℤ𝑁)) → 𝑀 ∈ (ℤ𝐾))
65, 1syl6eleqr 2698 1 ((𝑁𝑍𝑀 ∈ (ℤ𝑁)) → 𝑀𝑍)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  cfv 5789  cuz 11521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-pre-lttri 9866  ax-pre-lttrn 9867
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4942  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-ov 6529  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-neg 10120  df-z 11213  df-uz 11522
This theorem is referenced by:  eluznn0  11591  eluznn  11592  elfzuz2  12174  rexuz3  13884  r19.29uz  13886  r19.2uz  13887  clim2  14031  clim2c  14032  clim0c  14034  rlimclim1  14072  2clim  14099  climabs0  14112  climcn1  14118  climcn2  14119  climsqz  14167  climsqz2  14168  clim2ser  14181  clim2ser2  14182  climub  14188  climsup  14196  caurcvg2  14204  serf0  14207  iseraltlem1  14208  iseralt  14211  cvgcmp  14337  cvgcmpce  14339  isumsup2  14365  mertenslem1  14403  clim2div  14408  ntrivcvgfvn0  14418  ntrivcvgmullem  14420  fprodeq0  14492  lmbrf  20821  lmss  20859  lmres  20861  txlm  21208  uzrest  21458  lmmcvg  22811  lmmbrf  22812  iscau4  22829  iscauf  22830  caucfil  22833  iscmet3lem3  22840  iscmet3lem1  22841  lmle  22851  lmclim  22853  mbflimsup  23183  ulm2  23887  ulmcaulem  23896  ulmcau  23897  ulmss  23899  ulmdvlem1  23902  ulmdvlem3  23904  mtest  23906  itgulm  23910  logfaclbnd  24691  bposlem6  24758  caures  32509  caushft  32510  dvgrat  37316  cvgdvgrat  37317  climinf  38456  clim2f  38486  clim2cf  38500  clim0cf  38504  clim2f2  38520  fnlimfvre  38524  allbutfifvre  38525  smflimlem1  39440  smflimlem2  39441  smflimlem3  39442
  Copyright terms: Public domain W3C validator