Theorem uztrn2 12772

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

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

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 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680  ax-cnex 11084  ax-resscn 11085  ax-pre-lttri 11102  ax-pre-lttrn 11103

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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-ov 7361  df-er 8635  df-en 8886  df-dom 8887  df-sdom 8888  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-neg 11369  df-z 12491  df-uz 12754

This theorem is referenced by:  eluznn0  12832  eluznn  12833  elfzuz2  13447  rexuz3  15274  r19.29uz  15276  r19.2uz  15277  clim2  15429  clim2c  15430  clim0c  15432  rlimclim1  15470  2clim  15497  climabs0  15510  climcn1  15517  climcn2  15518  climsqz  15566  climsqz2  15567  clim2ser  15580  clim2ser2  15581  climub  15587  climsup  15595  caurcvg2  15603  serf0  15606  iseraltlem1  15607  iseralt  15610  cvgcmp  15741  cvgcmpce  15743  isumsup2  15771  mertenslem1  15809  clim2div  15814  ntrivcvgfvn0  15824  ntrivcvgmullem  15826  fprodeq0  15900  lmbrf  23206  lmss  23244  lmres  23246  txlm  23594  uzrest  23843  lmmcvg  25219  lmmbrf  25220  iscau4  25237  iscauf  25238  caucfil  25241  iscmet3lem3  25248  iscmet3lem1  25249  lmle  25259  lmclim  25261  mbflimsup  25625  ulm2  26352  ulmcaulem  26361  ulmcau  26362  ulmss  26364  ulmdvlem1  26367  ulmdvlem3  26369  mtest  26371  itgulm  26375  logfaclbnd  27191  bposlem6  27258  caures  37930  caushft  37931  dvgrat  44590  cvgdvgrat  44591  climinf  45889  clim2f  45917  clim2cf  45931  clim0cf  45935  clim2f2  45951  fnlimfvre  45955  allbutfifvre  45956  limsupvaluz2  46019  limsupreuzmpt  46020  supcnvlimsup  46021  climuzlem  46024  climisp  46027  climrescn  46029  climxrrelem  46030  climxrre  46031  limsupgtlem  46058  liminfreuzlem  46083  liminfltlem  46085  liminflimsupclim  46088  xlimpnfxnegmnf  46095  liminflbuz2  46096  liminfpnfuz  46097  liminflimsupxrre  46098  xlimmnfvlem2  46114  xlimmnfv  46115  xlimpnfvlem2  46118  xlimpnfv  46119  xlimmnfmpt  46124  xlimpnfmpt  46125  climxlim2lem  46126  xlimpnfxnegmnf2  46139  meaiuninc3v  46765  smflimlem1  47052  smflimlem2  47053  smflimlem3  47054  smflimmpt  47091  smflimsuplem4  47104  smflimsuplem7  47107  smflimsupmpt  47110  smfliminfmpt  47113