Theorem uztrn2 12819

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  ℤ_≥cuz 12800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-pre-lttri 11149  ax-pre-lttrn 11150

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-neg 11415  df-z 12537  df-uz 12801

This theorem is referenced by:  eluznn0  12883  eluznn  12884  elfzuz2  13497  rexuz3  15322  r19.29uz  15324  r19.2uz  15325  clim2  15477  clim2c  15478  clim0c  15480  rlimclim1  15518  2clim  15545  climabs0  15558  climcn1  15565  climcn2  15566  climsqz  15614  climsqz2  15615  clim2ser  15628  clim2ser2  15629  climub  15635  climsup  15643  caurcvg2  15651  serf0  15654  iseraltlem1  15655  iseralt  15658  cvgcmp  15789  cvgcmpce  15791  isumsup2  15819  mertenslem1  15857  clim2div  15862  ntrivcvgfvn0  15872  ntrivcvgmullem  15874  fprodeq0  15948  lmbrf  23154  lmss  23192  lmres  23194  txlm  23542  uzrest  23791  lmmcvg  25168  lmmbrf  25169  iscau4  25186  iscauf  25187  caucfil  25190  iscmet3lem3  25197  iscmet3lem1  25198  lmle  25208  lmclim  25210  mbflimsup  25574  ulm2  26301  ulmcaulem  26310  ulmcau  26311  ulmss  26313  ulmdvlem1  26316  ulmdvlem3  26318  mtest  26320  itgulm  26324  logfaclbnd  27140  bposlem6  27207  caures  37761  caushft  37762  dvgrat  44308  cvgdvgrat  44309  climinf  45611  clim2f  45641  clim2cf  45655  clim0cf  45659  clim2f2  45675  fnlimfvre  45679  allbutfifvre  45680  limsupvaluz2  45743  limsupreuzmpt  45744  supcnvlimsup  45745  climuzlem  45748  climisp  45751  climrescn  45753  climxrrelem  45754  climxrre  45755  limsupgtlem  45782  liminfreuzlem  45807  liminfltlem  45809  liminflimsupclim  45812  xlimpnfxnegmnf  45819  liminflbuz2  45820  liminfpnfuz  45821  liminflimsupxrre  45822  xlimmnfvlem2  45838  xlimmnfv  45839  xlimpnfvlem2  45842  xlimpnfv  45843  xlimmnfmpt  45848  xlimpnfmpt  45849  climxlim2lem  45850  xlimpnfxnegmnf2  45863  meaiuninc3v  46489  smflimlem1  46776  smflimlem2  46777  smflimlem3  46778  smflimmpt  46815  smflimsuplem4  46828  smflimsuplem7  46831  smflimsupmpt  46834  smfliminfmpt  46837