![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > uztrn2 | Structured version Visualization version GIF version |
Description: Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013.) |
Ref | Expression |
---|---|
uztrn2.1 | ⊢ 𝑍 = (ℤ≥‘𝐾) |
Ref | Expression |
---|---|
uztrn2 | ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uztrn2.1 | . . . 4 ⊢ 𝑍 = (ℤ≥‘𝐾) | |
2 | 1 | eleq2i 2826 | . . 3 ⊢ (𝑁 ∈ 𝑍 ↔ 𝑁 ∈ (ℤ≥‘𝐾)) |
3 | uztrn 12835 | . . . 4 ⊢ ((𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝑀 ∈ (ℤ≥‘𝐾)) | |
4 | 3 | ancoms 460 | . . 3 ⊢ ((𝑁 ∈ (ℤ≥‘𝐾) ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾)) |
5 | 2, 4 | sylanb 582 | . 2 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ (ℤ≥‘𝐾)) |
6 | 5, 1 | eleqtrrdi 2845 | 1 ⊢ ((𝑁 ∈ 𝑍 ∧ 𝑀 ∈ (ℤ≥‘𝑁)) → 𝑀 ∈ 𝑍) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ‘cfv 6539 ℤ≥cuz 12817 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5297 ax-nul 5304 ax-pow 5361 ax-pr 5425 ax-un 7719 ax-cnex 11161 ax-resscn 11162 ax-pre-lttri 11179 ax-pre-lttrn 11180 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4321 df-if 4527 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4907 df-br 5147 df-opab 5209 df-mpt 5230 df-id 5572 df-xp 5680 df-rel 5681 df-cnv 5682 df-co 5683 df-dm 5684 df-rn 5685 df-res 5686 df-ima 5687 df-iota 6491 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-ov 7406 df-er 8698 df-en 8935 df-dom 8936 df-sdom 8937 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-neg 11442 df-z 12554 df-uz 12818 |
This theorem is referenced by: eluznn0 12896 eluznn 12897 elfzuz2 13501 rexuz3 15290 r19.29uz 15292 r19.2uz 15293 clim2 15443 clim2c 15444 clim0c 15446 rlimclim1 15484 2clim 15511 climabs0 15524 climcn1 15531 climcn2 15532 climsqz 15580 climsqz2 15581 clim2ser 15596 clim2ser2 15597 climub 15603 climsup 15611 caurcvg2 15619 serf0 15622 iseraltlem1 15623 iseralt 15626 cvgcmp 15757 cvgcmpce 15759 isumsup2 15787 mertenslem1 15825 clim2div 15830 ntrivcvgfvn0 15840 ntrivcvgmullem 15842 fprodeq0 15914 lmbrf 22745 lmss 22783 lmres 22785 txlm 23133 uzrest 23382 lmmcvg 24759 lmmbrf 24760 iscau4 24777 iscauf 24778 caucfil 24781 iscmet3lem3 24788 iscmet3lem1 24789 lmle 24799 lmclim 24801 mbflimsup 25164 ulm2 25878 ulmcaulem 25887 ulmcau 25888 ulmss 25890 ulmdvlem1 25893 ulmdvlem3 25895 mtest 25897 itgulm 25901 logfaclbnd 26704 bposlem6 26771 caures 36565 caushft 36566 dvgrat 43003 cvgdvgrat 43004 climinf 44256 clim2f 44286 clim2cf 44300 clim0cf 44304 clim2f2 44320 fnlimfvre 44324 allbutfifvre 44325 limsupvaluz2 44388 limsupreuzmpt 44389 supcnvlimsup 44390 climuzlem 44393 climisp 44396 climrescn 44398 climxrrelem 44399 climxrre 44400 limsupgtlem 44427 liminfreuzlem 44452 liminfltlem 44454 liminflimsupclim 44457 xlimpnfxnegmnf 44464 liminflbuz2 44465 liminfpnfuz 44466 liminflimsupxrre 44467 xlimmnfvlem2 44483 xlimmnfv 44484 xlimpnfvlem2 44487 xlimpnfv 44488 xlimmnfmpt 44493 xlimpnfmpt 44494 climxlim2lem 44495 xlimpnfxnegmnf2 44508 meaiuninc3v 45134 smflimlem1 45421 smflimlem2 45422 smflimlem3 45423 smflimmpt 45460 smflimsuplem4 45473 smflimsuplem7 45476 smflimsupmpt 45479 smfliminfmpt 45482 |
Copyright terms: Public domain | W3C validator |