Theorem uztrn2 12897

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ‘cfv 6561  ℤ_≥cuz 12878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-pre-lttri 11229  ax-pre-lttrn 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-neg 11495  df-z 12614  df-uz 12879

This theorem is referenced by:  eluznn0  12959  eluznn  12960  elfzuz2  13569  rexuz3  15387  r19.29uz  15389  r19.2uz  15390  clim2  15540  clim2c  15541  clim0c  15543  rlimclim1  15581  2clim  15608  climabs0  15621  climcn1  15628  climcn2  15629  climsqz  15677  climsqz2  15678  clim2ser  15691  clim2ser2  15692  climub  15698  climsup  15706  caurcvg2  15714  serf0  15717  iseraltlem1  15718  iseralt  15721  cvgcmp  15852  cvgcmpce  15854  isumsup2  15882  mertenslem1  15920  clim2div  15925  ntrivcvgfvn0  15935  ntrivcvgmullem  15937  fprodeq0  16011  lmbrf  23268  lmss  23306  lmres  23308  txlm  23656  uzrest  23905  lmmcvg  25295  lmmbrf  25296  iscau4  25313  iscauf  25314  caucfil  25317  iscmet3lem3  25324  iscmet3lem1  25325  lmle  25335  lmclim  25337  mbflimsup  25701  ulm2  26428  ulmcaulem  26437  ulmcau  26438  ulmss  26440  ulmdvlem1  26443  ulmdvlem3  26445  mtest  26447  itgulm  26451  logfaclbnd  27266  bposlem6  27333  caures  37767  caushft  37768  dvgrat  44331  cvgdvgrat  44332  climinf  45621  clim2f  45651  clim2cf  45665  clim0cf  45669  clim2f2  45685  fnlimfvre  45689  allbutfifvre  45690  limsupvaluz2  45753  limsupreuzmpt  45754  supcnvlimsup  45755  climuzlem  45758  climisp  45761  climrescn  45763  climxrrelem  45764  climxrre  45765  limsupgtlem  45792  liminfreuzlem  45817  liminfltlem  45819  liminflimsupclim  45822  xlimpnfxnegmnf  45829  liminflbuz2  45830  liminfpnfuz  45831  liminflimsupxrre  45832  xlimmnfvlem2  45848  xlimmnfv  45849  xlimpnfvlem2  45852  xlimpnfv  45853  xlimmnfmpt  45858  xlimpnfmpt  45859  climxlim2lem  45860  xlimpnfxnegmnf2  45873  meaiuninc3v  46499  smflimlem1  46786  smflimlem2  46787  smflimlem3  46788  smflimmpt  46825  smflimsuplem4  46838  smflimsuplem7  46841  smflimsupmpt  46844  smfliminfmpt  46847