![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sstr2 | Structured version Visualization version GIF version |
Description: Transitivity of subclass relationship. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) Avoid axioms. (Revised by GG, 19-May-2025.) |
Ref | Expression |
---|---|
sstr2 | ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imim1 83 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))) | |
2 | 1 | al2imi 1809 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))) |
3 | df-ss 3961 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
4 | df-ss 3961 | . . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) | |
5 | df-ss 3961 | . . 3 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) | |
6 | 4, 5 | imbi12i 349 | . 2 ⊢ ((𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))) |
7 | 2, 3, 6 | 3imtr4i 291 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1531 ∈ wcel 2098 ⊆ wss 3944 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 |
This theorem depends on definitions: df-bi 206 df-ss 3961 |
This theorem is referenced by: sstr 3985 sstri 3986 sseq1 4002 sseq2 4003 ssun3 4172 ssun4 4173 ssinss1 4236 sspw 4615 triun 5281 trintss 5285 exss 5465 frss 5645 relss 5783 funss 6573 funimass2 6637 fss 6739 sucexeloniOLD 7814 suceloniOLD 7816 limsssuc 7855 oaordi 8567 oeworde 8614 nnaordi 8639 sbthlem2 9109 sbthlem3 9110 sbthlem6 9113 domunfican 9346 fiint 9350 fiss 9449 dffi3 9456 inf3lem1 9653 trcl 9753 tcss 9769 ac10ct 10059 ackbij2lem4 10267 cfslb 10291 cfslbn 10292 cfcoflem 10297 coftr 10298 fin23lem15 10359 fin23lem20 10362 fin23lem36 10373 isf32lem1 10378 axdc3lem2 10476 ttukeylem2 10535 wunex2 10763 tskcard 10806 clsslem 14967 mrcss 17599 isacs2 17636 lubss 18508 frmdss2 18823 lsmlub 19631 lsslss 20857 lspss 20880 ocv2ss 21622 ocvsscon 21624 lindsss 21775 lsslinds 21782 aspss 21827 mplcoe1 21997 mplcoe5 22000 mdetunilem9 22566 tgss 22915 tgcl 22916 tgss3 22933 clsss 23002 ntrss 23003 neiss 23057 ssnei2 23064 opnnei 23068 cnpnei 23212 cnpco 23215 cncls 23222 cnprest 23237 hauscmp 23355 1stcfb 23393 1stcelcls 23409 reftr 23462 txcnpi 23556 txcnp 23568 txtube 23588 qtoptop2 23647 fgcl 23826 filssufilg 23859 ufileu 23867 uffix 23869 elfm2 23896 fmfnfmlem1 23902 fmco 23909 fbflim2 23925 flffbas 23943 flftg 23944 cnpflf2 23948 alexsubALTlem4 23998 neibl 24454 metcnp3 24493 xlebnum 24935 lebnumii 24936 caubl 25280 caublcls 25281 bcthlem2 25297 bcthlem5 25300 ovolsslem 25457 volsuplem 25528 dyadmbllem 25572 ellimc3 25852 limciun 25867 cpnord 25909 precsexlem6 28160 precsexlem7 28161 ubthlem1 30752 occon3 31179 chsupval 31217 chsupcl 31222 chsupss 31224 spanss 31230 chsupval2 31292 stlei 32122 dmdbr5 32190 mdsl0 32192 chrelat2i 32247 chirredlem1 32272 mdsymlem5 32289 mdsymlem6 32290 gsumle 32894 gsumvsca1 33025 gsumvsca2 33026 omsmon 34046 cvmliftlem15 35036 ss2mcls 35306 mclsax 35307 clsint2 35941 fgmin 35982 filnetlem4 35993 limsucncmpi 36057 bj-restpw 36699 bj-0int 36708 rdgssun 36985 ptrecube 37221 heiborlem1 37412 heiborlem8 37419 refrelsredund4 38231 refrelredund4 38234 funALTVss 38298 pclssN 39494 dochexmidlem7 41066 incssnn0 42270 islssfg2 42634 hbtlem6 42692 hess 43349 psshepw 43357 clsf2 43695 mnuunid 43853 ismnushort 43877 sspwimpcf 44498 sspwimpcfVD 44499 dvmptfprod 45468 sprsymrelfo 46971 elbigo2 47808 subthinc 48229 setrec1lem2 48302 setrec1lem4 48304 setrec2mpt 48311 |
Copyright terms: Public domain | W3C validator |