Theorem sstr2 2074

Description: Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17.

Assertion

Ref	Expression
sstr2	⊢ (A ⊆ B → (B ⊆ C → A ⊆ C))

Proof of Theorem sstr2

Step	Hyp	Ref	Expression
1		dfss2 2061	. 2 ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
2		imim1 15	. . . 4 ⊢ ((x ∈ A → x ∈ B) → ((x ∈ B → x ∈ C) → (x ∈ A → x ∈ C)))
3	2	19.20ii 997	. . 3 ⊢ (∀x(x ∈ A → x ∈ B) → (∀x(x ∈ B → x ∈ C) → ∀x(x ∈ A → x ∈ C)))
4		dfss2 2061	. . 3 ⊢ (B ⊆ C ↔ ∀x(x ∈ B → x ∈ C))
5		dfss2 2061	. . 3 ⊢ (A ⊆ C ↔ ∀x(x ∈ A → x ∈ C))
6	3, 4, 5	3imtr4g 555	. 2 ⊢ (∀x(x ∈ A → x ∈ B) → (B ⊆ C → A ⊆ C))
7	1, 6	sylbi 199	1 ⊢ (A ⊆ B → (B ⊆ C → A ⊆ C))

Syntax hints:   → wi 3  ∀wal 956   ∈ wcel 960   ⊆ wss 2050

This theorem is referenced by:  sstr 2075  sstri 2076  sseq1 2085  sseq2 2086  ssun3 2198  ssun4 2199  ssin 2235  ssinss1 2240  ssdisj 2322  sspwb 2761  exss 2775  frss 2927  suceloni 3068  limsssuc 3127  relss 3252  cotr 3442  cnvsym 3443  coexg 3530  funimass2 3579  fss 3641  fco 3642  fssxp 3643  tfrlem1 3917  oaordi 4186  oeworde 4226  sbthlem1 4453  sbthlem2 4454  sbthlem3 4455  sbthlem6 4458  fiint 4572  fiintOLD 4573  inf3lem1 4622  trcl 4655  cfle 4925  uzwo3lem2 6219  tgclt 7623  tgsst 7635  tgss2t 7636  clsss 7684  ntrss 7685  neiss 7720  ssnei2 7727  opni3 7863  opnuni 7865  neibl 7874  bcthlem18 8013  chsupval2t 9297  chsupvalt 9298  chsupclt 9303  hsupss 9304  chsupss 9305  spanss 9313  shlej1 9343  shlej1t 9350  chlejb1 9394  stle 10162  dmdbr5 10230  mdsl0 10232  hatomistic 10284  chrelat2 10287  irredlem1 10312  mdsymlem5 10329  mdsymlem6 10330  inposet 10477  filintf 10554  rcfpfil 10569

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056

Copyright terms: Public domain