Theorem uztrn2 12256

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 2904	. . 3 ⊢ (𝑁 ∈ 𝑍 ↔ 𝑁 ∈ (ℤ≥‘𝐾))
3		uztrn 12255	. . . 4 ⊢ ((𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝑀 ∈ (ℤ≥‘𝐾))
4	3	ancoms 461	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
5	2, 4	sylanb 583	. 2 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
6	5, 1	eleqtrrdi 2924	1 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ‘cfv 6349  ℤ_≥cuz 12237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-pre-lttri 10605  ax-pre-lttrn 10606

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7153  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-neg 10867  df-z 11976  df-uz 12238

This theorem is referenced by:  eluznn0  12311  eluznn  12312  elfzuz2  12906  rexuz3  14702  r19.29uz  14704  r19.2uz  14705  clim2  14855  clim2c  14856  clim0c  14858  rlimclim1  14896  2clim  14923  climabs0  14936  climcn1  14942  climcn2  14943  climsqz  14991  climsqz2  14992  clim2ser  15005  clim2ser2  15006  climub  15012  climsup  15020  caurcvg2  15028  serf0  15031  iseraltlem1  15032  iseralt  15035  cvgcmp  15165  cvgcmpce  15167  isumsup2  15195  mertenslem1  15234  clim2div  15239  ntrivcvgfvn0  15249  ntrivcvgmullem  15251  fprodeq0  15323  lmbrf  21862  lmss  21900  lmres  21902  txlm  22250  uzrest  22499  lmmcvg  23858  lmmbrf  23859  iscau4  23876  iscauf  23877  caucfil  23880  iscmet3lem3  23887  iscmet3lem1  23888  lmle  23898  lmclim  23900  mbflimsup  24261  ulm2  24967  ulmcaulem  24976  ulmcau  24977  ulmss  24979  ulmdvlem1  24982  ulmdvlem3  24984  mtest  24986  itgulm  24990  logfaclbnd  25792  bposlem6  25859  caures  35029  caushft  35030  dvgrat  40637  cvgdvgrat  40638  climinf  41880  clim2f  41910  clim2cf  41924  clim0cf  41928  clim2f2  41944  fnlimfvre  41948  allbutfifvre  41949  limsupvaluz2  42012  limsupreuzmpt  42013  supcnvlimsup  42014  climuzlem  42017  climisp  42020  climrescn  42022  climxrrelem  42023  climxrre  42024  limsupgtlem  42051  liminfreuzlem  42076  liminfltlem  42078  liminflimsupclim  42081  xlimpnfxnegmnf  42088  liminflbuz2  42089  liminfpnfuz  42090  liminflimsupxrre  42091  xlimmnfvlem2  42107  xlimmnfv  42108  xlimpnfvlem2  42111  xlimpnfv  42112  xlimmnfmpt  42117  xlimpnfmpt  42118  climxlim2lem  42119  xlimpnfxnegmnf2  42132  meaiuninc3v  42760  smflimlem1  43041  smflimlem2  43042  smflimlem3  43043  smflimmpt  43078  smflimsuplem4  43091  smflimsuplem7  43094  smflimsupmpt  43097  smfliminfmpt  43100