Theorem uztrn2 12860

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 2856	. . 3 ⊢ (𝑁 ∈ 𝑍 ↔ 𝑁 ∈ (ℤ≥‘𝐾))
3		uztrn 12859	. . . 4 ⊢ ((𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝑀 ∈ (ℤ≥‘𝐾))
4	3	ancoms 462	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
5	2, 4	sylanb 590	. 2 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
6	5, 1	eleqtrrdi 2875	1 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1562   ∈ wcel 2144  ‘cfv 6523  ℤ_≥cuz 12841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-cnex 11131  ax-resscn 11132  ax-pre-lttri 11149  ax-pre-lttrn 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-ov 7401  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-neg 11419  df-z 12571  df-uz 12842

This theorem is referenced by:  eluznn0  12920  eluznn  12921  elfzuz2  13536  rexuz3  15378  r19.29uz  15380  r19.2uz  15381  clim2  15533  clim2c  15534  clim0c  15536  rlimclim1  15574  2clim  15601  climabs0  15614  climcn1  15621  climcn2  15622  climsqz  15670  climsqz2  15671  clim2ser  15684  clim2ser2  15685  climub  15691  climsup  15699  caurcvg2  15707  serf0  15710  iseraltlem1  15711  iseralt  15714  cvgcmp  15846  cvgcmpce  15848  isumsup2  15878  mertenslem1  15916  clim2div  15921  ntrivcvgfvn0  15931  ntrivcvgmullem  15933  fprodeq0  16007  lmbrf  23322  lmss  23360  lmres  23362  txlm  23710  uzrest  23959  lmmcvg  25325  lmmbrf  25326  iscau4  25343  iscauf  25344  caucfil  25347  iscmet3lem3  25354  iscmet3lem1  25355  lmle  25365  lmclim  25367  mbflimsup  25730  ulm2  26450  ulmcaulem  26459  ulmcau  26460  ulmss  26462  ulmdvlem1  26465  ulmdvlem3  26467  mtest  26469  itgulm  26473  logfaclbnd  27288  bposlem6  27355  caures  38264  caushft  38265  dvgrat  44893  cvgdvgrat  44894  climinf  46187  clim2f  46215  clim2cf  46229  clim0cf  46233  clim2f2  46249  fnlimfvre  46253  allbutfifvre  46254  limsupvaluz2  46317  limsupreuzmpt  46318  supcnvlimsup  46319  climuzlem  46322  climisp  46325  climrescn  46327  climxrrelem  46328  climxrre  46329  limsupgtlem  46356  liminfreuzlem  46381  liminfltlem  46383  liminflimsupclim  46386  xlimpnfxnegmnf  46393  liminflbuz2  46394  liminfpnfuz  46395  liminflimsupxrre  46396  xlimmnfvlem2  46412  xlimmnfv  46413  xlimpnfvlem2  46416  xlimpnfv  46417  xlimmnfmpt  46422  xlimpnfmpt  46423  climxlim2lem  46424  xlimpnfxnegmnf2  46437  meaiuninc3v  47063  smflimlem1  47350  smflimlem2  47351  smflimlem3  47352  smflimmpt  47389  smflimsuplem4  47402  smflimsuplem7  47405  smflimsupmpt  47408  smfliminfmpt  47411