Theorem uztrn2 12881

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 2861	. . 3 ⊢ (𝑁 ∈ 𝑍 ↔ 𝑁 ∈ (ℤ≥‘𝐾))
3		uztrn 12880	. . . 4 ⊢ ((𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝑀 ∈ (ℤ≥‘𝐾))
4	3	ancoms 463	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
5	2, 4	sylanb 592	. 2 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
6	5, 1	eleqtrrdi 2880	1 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ‘cfv 6537  ℤ_≥cuz 12862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5259  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11156  ax-resscn 11157  ax-pre-lttri 11174  ax-pre-lttrn 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-sbc 3752  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-neg 11444  df-z 12592  df-uz 12863

This theorem is referenced by:  eluznn0  12941  eluznn  12942  elfzuz2  13557  rexuz3  15400  r19.29uz  15402  r19.2uz  15403  clim2  15555  clim2c  15556  clim0c  15558  rlimclim1  15596  2clim  15623  climabs0  15636  climcn1  15643  climcn2  15644  climsqz  15692  climsqz2  15693  clim2ser  15706  clim2ser2  15707  climub  15713  climsup  15721  caurcvg2  15729  serf0  15732  iseraltlem1  15733  iseralt  15736  cvgcmp  15868  cvgcmpce  15870  isumsup2  15900  mertenslem1  15938  clim2div  15943  ntrivcvgfvn0  15953  ntrivcvgmullem  15955  fprodeq0  16029  lmbrf  23386  lmss  23424  lmres  23426  txlm  23774  uzrest  24023  lmmcvg  25389  lmmbrf  25390  iscau4  25407  iscauf  25408  caucfil  25411  iscmet3lem3  25418  iscmet3lem1  25419  lmle  25429  lmclim  25431  mbflimsup  25794  ulm2  26514  ulmcaulem  26523  ulmcau  26524  ulmss  26526  ulmdvlem1  26529  ulmdvlem3  26531  mtest  26533  itgulm  26537  logfaclbnd  27352  bposlem6  27419  caures  38334  caushft  38335  dvgrat  44949  cvgdvgrat  44950  climinf  46249  clim2f  46277  clim2cf  46291  clim0cf  46295  clim2f2  46311  fnlimfvre  46315  allbutfifvre  46316  limsupvaluz2  46379  limsupreuzmpt  46380  supcnvlimsup  46381  climuzlem  46384  climisp  46387  climrescn  46389  climxrrelem  46390  climxrre  46391  limsupgtlem  46418  liminfreuzlem  46443  liminfltlem  46445  liminflimsupclim  46448  xlimpnfxnegmnf  46455  liminflbuz2  46456  liminfpnfuz  46457  liminflimsupxrre  46458  xlimmnfvlem2  46474  xlimmnfv  46475  xlimpnfvlem2  46478  xlimpnfv  46479  xlimmnfmpt  46484  xlimpnfmpt  46485  climxlim2lem  46486  xlimpnfxnegmnf2  46499  meaiuninc3v  47125  smflimlem1  47412  smflimlem2  47413  smflimlem3  47414  smflimmpt  47451  smflimsuplem4  47464  smflimsuplem7  47467  smflimsupmpt  47470  smfliminfmpt  47473