Theorem uztrn2 12836

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

Step	Hyp	Ref	Expression
1		uztrn2.1	. . . 4 ⊢ 𝑍 = (ℤ≥‘𝐾)
2	1	eleq2i 2826	. . 3 ⊢ (𝑁 ∈ 𝑍 ↔ 𝑁 ∈ (ℤ≥‘𝐾))
3		uztrn 12835	. . . 4 ⊢ ((𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝑀 ∈ (ℤ≥‘𝐾))
4	3	ancoms 460	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
5	2, 4	sylanb 582	. 2 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
6	5, 1	eleqtrrdi 2845	1 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ‘cfv 6539  ℤ_≥cuz 12817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5297  ax-nul 5304  ax-pow 5361  ax-pr 5425  ax-un 7719  ax-cnex 11161  ax-resscn 11162  ax-pre-lttri 11179  ax-pre-lttrn 11180

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4527  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4907  df-br 5147  df-opab 5209  df-mpt 5230  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-iota 6491  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7406  df-er 8698  df-en 8935  df-dom 8936  df-sdom 8937  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-neg 11442  df-z 12554  df-uz 12818

This theorem is referenced by:  eluznn0  12896  eluznn  12897  elfzuz2  13501  rexuz3  15290  r19.29uz  15292  r19.2uz  15293  clim2  15443  clim2c  15444  clim0c  15446  rlimclim1  15484  2clim  15511  climabs0  15524  climcn1  15531  climcn2  15532  climsqz  15580  climsqz2  15581  clim2ser  15596  clim2ser2  15597  climub  15603  climsup  15611  caurcvg2  15619  serf0  15622  iseraltlem1  15623  iseralt  15626  cvgcmp  15757  cvgcmpce  15759  isumsup2  15787  mertenslem1  15825  clim2div  15830  ntrivcvgfvn0  15840  ntrivcvgmullem  15842  fprodeq0  15914  lmbrf  22745  lmss  22783  lmres  22785  txlm  23133  uzrest  23382  lmmcvg  24759  lmmbrf  24760  iscau4  24777  iscauf  24778  caucfil  24781  iscmet3lem3  24788  iscmet3lem1  24789  lmle  24799  lmclim  24801  mbflimsup  25164  ulm2  25878  ulmcaulem  25887  ulmcau  25888  ulmss  25890  ulmdvlem1  25893  ulmdvlem3  25895  mtest  25897  itgulm  25901  logfaclbnd  26704  bposlem6  26771  caures  36565  caushft  36566  dvgrat  43003  cvgdvgrat  43004  climinf  44256  clim2f  44286  clim2cf  44300  clim0cf  44304  clim2f2  44320  fnlimfvre  44324  allbutfifvre  44325  limsupvaluz2  44388  limsupreuzmpt  44389  supcnvlimsup  44390  climuzlem  44393  climisp  44396  climrescn  44398  climxrrelem  44399  climxrre  44400  limsupgtlem  44427  liminfreuzlem  44452  liminfltlem  44454  liminflimsupclim  44457  xlimpnfxnegmnf  44464  liminflbuz2  44465  liminfpnfuz  44466  liminflimsupxrre  44467  xlimmnfvlem2  44483  xlimmnfv  44484  xlimpnfvlem2  44487  xlimpnfv  44488  xlimmnfmpt  44493  xlimpnfmpt  44494  climxlim2lem  44495  xlimpnfxnegmnf2  44508  meaiuninc3v  45134  smflimlem1  45421  smflimlem2  45422  smflimlem3  45423  smflimmpt  45460  smflimsuplem4  45473  smflimsuplem7  45476  smflimsupmpt  45479  smfliminfmpt  45482