Theorem uztrn2 12953

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ‘cfv 6527  ℤ_≥cuz 12934

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-cnex 11227  ax-resscn 11228  ax-pre-lttri 11245  ax-pre-lttrn 11246

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-ov 7411  df-er 8695  df-en 8952  df-dom 8953  df-sdom 8954  df-pnf 11316  df-mnf 11317  df-xr 11318  df-ltxr 11319  df-le 11320  df-neg 11515  df-z 12663  df-uz 12935

This theorem is used by:  eluznn0  13013  eluznn  13014  elfzuz2  13630  rexuz3  15483  r19.29uz  15485  r19.2uz  15486  clim2  15638  clim2c  15639  clim0c  15641  rlimclim1  15679  2clim  15706  climabs0  15719  climcn1  15726  climcn2  15727  climsqz  15775  climsqz2  15776  clim2ser  15789  clim2ser2  15790  climub  15796  climsup  15804  caurcvg2  15812  serf0  15815  iseraltlem1  15816  iseralt  15819  cvgcmp  15950  cvgcmpce  15952  isumsup2  15982  mertenslem1  16020  clim2div  16025  ntrivcvgfvn0  16035  ntrivcvgmullem  16037  fprodeq0  16109  lmbrf  23539  lmss  23577  lmres  23579  txlm  23928  uzrest  24177  lmmcvg  25543  lmmbrf  25544  iscau4  25561  iscauf  25562  caucfil  25565  iscmet3lem3  25572  iscmet3lem1  25573  lmle  25583  lmclim  25585  mbflimsup  25948  ulm2  26675  ulmcaulem  26684  ulmcau  26685  ulmss  26687  ulmdvlem1  26690  ulmdvlem3  26692  mtest  26694  itgulm  26698  logfaclbnd  27512  bposlem6  27579  caures  38614  caushft  38615  dvgrat  45240  cvgdvgrat  45241  climinf  46540  clim2f  46568  clim2cf  46582  clim0cf  46586  clim2f2  46602  fnlimfvre  46606  allbutfifvre  46607  limsupvaluz2  46670  limsupreuzmpt  46671  supcnvlimsup  46672  climuzlem  46675  climisp  46678  climrescn  46680  climxrrelem  46681  climxrre  46682  limsupgtlem  46709  liminfreuzlem  46734  liminfltlem  46736  liminflimsupclim  46739  xlimpnfxnegmnf  46746  liminflbuz2  46747  liminfpnfuz  46748  liminflimsupxrre  46749  xlimmnfvlem2  46765  xlimmnfv  46766  xlimpnfvlem2  46769  xlimpnfv  46770  xlimmnfmpt  46775  xlimpnfmpt  46776  climxlim2lem  46777  xlimpnfxnegmnf2  46790  meaiuninc3v  47416  smflimlem1  47703  smflimlem2  47704  smflimlem3  47705  smflimmpt  47742  smflimsuplem4  47755  smflimsuplem7  47758  smflimsupmpt  47761  smfliminfmpt  47764