Theorem uztrn2 12601

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 12600	. . . 4 ⊢ ((𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝑀 ∈ (ℤ≥‘𝐾))
4	3	ancoms 459	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
5	2, 4	sylanb 581	. 2 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
6	5, 1	eleqtrrdi 2850	1 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ‘cfv 6433  ℤ_≥cuz 12582

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-pre-lttri 10945  ax-pre-lttrn 10946

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-nel 3050  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-neg 11208  df-z 12320  df-uz 12583

This theorem is referenced by:  eluznn0  12657  eluznn  12658  elfzuz2  13261  rexuz3  15060  r19.29uz  15062  r19.2uz  15063  clim2  15213  clim2c  15214  clim0c  15216  rlimclim1  15254  2clim  15281  climabs0  15294  climcn1  15301  climcn2  15302  climsqz  15350  climsqz2  15351  clim2ser  15366  clim2ser2  15367  climub  15373  climsup  15381  caurcvg2  15389  serf0  15392  iseraltlem1  15393  iseralt  15396  cvgcmp  15528  cvgcmpce  15530  isumsup2  15558  mertenslem1  15596  clim2div  15601  ntrivcvgfvn0  15611  ntrivcvgmullem  15613  fprodeq0  15685  lmbrf  22411  lmss  22449  lmres  22451  txlm  22799  uzrest  23048  lmmcvg  24425  lmmbrf  24426  iscau4  24443  iscauf  24444  caucfil  24447  iscmet3lem3  24454  iscmet3lem1  24455  lmle  24465  lmclim  24467  mbflimsup  24830  ulm2  25544  ulmcaulem  25553  ulmcau  25554  ulmss  25556  ulmdvlem1  25559  ulmdvlem3  25561  mtest  25563  itgulm  25567  logfaclbnd  26370  bposlem6  26437  caures  35918  caushft  35919  dvgrat  41930  cvgdvgrat  41931  climinf  43147  clim2f  43177  clim2cf  43191  clim0cf  43195  clim2f2  43211  fnlimfvre  43215  allbutfifvre  43216  limsupvaluz2  43279  limsupreuzmpt  43280  supcnvlimsup  43281  climuzlem  43284  climisp  43287  climrescn  43289  climxrrelem  43290  climxrre  43291  limsupgtlem  43318  liminfreuzlem  43343  liminfltlem  43345  liminflimsupclim  43348  xlimpnfxnegmnf  43355  liminflbuz2  43356  liminfpnfuz  43357  liminflimsupxrre  43358  xlimmnfvlem2  43374  xlimmnfv  43375  xlimpnfvlem2  43378  xlimpnfv  43379  xlimmnfmpt  43384  xlimpnfmpt  43385  climxlim2lem  43386  xlimpnfxnegmnf2  43399  meaiuninc3v  44022  smflimlem1  44306  smflimlem2  44307  smflimlem3  44308  smflimmpt  44343  smflimsuplem4  44356  smflimsuplem7  44359  smflimsupmpt  44362  smfliminfmpt  44365