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 2833	. . 3 ⊢ (𝑁 ∈ 𝑍 ↔ 𝑁 ∈ (ℤ≥‘𝐾))
3		uztrn 12801	. . . 4 ⊢ ((𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝑀 ∈ (ℤ≥‘𝐾))
4	3	ancoms 460	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
5	2, 4	sylanb 588	. 2 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
6	5, 1	eleqtrrdi 2852	1 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1548   ∈ wcel 2121  ‘cfv 6489  ℤ_≥cuz 12783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-cnex 11089  ax-resscn 11090  ax-pre-lttri 11107  ax-pre-lttrn 11108

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7363  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  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  23247  lmss  23285  lmres  23287  txlm  23635  uzrest  23884  lmmcvg  25250  lmmbrf  25251  iscau4  25268  iscauf  25269  caucfil  25272  iscmet3lem3  25279  iscmet3lem1  25280  lmle  25290  lmclim  25292  mbflimsup  25655  ulm2  26372  ulmcaulem  26381  ulmcau  26382  ulmss  26384  ulmdvlem1  26387  ulmdvlem3  26389  mtest  26391  itgulm  26395  logfaclbnd  27207  bposlem6  27274  caures  38142  caushft  38143  dvgrat  44771  cvgdvgrat  44772  climinf  46065  clim2f  46093  clim2cf  46107  clim0cf  46111  clim2f2  46127  fnlimfvre  46131  allbutfifvre  46132  limsupvaluz2  46195  limsupreuzmpt  46196  supcnvlimsup  46197  climuzlem  46200  climisp  46203  climrescn  46205  climxrrelem  46206  climxrre  46207  limsupgtlem  46234  liminfreuzlem  46259  liminfltlem  46261  liminflimsupclim  46264  xlimpnfxnegmnf  46271  liminflbuz2  46272  liminfpnfuz  46273  liminflimsupxrre  46274  xlimmnfvlem2  46290  xlimmnfv  46291  xlimpnfvlem2  46294  xlimpnfv  46295  xlimmnfmpt  46300  xlimpnfmpt  46301  climxlim2lem  46302  xlimpnfxnegmnf2  46315  meaiuninc3v  46941  smflimlem1  47228  smflimlem2  47229  smflimlem3  47230  smflimmpt  47267  smflimsuplem4  47280  smflimsuplem7  47283  smflimsupmpt  47286  smfliminfmpt  47289