Theorem uztrn2 12784

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 2829	. . 3 ⊢ (𝑁 ∈ 𝑍 ↔ 𝑁 ∈ (ℤ≥‘𝐾))
3		uztrn 12783	. . . 4 ⊢ ((𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝑀 ∈ (ℤ≥‘𝐾))
4	3	ancoms 458	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
5	2, 4	sylanb 582	. 2 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
6	5, 1	eleqtrrdi 2848	1 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ‘cfv 6502  ℤ_≥cuz 12765

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-cnex 11096  ax-resscn 11097  ax-pre-lttri 11114  ax-pre-lttrn 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-ov 7373  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-neg 11381  df-z 12503  df-uz 12766

This theorem is referenced by:  eluznn0  12844  eluznn  12845  elfzuz2  13459  rexuz3  15286  r19.29uz  15288  r19.2uz  15289  clim2  15441  clim2c  15442  clim0c  15444  rlimclim1  15482  2clim  15509  climabs0  15522  climcn1  15529  climcn2  15530  climsqz  15578  climsqz2  15579  clim2ser  15592  clim2ser2  15593  climub  15599  climsup  15607  caurcvg2  15615  serf0  15618  iseraltlem1  15619  iseralt  15622  cvgcmp  15753  cvgcmpce  15755  isumsup2  15783  mertenslem1  15821  clim2div  15826  ntrivcvgfvn0  15836  ntrivcvgmullem  15838  fprodeq0  15912  lmbrf  23221  lmss  23259  lmres  23261  txlm  23609  uzrest  23858  lmmcvg  25234  lmmbrf  25235  iscau4  25252  iscauf  25253  caucfil  25256  iscmet3lem3  25263  iscmet3lem1  25264  lmle  25274  lmclim  25276  mbflimsup  25640  ulm2  26367  ulmcaulem  26376  ulmcau  26377  ulmss  26379  ulmdvlem1  26382  ulmdvlem3  26384  mtest  26386  itgulm  26390  logfaclbnd  27206  bposlem6  27273  caures  38040  caushft  38041  dvgrat  44697  cvgdvgrat  44698  climinf  45995  clim2f  46023  clim2cf  46037  clim0cf  46041  clim2f2  46057  fnlimfvre  46061  allbutfifvre  46062  limsupvaluz2  46125  limsupreuzmpt  46126  supcnvlimsup  46127  climuzlem  46130  climisp  46133  climrescn  46135  climxrrelem  46136  climxrre  46137  limsupgtlem  46164  liminfreuzlem  46189  liminfltlem  46191  liminflimsupclim  46194  xlimpnfxnegmnf  46201  liminflbuz2  46202  liminfpnfuz  46203  liminflimsupxrre  46204  xlimmnfvlem2  46220  xlimmnfv  46221  xlimpnfvlem2  46224  xlimpnfv  46225  xlimmnfmpt  46230  xlimpnfmpt  46231  climxlim2lem  46232  xlimpnfxnegmnf2  46245  meaiuninc3v  46871  smflimlem1  47158  smflimlem2  47159  smflimlem3  47160  smflimmpt  47197  smflimsuplem4  47210  smflimsuplem7  47213  smflimsupmpt  47216  smfliminfmpt  47219