Theorem sstr2 3941

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.)

Assertion

Ref	Expression
sstr2	⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

Proof of Theorem sstr2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		imim1 84	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
2	1	al2imi 1848	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
3		df-ss 3919	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3919	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
5		df-ss 3919	. . 3 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6	4, 5	imbi12i 353	. 2 ⊢ ((𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
7	2, 3, 6	3imtr4i 295	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2145   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ss 3919

This theorem is used by:  sstr  3942  sstri  3943  sseq1  3959  sseq2  3960  ssun3  4129  ssun4  4130  ssinss1OLD  4195  sspw  4571  triun  5231  trintss  5235  exss  5442  frss  5623  relss  5766  funss  6556  funimass2  6620  fss  6723  limsssuc  7850  oaordi  8537  oeworde  8585  nnaordi  8610  sbthlem2  9090  sbthlem3  9091  sbthlem6  9094  domunfican  9295  fiint  9300  fiss  9398  dffi3  9405  inf3lem1  9611  trcl  9711  tcss  9725  ackbij2lem4  10247  cfslb  10272  cfslbn  10273  cfcoflem  10278  coftr  10279  fin23lem15  10340  fin23lem20  10343  fin23lem36  10354  isf32lem1  10359  axdc3lem2  10457  ttukeylem2  10516  wunex2  10751  tskcard  10794  clsslem  15061  mrcss  17710  isacs2  17747  lubss  18607  frmdss2  18978  lsmlub  19797  gsumle  20278  lsslss  21151  lspss  21174  ocv2ss  21892  ocvsscon  21894  lindsss  22043  lsslinds  22050  aspss  22097  mplcoe1  22259  mplcoe5  22262  mdetunilem9  22848  tgss  23199  tgcl  23200  tgss3  23217  clsss  23285  ntrss  23286  neiss  23340  ssnei2  23347  opnnei  23351  cnpnei  23495  cnpco  23498  cncls  23505  cnprest  23520  hauscmp  23638  1stcfb  23676  1stcelcls  23693  reftr  23746  txcnpi  23840  txcnp  23852  txtube  23872  qtoptop2  23931  fgcl  24110  filssufilg  24143  ufileu  24151  uffix  24153  elfm2  24180  fmfnfmlem1  24186  fmco  24193  fbflim2  24209  flffbas  24227  flftg  24228  cnpflf2  24232  alexsubALTlem4  24282  neibl  24733  metcnp3  24772  xlebnum  25199  lebnumii  25200  caubl  25542  caublcls  25543  bcthlem2  25559  bcthlem5  25562  ovolsslem  25718  volsuplem  25789  dyadmbllem  25833  ellimc3  26113  limciun  26128  cpnord  26169  precsexlem6  28485  precsexlem7  28486  ubthlem1  31359  occon3  31786  chsupval  31824  chsupcl  31829  chsupss  31831  spanss  31837  chsupval2  31899  stlei  32729  dmdbr5  32797  mdsl0  32799  chrelat2i  32854  chirredlem1  32879  mdsymlem5  32896  mdsymlem6  32897  gsumvsca1  33674  gsumvsca2  33675  omsmon  34817  cvmliftlem15  35885  ss2mcls  36155  mclsax  36156  clsint2  36956  fgmin  36997  filnetlem4  37008  limsucncmpi  37072  bj-restpw  37850  bj-0int  37859  rdgssun  38140  ptrecube  38377  heiborlem1  38569  heiborlem8  38576  refrelsredund4  39472  refrelredund4  39475  funALTVss  39540  pclssN  40775  dochexmidlem7  42347  incssnn0  43564  islssfg2  43920  hbtlem6  43978  hess  44628  psshepw  44636  clsf2  44974  mnuunid  45109  ismnushort  45133  sspwimpcf  45750  sspwimpcfVD  45751  dvmptfprod  46781  sprsymrelfo  48405  elbigo2  49490  subthinc  50377  setrec1lem2  50622  setrec1lem4  50624  setrec2mpt  50631