Theorem uztrn2 12250

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 2881	. . 3 ⊢ (𝑁 ∈ 𝑍 ↔ 𝑁 ∈ (ℤ≥‘𝐾))
3		uztrn 12249	. . . 4 ⊢ ((𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝑀 ∈ (ℤ≥‘𝐾))
4	3	ancoms 462	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
5	2, 4	sylanb 584	. 2 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
6	5, 1	eleqtrrdi 2901	1 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ‘cfv 6324  ℤ_≥cuz 12231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-pre-lttri 10600  ax-pre-lttrn 10601

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-neg 10862  df-z 11970  df-uz 12232

This theorem is referenced by:  eluznn0  12305  eluznn  12306  elfzuz2  12907  rexuz3  14700  r19.29uz  14702  r19.2uz  14703  clim2  14853  clim2c  14854  clim0c  14856  rlimclim1  14894  2clim  14921  climabs0  14934  climcn1  14940  climcn2  14941  climsqz  14989  climsqz2  14990  clim2ser  15003  clim2ser2  15004  climub  15010  climsup  15018  caurcvg2  15026  serf0  15029  iseraltlem1  15030  iseralt  15033  cvgcmp  15163  cvgcmpce  15165  isumsup2  15193  mertenslem1  15232  clim2div  15237  ntrivcvgfvn0  15247  ntrivcvgmullem  15249  fprodeq0  15321  lmbrf  21865  lmss  21903  lmres  21905  txlm  22253  uzrest  22502  lmmcvg  23865  lmmbrf  23866  iscau4  23883  iscauf  23884  caucfil  23887  iscmet3lem3  23894  iscmet3lem1  23895  lmle  23905  lmclim  23907  mbflimsup  24270  ulm2  24980  ulmcaulem  24989  ulmcau  24990  ulmss  24992  ulmdvlem1  24995  ulmdvlem3  24997  mtest  24999  itgulm  25003  logfaclbnd  25806  bposlem6  25873  caures  35198  caushft  35199  dvgrat  41016  cvgdvgrat  41017  climinf  42248  clim2f  42278  clim2cf  42292  clim0cf  42296  clim2f2  42312  fnlimfvre  42316  allbutfifvre  42317  limsupvaluz2  42380  limsupreuzmpt  42381  supcnvlimsup  42382  climuzlem  42385  climisp  42388  climrescn  42390  climxrrelem  42391  climxrre  42392  limsupgtlem  42419  liminfreuzlem  42444  liminfltlem  42446  liminflimsupclim  42449  xlimpnfxnegmnf  42456  liminflbuz2  42457  liminfpnfuz  42458  liminflimsupxrre  42459  xlimmnfvlem2  42475  xlimmnfv  42476  xlimpnfvlem2  42479  xlimpnfv  42480  xlimmnfmpt  42485  xlimpnfmpt  42486  climxlim2lem  42487  xlimpnfxnegmnf2  42500  meaiuninc3v  43123  smflimlem1  43404  smflimlem2  43405  smflimlem3  43406  smflimmpt  43441  smflimsuplem4  43454  smflimsuplem7  43457  smflimsupmpt  43460  smfliminfmpt  43463