Theorem uztrn2 12457

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 12456	. . . 4 ⊢ ((𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝑀 ∈ (ℤ≥‘𝐾))
4	3	ancoms 462	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
5	2, 4	sylanb 584	. 2 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾))
6	5, 1	eleqtrrdi 2849	1 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2110  ‘cfv 6380  ℤ_≥cuz 12438

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 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-pre-lttri 10803  ax-pre-lttrn 10804

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-ov 7216  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-neg 11065  df-z 12177  df-uz 12439

This theorem is referenced by:  eluznn0  12513  eluznn  12514  elfzuz2  13117  rexuz3  14912  r19.29uz  14914  r19.2uz  14915  clim2  15065  clim2c  15066  clim0c  15068  rlimclim1  15106  2clim  15133  climabs0  15146  climcn1  15153  climcn2  15154  climsqz  15202  climsqz2  15203  clim2ser  15218  clim2ser2  15219  climub  15225  climsup  15233  caurcvg2  15241  serf0  15244  iseraltlem1  15245  iseralt  15248  cvgcmp  15380  cvgcmpce  15382  isumsup2  15410  mertenslem1  15448  clim2div  15453  ntrivcvgfvn0  15463  ntrivcvgmullem  15465  fprodeq0  15537  lmbrf  22157  lmss  22195  lmres  22197  txlm  22545  uzrest  22794  lmmcvg  24158  lmmbrf  24159  iscau4  24176  iscauf  24177  caucfil  24180  iscmet3lem3  24187  iscmet3lem1  24188  lmle  24198  lmclim  24200  mbflimsup  24563  ulm2  25277  ulmcaulem  25286  ulmcau  25287  ulmss  25289  ulmdvlem1  25292  ulmdvlem3  25294  mtest  25296  itgulm  25300  logfaclbnd  26103  bposlem6  26170  caures  35655  caushft  35656  dvgrat  41603  cvgdvgrat  41604  climinf  42822  clim2f  42852  clim2cf  42866  clim0cf  42870  clim2f2  42886  fnlimfvre  42890  allbutfifvre  42891  limsupvaluz2  42954  limsupreuzmpt  42955  supcnvlimsup  42956  climuzlem  42959  climisp  42962  climrescn  42964  climxrrelem  42965  climxrre  42966  limsupgtlem  42993  liminfreuzlem  43018  liminfltlem  43020  liminflimsupclim  43023  xlimpnfxnegmnf  43030  liminflbuz2  43031  liminfpnfuz  43032  liminflimsupxrre  43033  xlimmnfvlem2  43049  xlimmnfv  43050  xlimpnfvlem2  43053  xlimpnfv  43054  xlimmnfmpt  43059  xlimpnfmpt  43060  climxlim2lem  43061  xlimpnfxnegmnf2  43074  meaiuninc3v  43697  smflimlem1  43978  smflimlem2  43979  smflimlem3  43980  smflimmpt  44015  smflimsuplem4  44028  smflimsuplem7  44031  smflimsupmpt  44034  smfliminfmpt  44037