Theorem uztrn2 12802

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 12801	. . . 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 6494  ℤ_≥cuz 12783

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 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684  ax-cnex 11089  ax-resscn 11090  ax-pre-lttri 11107  ax-pre-lttrn 11108

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 5521  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-ov 7365  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-neg 11375  df-z 12520  df-uz 12784

This theorem is referenced by:  eluznn0  12862  eluznn  12863  elfzuz2  13478  rexuz3  15306  r19.29uz  15308  r19.2uz  15309  clim2  15461  clim2c  15462  clim0c  15464  rlimclim1  15502  2clim  15529  climabs0  15542  climcn1  15549  climcn2  15550  climsqz  15598  climsqz2  15599  clim2ser  15612  clim2ser2  15613  climub  15619  climsup  15627  caurcvg2  15635  serf0  15638  iseraltlem1  15639  iseralt  15642  cvgcmp  15774  cvgcmpce  15776  isumsup2  15806  mertenslem1  15844  clim2div  15849  ntrivcvgfvn0  15859  ntrivcvgmullem  15861  fprodeq0  15935  lmbrf  23239  lmss  23277  lmres  23279  txlm  23627  uzrest  23876  lmmcvg  25242  lmmbrf  25243  iscau4  25260  iscauf  25261  caucfil  25264  iscmet3lem3  25271  iscmet3lem1  25272  lmle  25282  lmclim  25284  mbflimsup  25647  ulm2  26367  ulmcaulem  26376  ulmcau  26377  ulmss  26379  ulmdvlem1  26382  ulmdvlem3  26384  mtest  26386  itgulm  26390  logfaclbnd  27203  bposlem6  27270  caures  38101  caushft  38102  dvgrat  44763  cvgdvgrat  44764  climinf  46060  clim2f  46088  clim2cf  46102  clim0cf  46106  clim2f2  46122  fnlimfvre  46126  allbutfifvre  46127  limsupvaluz2  46190  limsupreuzmpt  46191  supcnvlimsup  46192  climuzlem  46195  climisp  46198  climrescn  46200  climxrrelem  46201  climxrre  46202  limsupgtlem  46229  liminfreuzlem  46254  liminfltlem  46256  liminflimsupclim  46259  xlimpnfxnegmnf  46266  liminflbuz2  46267  liminfpnfuz  46268  liminflimsupxrre  46269  xlimmnfvlem2  46285  xlimmnfv  46286  xlimpnfvlem2  46289  xlimpnfv  46290  xlimmnfmpt  46295  xlimpnfmpt  46296  climxlim2lem  46297  xlimpnfxnegmnf2  46310  meaiuninc3v  46936  smflimlem1  47223  smflimlem2  47224  smflimlem3  47225  smflimmpt  47262  smflimsuplem4  47275  smflimsuplem7  47278  smflimsupmpt  47281  smfliminfmpt  47284