| 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 1815 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))) |
| 3 | df-ss 3968 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
| 4 | df-ss 3968 | . . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) | |
| 5 | df-ss 3968 | . . 3 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) | |
| 6 | 4, 5 | imbi12i 350 | . 2 ⊢ ((𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))) |
| 7 | 2, 3, 6 | 3imtr4i 292 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 ∈ wcel 2108 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-ss 3968 |
| This theorem is referenced by: sstr 3992 sstri 3993 sseq1 4009 sseq2 4010 ssun3 4180 ssun4 4181 ssinss1 4246 sspw 4611 triun 5274 trintss 5278 exss 5468 frss 5649 relss 5791 funss 6585 funimass2 6649 fss 6752 sucexeloniOLD 7830 suceloniOLD 7832 limsssuc 7871 oaordi 8584 oeworde 8631 nnaordi 8656 sbthlem2 9124 sbthlem3 9125 sbthlem6 9128 domunfican 9361 fiint 9366 fiintOLD 9367 fiss 9464 dffi3 9471 inf3lem1 9668 trcl 9768 tcss 9784 ac10ct 10074 ackbij2lem4 10281 cfslb 10306 cfslbn 10307 cfcoflem 10312 coftr 10313 fin23lem15 10374 fin23lem20 10377 fin23lem36 10388 isf32lem1 10393 axdc3lem2 10491 ttukeylem2 10550 wunex2 10778 tskcard 10821 clsslem 15023 mrcss 17659 isacs2 17696 lubss 18558 frmdss2 18876 lsmlub 19682 lsslss 20959 lspss 20982 ocv2ss 21691 ocvsscon 21693 lindsss 21844 lsslinds 21851 aspss 21897 mplcoe1 22055 mplcoe5 22058 mdetunilem9 22626 tgss 22975 tgcl 22976 tgss3 22993 clsss 23062 ntrss 23063 neiss 23117 ssnei2 23124 opnnei 23128 cnpnei 23272 cnpco 23275 cncls 23282 cnprest 23297 hauscmp 23415 1stcfb 23453 1stcelcls 23469 reftr 23522 txcnpi 23616 txcnp 23628 txtube 23648 qtoptop2 23707 fgcl 23886 filssufilg 23919 ufileu 23927 uffix 23929 elfm2 23956 fmfnfmlem1 23962 fmco 23969 fbflim2 23985 flffbas 24003 flftg 24004 cnpflf2 24008 alexsubALTlem4 24058 neibl 24514 metcnp3 24553 xlebnum 24997 lebnumii 24998 caubl 25342 caublcls 25343 bcthlem2 25359 bcthlem5 25362 ovolsslem 25519 volsuplem 25590 dyadmbllem 25634 ellimc3 25914 limciun 25929 cpnord 25971 precsexlem6 28236 precsexlem7 28237 ubthlem1 30889 occon3 31316 chsupval 31354 chsupcl 31359 chsupss 31361 spanss 31367 chsupval2 31429 stlei 32259 dmdbr5 32327 mdsl0 32329 chrelat2i 32384 chirredlem1 32409 mdsymlem5 32426 mdsymlem6 32427 gsumle 33101 gsumvsca1 33232 gsumvsca2 33233 omsmon 34300 cvmliftlem15 35303 ss2mcls 35573 mclsax 35574 clsint2 36330 fgmin 36371 filnetlem4 36382 limsucncmpi 36446 bj-restpw 37093 bj-0int 37102 rdgssun 37379 ptrecube 37627 heiborlem1 37818 heiborlem8 37825 refrelsredund4 38633 refrelredund4 38636 funALTVss 38700 pclssN 39896 dochexmidlem7 41468 incssnn0 42722 islssfg2 43083 hbtlem6 43141 hess 43793 psshepw 43801 clsf2 44139 mnuunid 44296 ismnushort 44320 sspwimpcf 44940 sspwimpcfVD 44941 dvmptfprod 45960 sprsymrelfo 47484 elbigo2 48473 subthinc 49092 setrec1lem2 49207 setrec1lem4 49209 setrec2mpt 49216 |
| Copyright terms: Public domain | W3C validator |