Theorem sstr2 3947

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 3925	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3925	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
5		df-ss 3925	. . 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 2146   ⊆ wss 3908

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 3925

This theorem is used by:  sstr  3948  sstri  3949  sseq1  3965  sseq2  3966  ssun3  4136  ssun4  4137  ssinss1OLD  4202  sspw  4578  triun  5238  trintss  5242  exss  5449  frss  5630  relss  5773  funss  6562  funimass2  6626  fss  6729  limsssuc  7855  oaordi  8540  oeworde  8588  nnaordi  8613  sbthlem2  9086  sbthlem3  9087  sbthlem6  9090  domunfican  9291  fiint  9296  fiss  9394  dffi3  9401  inf3lem1  9607  trcl  9707  tcss  9721  ackbij2lem4  10243  cfslb  10268  cfslbn  10269  cfcoflem  10274  coftr  10275  fin23lem15  10336  fin23lem20  10339  fin23lem36  10350  isf32lem1  10355  axdc3lem2  10453  ttukeylem2  10512  wunex2  10741  tskcard  10784  clsslem  15047  mrcss  17697  isacs2  17734  lubss  18594  frmdss2  18953  lsmlub  19765  gsumle  20246  lsslss  21119  lspss  21142  ocv2ss  21860  ocvsscon  21862  lindsss  22011  lsslinds  22018  aspss  22063  mplcoe1  22225  mplcoe5  22228  mdetunilem9  22814  tgss  23162  tgcl  23163  tgss3  23180  clsss  23248  ntrss  23249  neiss  23303  ssnei2  23310  opnnei  23314  cnpnei  23458  cnpco  23461  cncls  23468  cnprest  23483  hauscmp  23601  1stcfb  23639  1stcelcls  23655  reftr  23708  txcnpi  23802  txcnp  23814  txtube  23834  qtoptop2  23893  fgcl  24072  filssufilg  24105  ufileu  24113  uffix  24115  elfm2  24142  fmfnfmlem1  24148  fmco  24155  fbflim2  24171  flffbas  24189  flftg  24190  cnpflf2  24194  alexsubALTlem4  24244  neibl  24695  metcnp3  24734  xlebnum  25161  lebnumii  25162  caubl  25504  caublcls  25505  bcthlem2  25521  bcthlem5  25524  ovolsslem  25680  volsuplem  25751  dyadmbllem  25795  ellimc3  26075  limciun  26090  cpnord  26131  precsexlem6  28442  precsexlem7  28443  ubthlem1  31259  occon3  31686  chsupval  31724  chsupcl  31729  chsupss  31731  spanss  31737  chsupval2  31799  stlei  32629  dmdbr5  32697  mdsl0  32699  chrelat2i  32754  chirredlem1  32779  mdsymlem5  32796  mdsymlem6  32797  gsumvsca1  33577  gsumvsca2  33578  omsmon  34720  cvmliftlem15  35811  ss2mcls  36081  mclsax  36082  clsint2  36881  fgmin  36922  filnetlem4  36933  limsucncmpi  36997  bj-restpw  37775  bj-0int  37784  rdgssun  38065  ptrecube  38312  heiborlem1  38503  heiborlem8  38510  refrelsredund4  39406  refrelredund4  39409  funALTVss  39474  pclssN  40709  dochexmidlem7  42281  incssnn0  43483  islssfg2  43839  hbtlem6  43897  hess  44547  psshepw  44555  clsf2  44893  mnuunid  45028  ismnushort  45052  sspwimpcf  45669  sspwimpcfVD  45670  dvmptfprod  46700  sprsymrelfo  48287  elbigo2  49373  subthinc  50262  setrec1lem2  50507  setrec1lem4  50509  setrec2mpt  50516