Theorem sstr2 3937

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 83	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
2	1	al2imi 1816	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
3		df-ss 3915	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3915	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
5		df-ss 3915	. . 3 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6	4, 5	imbi12i 350	. 2 ⊢ ((𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
7	2, 3, 6	3imtr4i 292	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2113   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 207  df-ss 3915

This theorem is referenced by:  sstr  3939  sstri  3940  sseq1  3956  sseq2  3957  ssun3  4129  ssun4  4130  ssinss1  4195  sspw  4560  triun  5214  trintss  5218  exss  5406  frss  5583  relss  5726  funss  6505  funimass2  6569  fss  6672  limsssuc  7786  oaordi  8467  oeworde  8514  nnaordi  8539  sbthlem2  9008  sbthlem3  9009  sbthlem6  9012  domunfican  9213  fiint  9218  fiss  9315  dffi3  9322  inf3lem1  9525  trcl  9625  tcss  9639  ac10ct  9932  ackbij2lem4  10139  cfslb  10164  cfslbn  10165  cfcoflem  10170  coftr  10171  fin23lem15  10232  fin23lem20  10235  fin23lem36  10246  isf32lem1  10251  axdc3lem2  10349  ttukeylem2  10408  wunex2  10636  tskcard  10679  clsslem  14893  mrcss  17524  isacs2  17561  lubss  18421  frmdss2  18773  lsmlub  19578  gsumle  20059  lsslss  20896  lspss  20919  ocv2ss  21612  ocvsscon  21614  lindsss  21763  lsslinds  21770  aspss  21816  mplcoe1  21973  mplcoe5  21976  mdetunilem9  22536  tgss  22884  tgcl  22885  tgss3  22902  clsss  22970  ntrss  22971  neiss  23025  ssnei2  23032  opnnei  23036  cnpnei  23180  cnpco  23183  cncls  23190  cnprest  23205  hauscmp  23323  1stcfb  23361  1stcelcls  23377  reftr  23430  txcnpi  23524  txcnp  23536  txtube  23556  qtoptop2  23615  fgcl  23794  filssufilg  23827  ufileu  23835  uffix  23837  elfm2  23864  fmfnfmlem1  23870  fmco  23877  fbflim2  23893  flffbas  23911  flftg  23912  cnpflf2  23916  alexsubALTlem4  23966  neibl  24417  metcnp3  24456  xlebnum  24892  lebnumii  24893  caubl  25236  caublcls  25237  bcthlem2  25253  bcthlem5  25256  ovolsslem  25413  volsuplem  25484  dyadmbllem  25528  ellimc3  25808  limciun  25823  cpnord  25865  precsexlem6  28151  precsexlem7  28152  ubthlem1  30852  occon3  31279  chsupval  31317  chsupcl  31322  chsupss  31324  spanss  31330  chsupval2  31392  stlei  32222  dmdbr5  32290  mdsl0  32292  chrelat2i  32347  chirredlem1  32372  mdsymlem5  32389  mdsymlem6  32390  gsumvsca1  33202  gsumvsca2  33203  omsmon  34332  cvmliftlem15  35363  ss2mcls  35633  mclsax  35634  clsint2  36394  fgmin  36435  filnetlem4  36446  limsucncmpi  36510  bj-restpw  37157  bj-0int  37166  rdgssun  37443  ptrecube  37680  heiborlem1  37871  heiborlem8  37878  refrelsredund4  38748  refrelredund4  38751  funALTVss  38817  pclssN  40013  dochexmidlem7  41585  incssnn0  42828  islssfg2  43188  hbtlem6  43246  hess  43897  psshepw  43905  clsf2  44243  mnuunid  44394  ismnushort  44418  sspwimpcf  45036  sspwimpcfVD  45037  dvmptfprod  46067  sprsymrelfo  47621  elbigo2  48677  subthinc  49568  setrec1lem2  49813  setrec1lem4  49815  setrec2mpt  49822