Theorem cotr 5054

Description: Two ways of saying a relation is transitive. Definition of transitivity in [Schechter] p. 51. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
cotr	|- ( ( R o. R ) C_ R <-> A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) )

Distinct variable group:   x, y, z, R

Proof of Theorem cotr

Step	Hyp	Ref	Expression
1		df-co 4697	. . . 4 |- ( R o. R ) = { <. x , z >. | E. y ( x R y /\ y R z ) }
2	1	relopabi 4810	. . 3 |- Rel ( R o. R )
3		ssrel 4775	. . 3 |- ( Rel ( R o. R ) -> ( ( R o. R ) C_ R <-> A. x A. z ( <. x , z >. e. ( R o. R ) -> <. x , z >. e. R ) ) )
4	2, 3	ax-mp 8	. 2 |- ( ( R o. R ) C_ R <-> A. x A. z ( <. x , z >. e. ( R o. R ) -> <. x , z >. e. R ) )
5		vex 2792	. . . . . . . 8 |- x e. _V
6		vex 2792	. . . . . . . 8 |- z e. _V
7	5, 6	opelco 4852	. . . . . . 7 |- ( <. x , z >. e. ( R o. R ) <-> E. y ( x R y /\ y R z ) )
8		df-br 4025	. . . . . . . 8 |- ( x R z <-> <. x , z >. e. R )
9	8	bicomi 193	. . . . . . 7 |- ( <. x , z >. e. R <-> x R z )
10	7, 9	imbi12i 316	. . . . . 6 |- ( ( <. x , z >. e. ( R o. R ) -> <. x , z >. e. R ) <-> ( E. y ( x R y /\ y R z ) -> x R z ) )
11		19.23v 1834	. . . . . 6 |- ( A. y ( ( x R y /\ y R z ) -> x R z ) <-> ( E. y ( x R y /\ y R z ) -> x R z ) )
12	10, 11	bitr4i 243	. . . . 5 |- ( ( <. x , z >. e. ( R o. R ) -> <. x , z >. e. R ) <-> A. y ( ( x R y /\ y R z ) -> x R z ) )
13	12	albii 1553	. . . 4 |- ( A. z ( <. x , z >. e. ( R o. R ) -> <. x , z >. e. R ) <-> A. z A. y ( ( x R y /\ y R z ) -> x R z ) )
14		alcom 1712	. . . 4 |- ( A. z A. y ( ( x R y /\ y R z ) -> x R z ) <-> A. y A. z ( ( x R y /\ y R z ) -> x R z ) )
15	13, 14	bitri 240	. . 3 |- ( A. z ( <. x , z >. e. ( R o. R ) -> <. x , z >. e. R ) <-> A. y A. z ( ( x R y /\ y R z ) -> x R z ) )
16	15	albii 1553	. 2 |- ( A. x A. z ( <. x , z >. e. ( R o. R ) -> <. x , z >. e. R ) <-> A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) )
17	4, 16	bitri 240	1 |- ( ( R o. R ) C_ R <-> A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) )

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358   A.wal 1527   E.wex 1528   e. wcel 1685   C_ wss 3153   <.cop 3644   class class class wbr 4024   o. ccom 4692   Rel wrel 4693

This theorem is referenced by:  xpidtr  5064  trin2  5065  dfer2  6657  pslem  14311  letsr  14345  dirtr  14354  preotr2  24646  filnetlem3  25740

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025  df-opab 4079  df-xp 4694  df-rel 4695  df-co 4697