Theorem sstr2 1510

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 1497	. 2 |- (A (_ B <-> A.x(x e. A -> x e. B))
2		syl2 17	. . . 4 |- ((x e. A -> x e. B) -> ((x e. B -> x e. C) -> (x e. A -> x e. C)))
3	2	19.20ii 692	. . 3 |- (A.x(x e. A -> x e. B) -> (A.x(x e. B -> x e. C) -> A.x(x e. A -> x e. C)))
4		dfss2 1497	. . 3 |- (B (_ C <-> A.x(x e. B -> x e. C))
5		dfss2 1497	. . 3 |- (A (_ C <-> A.x(x e. A -> x e. C))
6	3, 4, 5	3imtr4g 426	. 2 |- (A.x(x e. A -> x e. B) -> (B (_ C -> A (_ C))
7	1, 6	sylbi 174	1 |- (A (_ B -> (B (_ C -> A (_ C))

Syntax hints:   -> wi 2  A.wal 672   e. wcel 1092   (_ wss 1487

This theorem is referenced by:  sstr 1511  sstri 1512  sseq1 1521  sseq2 1522  ssun3 1623  ssun4 1624  ssin 1659  ssinss1 1664  sspwb 1863  exss 1881  frss 2173  suceloni 2314  limsssuc 2362  ssrel 2479  cotr 2625  cnvsym 2626  coexg 2671  funimass2 2713  fss 2759  fco 2760  fssxp 2761  tfrlem1 2949  oaordi 3148  nnmordi 3188  sbthlem1 3349  sbthlem2 3350  sbthlem3 3351  sbthlem6 3354  fiint 3445  inf3lem1 3464  trcl 3489  cfle 3708  uzwo3lem2 4615  chsupval2t 5303  chsupvalt 5304  chsupclt 5309  hsupss 5310  chsupss 5311  spanss 5319  shlej1 5349  shlej1t 5356  chlejb1 5397  stle 5681  hatomistic 5755  chrelat2 5758  mdsymlem5 5780  mdsymlem6 5781

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-in 1491  df-ss 1492

metamath.org