Theorem uztrn2 12984

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ‘cfv 6538  ℤ_≥cuz 12965

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-pre-lttri 11274  ax-pre-lttrn 11275

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-neg 11544  df-z 12694  df-uz 12966

This theorem is used by:  eluznn0  13044  eluznn  13045  elfzuz2  13662  rexuz3  15516  r19.29uz  15518  r19.2uz  15519  clim2  15671  clim2c  15672  clim0c  15674  rlimclim1  15712  2clim  15739  climabs0  15752  climcn1  15759  climcn2  15760  climsqz  15808  climsqz2  15809  clim2ser  15822  clim2ser2  15823  climub  15829  climsup  15837  caurcvg2  15845  serf0  15848  iseraltlem1  15849  iseralt  15852  cvgcmp  15983  cvgcmpce  15985  isumsup2  16015  mertenslem1  16053  clim2div  16058  ntrivcvgfvn0  16068  ntrivcvgmullem  16070  fprodeq0  16142  lmbrf  23578  lmss  23616  lmres  23618  txlm  23967  uzrest  24216  lmmcvg  25582  lmmbrf  25583  iscau4  25600  iscauf  25601  caucfil  25604  iscmet3lem3  25611  iscmet3lem1  25612  lmle  25622  lmclim  25624  mbflimsup  25987  ulm2  26712  ulmcaulem  26721  ulmcau  26722  ulmss  26724  ulmdvlem1  26727  ulmdvlem3  26729  mtest  26731  itgulm  26735  logfaclbnd  27549  bposlem6  27616  caures  38695  caushft  38696  dvgrat  45296  cvgdvgrat  45297  climinf  46618  clim2f  46646  clim2cf  46660  clim0cf  46664  clim2f2  46680  fnlimfvre  46684  allbutfifvre  46685  limsupvaluz2  46748  limsupreuzmpt  46749  supcnvlimsup  46750  climuzlem  46753  climisp  46756  climrescn  46758  climxrrelem  46759  climxrre  46760  limsupgtlem  46787  liminfreuzlem  46812  liminfltlem  46814  liminflimsupclim  46817  xlimpnfxnegmnf  46824  liminflbuz2  46825  liminfpnfuz  46826  liminflimsupxrre  46827  xlimmnfvlem2  46843  xlimmnfv  46844  xlimpnfvlem2  46847  xlimpnfv  46848  xlimmnfmpt  46853  xlimpnfmpt  46854  climxlim2lem  46855  xlimpnfxnegmnf2  46868  meaiuninc3v  47494  smflimlem1  47781  smflimlem2  47782  smflimlem3  47783  smflimmpt  47820  smflimsuplem4  47833  smflimsuplem7  47836  smflimsupmpt  47839  smfliminfmpt  47842