Theorem uztrn2 12771

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 12770	. . . 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 6490  ℤ_≥cuz 12752

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 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-cnex 11083  ax-resscn 11084  ax-pre-lttri 11101  ax-pre-lttrn 11102

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 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7361  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11169  df-mnf 11170  df-xr 11171  df-ltxr 11172  df-le 11173  df-neg 11368  df-z 12490  df-uz 12753

This theorem is referenced by:  eluznn0  12831  eluznn  12832  elfzuz2  13446  rexuz3  15273  r19.29uz  15275  r19.2uz  15276  clim2  15428  clim2c  15429  clim0c  15431  rlimclim1  15469  2clim  15496  climabs0  15509  climcn1  15516  climcn2  15517  climsqz  15565  climsqz2  15566  clim2ser  15579  clim2ser2  15580  climub  15586  climsup  15594  caurcvg2  15602  serf0  15605  iseraltlem1  15606  iseralt  15609  cvgcmp  15740  cvgcmpce  15742  isumsup2  15770  mertenslem1  15808  clim2div  15813  ntrivcvgfvn0  15823  ntrivcvgmullem  15825  fprodeq0  15899  lmbrf  23203  lmss  23241  lmres  23243  txlm  23591  uzrest  23840  lmmcvg  25206  lmmbrf  25207  iscau4  25224  iscauf  25225  caucfil  25228  iscmet3lem3  25235  iscmet3lem1  25236  lmle  25246  lmclim  25248  mbflimsup  25611  ulm2  26334  ulmcaulem  26343  ulmcau  26344  ulmss  26346  ulmdvlem1  26349  ulmdvlem3  26351  mtest  26353  itgulm  26357  logfaclbnd  27173  bposlem6  27240  caures  38072  caushft  38073  dvgrat  44742  cvgdvgrat  44743  climinf  46040  clim2f  46068  clim2cf  46082  clim0cf  46086  clim2f2  46102  fnlimfvre  46106  allbutfifvre  46107  limsupvaluz2  46170  limsupreuzmpt  46171  supcnvlimsup  46172  climuzlem  46175  climisp  46178  climrescn  46180  climxrrelem  46181  climxrre  46182  limsupgtlem  46209  liminfreuzlem  46234  liminfltlem  46236  liminflimsupclim  46239  xlimpnfxnegmnf  46246  liminflbuz2  46247  liminfpnfuz  46248  liminflimsupxrre  46249  xlimmnfvlem2  46265  xlimmnfv  46266  xlimpnfvlem2  46269  xlimpnfv  46270  xlimmnfmpt  46275  xlimpnfmpt  46276  climxlim2lem  46277  xlimpnfxnegmnf2  46290  meaiuninc3v  46916  smflimlem1  47203  smflimlem2  47204  smflimlem3  47205  smflimmpt  47242  smflimsuplem4  47255  smflimsuplem7  47258  smflimsupmpt  47261  smfliminfmpt  47264