Theorem uztrn2 12807

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

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

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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-pre-lttri 11112  ax-pre-lttrn 11113

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-neg 11380  df-z 12525  df-uz 12789

This theorem is referenced by:  eluznn0  12867  eluznn  12868  elfzuz2  13483  rexuz3  15311  r19.29uz  15313  r19.2uz  15314  clim2  15466  clim2c  15467  clim0c  15469  rlimclim1  15507  2clim  15534  climabs0  15547  climcn1  15554  climcn2  15555  climsqz  15603  climsqz2  15604  clim2ser  15617  clim2ser2  15618  climub  15624  climsup  15632  caurcvg2  15640  serf0  15643  iseraltlem1  15644  iseralt  15647  cvgcmp  15779  cvgcmpce  15781  isumsup2  15811  mertenslem1  15849  clim2div  15854  ntrivcvgfvn0  15864  ntrivcvgmullem  15866  fprodeq0  15940  lmbrf  23225  lmss  23263  lmres  23265  txlm  23613  uzrest  23862  lmmcvg  25228  lmmbrf  25229  iscau4  25246  iscauf  25247  caucfil  25250  iscmet3lem3  25257  iscmet3lem1  25258  lmle  25268  lmclim  25270  mbflimsup  25633  ulm2  26350  ulmcaulem  26359  ulmcau  26360  ulmss  26362  ulmdvlem1  26365  ulmdvlem3  26367  mtest  26369  itgulm  26373  logfaclbnd  27185  bposlem6  27252  caures  38081  caushft  38082  dvgrat  44739  cvgdvgrat  44740  climinf  46036  clim2f  46064  clim2cf  46078  clim0cf  46082  clim2f2  46098  fnlimfvre  46102  allbutfifvre  46103  limsupvaluz2  46166  limsupreuzmpt  46167  supcnvlimsup  46168  climuzlem  46171  climisp  46174  climrescn  46176  climxrrelem  46177  climxrre  46178  limsupgtlem  46205  liminfreuzlem  46230  liminfltlem  46232  liminflimsupclim  46235  xlimpnfxnegmnf  46242  liminflbuz2  46243  liminfpnfuz  46244  liminflimsupxrre  46245  xlimmnfvlem2  46261  xlimmnfv  46262  xlimpnfvlem2  46265  xlimpnfv  46266  xlimmnfmpt  46271  xlimpnfmpt  46272  climxlim2lem  46273  xlimpnfxnegmnf2  46286  meaiuninc3v  46912  smflimlem1  47199  smflimlem2  47200  smflimlem3  47201  smflimmpt  47238  smflimsuplem4  47251  smflimsuplem7  47254  smflimsupmpt  47257  smfliminfmpt  47260