Theorem uztrn2 12894

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 2830	. . 3 ⊢ (𝑁 ∈ 𝑍 ↔ 𝑁 ∈ (ℤ≥‘𝐾))
3		uztrn 12893	. . . 4 ⊢ ((𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝑀 ∈ (ℤ≥‘𝐾))
4	3	ancoms 458	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
5	2, 4	sylanb 581	. 2 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
6	5, 1	eleqtrrdi 2849	1 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ‘cfv 6562  ℤ_≥cuz 12875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-pre-lttri 11226  ax-pre-lttrn 11227

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-neg 11492  df-z 12611  df-uz 12876

This theorem is referenced by:  eluznn0  12956  eluznn  12957  elfzuz2  13565  rexuz3  15383  r19.29uz  15385  r19.2uz  15386  clim2  15536  clim2c  15537  clim0c  15539  rlimclim1  15577  2clim  15604  climabs0  15617  climcn1  15624  climcn2  15625  climsqz  15673  climsqz2  15674  clim2ser  15687  clim2ser2  15688  climub  15694  climsup  15702  caurcvg2  15710  serf0  15713  iseraltlem1  15714  iseralt  15717  cvgcmp  15848  cvgcmpce  15850  isumsup2  15878  mertenslem1  15916  clim2div  15921  ntrivcvgfvn0  15931  ntrivcvgmullem  15933  fprodeq0  16007  lmbrf  23283  lmss  23321  lmres  23323  txlm  23671  uzrest  23920  lmmcvg  25308  lmmbrf  25309  iscau4  25326  iscauf  25327  caucfil  25330  iscmet3lem3  25337  iscmet3lem1  25338  lmle  25348  lmclim  25350  mbflimsup  25714  ulm2  26442  ulmcaulem  26451  ulmcau  26452  ulmss  26454  ulmdvlem1  26457  ulmdvlem3  26459  mtest  26461  itgulm  26465  logfaclbnd  27280  bposlem6  27347  caures  37746  caushft  37747  dvgrat  44307  cvgdvgrat  44308  climinf  45561  clim2f  45591  clim2cf  45605  clim0cf  45609  clim2f2  45625  fnlimfvre  45629  allbutfifvre  45630  limsupvaluz2  45693  limsupreuzmpt  45694  supcnvlimsup  45695  climuzlem  45698  climisp  45701  climrescn  45703  climxrrelem  45704  climxrre  45705  limsupgtlem  45732  liminfreuzlem  45757  liminfltlem  45759  liminflimsupclim  45762  xlimpnfxnegmnf  45769  liminflbuz2  45770  liminfpnfuz  45771  liminflimsupxrre  45772  xlimmnfvlem2  45788  xlimmnfv  45789  xlimpnfvlem2  45792  xlimpnfv  45793  xlimmnfmpt  45798  xlimpnfmpt  45799  climxlim2lem  45800  xlimpnfxnegmnf2  45813  meaiuninc3v  46439  smflimlem1  46726  smflimlem2  46727  smflimlem3  46728  smflimmpt  46765  smflimsuplem4  46778  smflimsuplem7  46781  smflimsupmpt  46784  smfliminfmpt  46787