Theorem trer 32310

Description: A relation intersected with its converse is an equivalence relation if the relation is transitive. (Contributed by Jeff Hankins, 6-Oct-2009.) (Revised by Mario Carneiro, 12-Aug-2015.)

Assertion

Ref	Expression
trer	|- ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> ( .<_ i^i `' .<_ ) Er dom ( .<_ i^i `' .<_ ) )

Distinct variable group:   a, b, c, .<_

Proof of Theorem trer

Dummy variables r s t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss2 3834	. . . 4 |- ( .<_ i^i `' .<_ ) C_ `' .<_
2		relcnv 5503	. . . 4 |- Rel `' .<_
3		relss 5206	. . . 4 |- ( ( .<_ i^i `' .<_ ) C_ `' .<_ -> ( Rel `' .<_ -> Rel ( .<_ i^i `' .<_ ) ) )
4	1, 2, 3	mp2 9	. . 3 |- Rel ( .<_ i^i `' .<_ )
5	4	a1i 11	. 2 |- ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> Rel ( .<_ i^i `' .<_ ) )
6		eqidd 2623	. 2 |- ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> dom ( .<_ i^i `' .<_ ) = dom ( .<_ i^i `' .<_ ) )
7		brin 4704	. . . . . . . 8 |- ( r ( .<_ i^i `' .<_ ) s <-> ( r .<_ s /\ r `' .<_ s ) )
8		vex 3203	. . . . . . . . . 10 |- r e. _V
9		vex 3203	. . . . . . . . . 10 |- s e. _V
10	8, 9	brcnv 5305	. . . . . . . . 9 |- ( r `' .<_ s <-> s .<_ r )
11	10	anbi2i 730	. . . . . . . 8 |- ( ( r .<_ s /\ r `' .<_ s ) <-> ( r .<_ s /\ s .<_ r ) )
12	7, 11	bitri 264	. . . . . . 7 |- ( r ( .<_ i^i `' .<_ ) s <-> ( r .<_ s /\ s .<_ r ) )
13		brin 4704	. . . . . . . 8 |- ( s ( .<_ i^i `' .<_ ) t <-> ( s .<_ t /\ s `' .<_ t ) )
14		vex 3203	. . . . . . . . . 10 |- t e. _V
15	9, 14	brcnv 5305	. . . . . . . . 9 |- ( s `' .<_ t <-> t .<_ s )
16	15	anbi2i 730	. . . . . . . 8 |- ( ( s .<_ t /\ s `' .<_ t ) <-> ( s .<_ t /\ t .<_ s ) )
17	13, 16	bitri 264	. . . . . . 7 |- ( s ( .<_ i^i `' .<_ ) t <-> ( s .<_ t /\ t .<_ s ) )
18	12, 17	anbi12i 733	. . . . . 6 |- ( ( r ( .<_ i^i `' .<_ ) s /\ s ( .<_ i^i `' .<_ ) t ) <-> ( ( r .<_ s /\ s .<_ r ) /\ ( s .<_ t /\ t .<_ s ) ) )
19		breq1 4656	. . . . . . . . . . . . 13 |- ( a = r -> ( a .<_ b <-> r .<_ b ) )
20	19	anbi1d 741	. . . . . . . . . . . 12 |- ( a = r -> ( ( a .<_ b /\ b .<_ c ) <-> ( r .<_ b /\ b .<_ c ) ) )
21		breq1 4656	. . . . . . . . . . . 12 |- ( a = r -> ( a .<_ c <-> r .<_ c ) )
22	20, 21	imbi12d 334	. . . . . . . . . . 11 |- ( a = r -> ( ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) <-> ( ( r .<_ b /\ b .<_ c ) -> r .<_ c ) ) )
23	22	2albidv 1851	. . . . . . . . . 10 |- ( a = r -> ( A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) <-> A. b A. c ( ( r .<_ b /\ b .<_ c ) -> r .<_ c ) ) )
24	23	spv 2260	. . . . . . . . 9 |- ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> A. b A. c ( ( r .<_ b /\ b .<_ c ) -> r .<_ c ) )
25		breq2 4657	. . . . . . . . . . . . 13 |- ( b = s -> ( r .<_ b <-> r .<_ s ) )
26		breq1 4656	. . . . . . . . . . . . 13 |- ( b = s -> ( b .<_ c <-> s .<_ c ) )
27	25, 26	anbi12d 747	. . . . . . . . . . . 12 |- ( b = s -> ( ( r .<_ b /\ b .<_ c ) <-> ( r .<_ s /\ s .<_ c ) ) )
28	27	imbi1d 331	. . . . . . . . . . 11 |- ( b = s -> ( ( ( r .<_ b /\ b .<_ c ) -> r .<_ c ) <-> ( ( r .<_ s /\ s .<_ c ) -> r .<_ c ) ) )
29	28	albidv 1849	. . . . . . . . . 10 |- ( b = s -> ( A. c ( ( r .<_ b /\ b .<_ c ) -> r .<_ c ) <-> A. c ( ( r .<_ s /\ s .<_ c ) -> r .<_ c ) ) )
30	29	spv 2260	. . . . . . . . 9 |- ( A. b A. c ( ( r .<_ b /\ b .<_ c ) -> r .<_ c ) -> A. c ( ( r .<_ s /\ s .<_ c ) -> r .<_ c ) )
31		breq2 4657	. . . . . . . . . . . 12 |- ( c = t -> ( s .<_ c <-> s .<_ t ) )
32	31	anbi2d 740	. . . . . . . . . . 11 |- ( c = t -> ( ( r .<_ s /\ s .<_ c ) <-> ( r .<_ s /\ s .<_ t ) ) )
33		breq2 4657	. . . . . . . . . . 11 |- ( c = t -> ( r .<_ c <-> r .<_ t ) )
34	32, 33	imbi12d 334	. . . . . . . . . 10 |- ( c = t -> ( ( ( r .<_ s /\ s .<_ c ) -> r .<_ c ) <-> ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) ) )
35	34	spv 2260	. . . . . . . . 9 |- ( A. c ( ( r .<_ s /\ s .<_ c ) -> r .<_ c ) -> ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) )
36		pm3.3 460	. . . . . . . . . . . . . 14 |- ( ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) -> ( r .<_ s -> ( s .<_ t -> r .<_ t ) ) )
37	36	com23 86	. . . . . . . . . . . . 13 |- ( ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) -> ( s .<_ t -> ( r .<_ s -> r .<_ t ) ) )
38	37	adantrd 484	. . . . . . . . . . . 12 |- ( ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) -> ( ( s .<_ t /\ t .<_ s ) -> ( r .<_ s -> r .<_ t ) ) )
39	38	com23 86	. . . . . . . . . . 11 |- ( ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) -> ( r .<_ s -> ( ( s .<_ t /\ t .<_ s ) -> r .<_ t ) ) )
40	39	adantrd 484	. . . . . . . . . 10 |- ( ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) -> ( ( r .<_ s /\ s .<_ r ) -> ( ( s .<_ t /\ t .<_ s ) -> r .<_ t ) ) )
41	40	impd 447	. . . . . . . . 9 |- ( ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) -> ( ( ( r .<_ s /\ s .<_ r ) /\ ( s .<_ t /\ t .<_ s ) ) -> r .<_ t ) )
42	24, 30, 35, 41	4syl 19	. . . . . . . 8 |- ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> ( ( ( r .<_ s /\ s .<_ r ) /\ ( s .<_ t /\ t .<_ s ) ) -> r .<_ t ) )
43		breq1 4656	. . . . . . . . . . . . 13 |- ( a = t -> ( a .<_ b <-> t .<_ b ) )
44	43	anbi1d 741	. . . . . . . . . . . 12 |- ( a = t -> ( ( a .<_ b /\ b .<_ c ) <-> ( t .<_ b /\ b .<_ c ) ) )
45		breq1 4656	. . . . . . . . . . . 12 |- ( a = t -> ( a .<_ c <-> t .<_ c ) )
46	44, 45	imbi12d 334	. . . . . . . . . . 11 |- ( a = t -> ( ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) <-> ( ( t .<_ b /\ b .<_ c ) -> t .<_ c ) ) )
47	46	2albidv 1851	. . . . . . . . . 10 |- ( a = t -> ( A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) <-> A. b A. c ( ( t .<_ b /\ b .<_ c ) -> t .<_ c ) ) )
48	47	spv 2260	. . . . . . . . 9 |- ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> A. b A. c ( ( t .<_ b /\ b .<_ c ) -> t .<_ c ) )
49		breq2 4657	. . . . . . . . . . . . 13 |- ( b = s -> ( t .<_ b <-> t .<_ s ) )
50	49, 26	anbi12d 747	. . . . . . . . . . . 12 |- ( b = s -> ( ( t .<_ b /\ b .<_ c ) <-> ( t .<_ s /\ s .<_ c ) ) )
51	50	imbi1d 331	. . . . . . . . . . 11 |- ( b = s -> ( ( ( t .<_ b /\ b .<_ c ) -> t .<_ c ) <-> ( ( t .<_ s /\ s .<_ c ) -> t .<_ c ) ) )
52	51	albidv 1849	. . . . . . . . . 10 |- ( b = s -> ( A. c ( ( t .<_ b /\ b .<_ c ) -> t .<_ c ) <-> A. c ( ( t .<_ s /\ s .<_ c ) -> t .<_ c ) ) )
53	52	spv 2260	. . . . . . . . 9 |- ( A. b A. c ( ( t .<_ b /\ b .<_ c ) -> t .<_ c ) -> A. c ( ( t .<_ s /\ s .<_ c ) -> t .<_ c ) )
54		breq2 4657	. . . . . . . . . . . 12 |- ( c = r -> ( s .<_ c <-> s .<_ r ) )
55	54	anbi2d 740	. . . . . . . . . . 11 |- ( c = r -> ( ( t .<_ s /\ s .<_ c ) <-> ( t .<_ s /\ s .<_ r ) ) )
56		breq2 4657	. . . . . . . . . . 11 |- ( c = r -> ( t .<_ c <-> t .<_ r ) )
57	55, 56	imbi12d 334	. . . . . . . . . 10 |- ( c = r -> ( ( ( t .<_ s /\ s .<_ c ) -> t .<_ c ) <-> ( ( t .<_ s /\ s .<_ r ) -> t .<_ r ) ) )
58	57	spv 2260	. . . . . . . . 9 |- ( A. c ( ( t .<_ s /\ s .<_ c ) -> t .<_ c ) -> ( ( t .<_ s /\ s .<_ r ) -> t .<_ r ) )
59		pm3.3 460	. . . . . . . . . . . . 13 |- ( ( ( t .<_ s /\ s .<_ r ) -> t .<_ r ) -> ( t .<_ s -> ( s .<_ r -> t .<_ r ) ) )
60	59	adantld 483	. . . . . . . . . . . 12 |- ( ( ( t .<_ s /\ s .<_ r ) -> t .<_ r ) -> ( ( s .<_ t /\ t .<_ s ) -> ( s .<_ r -> t .<_ r ) ) )
61	60	com23 86	. . . . . . . . . . 11 |- ( ( ( t .<_ s /\ s .<_ r ) -> t .<_ r ) -> ( s .<_ r -> ( ( s .<_ t /\ t .<_ s ) -> t .<_ r ) ) )
62	61	adantld 483	. . . . . . . . . 10 |- ( ( ( t .<_ s /\ s .<_ r ) -> t .<_ r ) -> ( ( r .<_ s /\ s .<_ r ) -> ( ( s .<_ t /\ t .<_ s ) -> t .<_ r ) ) )
63	62	impd 447	. . . . . . . . 9 |- ( ( ( t .<_ s /\ s .<_ r ) -> t .<_ r ) -> ( ( ( r .<_ s /\ s .<_ r ) /\ ( s .<_ t /\ t .<_ s ) ) -> t .<_ r ) )
64	48, 53, 58, 63	4syl 19	. . . . . . . 8 |- ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> ( ( ( r .<_ s /\ s .<_ r ) /\ ( s .<_ t /\ t .<_ s ) ) -> t .<_ r ) )
65	42, 64	jcad 555	. . . . . . 7 |- ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> ( ( ( r .<_ s /\ s .<_ r ) /\ ( s .<_ t /\ t .<_ s ) ) -> ( r .<_ t /\ t .<_ r ) ) )
66		brin 4704	. . . . . . . 8 |- ( r ( .<_ i^i `' .<_ ) t <-> ( r .<_ t /\ r `' .<_ t ) )
67	8, 14	brcnv 5305	. . . . . . . . 9 |- ( r `' .<_ t <-> t .<_ r )
68	67	anbi2i 730	. . . . . . . 8 |- ( ( r .<_ t /\ r `' .<_ t ) <-> ( r .<_ t /\ t .<_ r ) )
69	66, 68	bitr2i 265	. . . . . . 7 |- ( ( r .<_ t /\ t .<_ r ) <-> r ( .<_ i^i `' .<_ ) t )
70	65, 69	syl6ib 241	. . . . . 6 |- ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> ( ( ( r .<_ s /\ s .<_ r ) /\ ( s .<_ t /\ t .<_ s ) ) -> r ( .<_ i^i `' .<_ ) t ) )
71	18, 70	syl5bi 232	. . . . 5 |- ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> ( ( r ( .<_ i^i `' .<_ ) s /\ s ( .<_ i^i `' .<_ ) t ) -> r ( .<_ i^i `' .<_ ) t ) )
72	9, 8	brcnv 5305	. . . . . . . . 9 |- ( s `' .<_ r <-> r .<_ s )
73	72	bicomi 214	. . . . . . . 8 |- ( r .<_ s <-> s `' .<_ r )
74	73, 10	anbi12ci 734	. . . . . . 7 |- ( ( r .<_ s /\ r `' .<_ s ) <-> ( s .<_ r /\ s `' .<_ r ) )
75		brin 4704	. . . . . . 7 |- ( s ( .<_ i^i `' .<_ ) r <-> ( s .<_ r /\ s `' .<_ r ) )
76	74, 7, 75	3bitr4i 292	. . . . . 6 |- ( r ( .<_ i^i `' .<_ ) s <-> s ( .<_ i^i `' .<_ ) r )
77	76	biimpi 206	. . . . 5 |- ( r ( .<_ i^i `' .<_ ) s -> s ( .<_ i^i `' .<_ ) r )
78	71, 77	jctil 560	. . . 4 |- ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> ( ( r ( .<_ i^i `' .<_ ) s -> s ( .<_ i^i `' .<_ ) r ) /\ ( ( r ( .<_ i^i `' .<_ ) s /\ s ( .<_ i^i `' .<_ ) t ) -> r ( .<_ i^i `' .<_ ) t ) ) )
79	78	alrimiv 1855	. . 3 |- ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> A. t ( ( r ( .<_ i^i `' .<_ ) s -> s ( .<_ i^i `' .<_ ) r ) /\ ( ( r ( .<_ i^i `' .<_ ) s /\ s ( .<_ i^i `' .<_ ) t ) -> r ( .<_ i^i `' .<_ ) t ) ) )
80	79	alrimivv 1856	. 2 |- ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> A. r A. s A. t ( ( r ( .<_ i^i `' .<_ ) s -> s ( .<_ i^i `' .<_ ) r ) /\ ( ( r ( .<_ i^i `' .<_ ) s /\ s ( .<_ i^i `' .<_ ) t ) -> r ( .<_ i^i `' .<_ ) t ) ) )
81		dfer2 7743	. 2 |- ( ( .<_ i^i `' .<_ ) Er dom ( .<_ i^i `' .<_ ) <-> ( Rel ( .<_ i^i `' .<_ ) /\ dom ( .<_ i^i `' .<_ ) = dom ( .<_ i^i `' .<_ ) /\ A. r A. s A. t ( ( r ( .<_ i^i `' .<_ ) s -> s ( .<_ i^i `' .<_ ) r ) /\ ( ( r ( .<_ i^i `' .<_ ) s /\ s ( .<_ i^i `' .<_ ) t ) -> r ( .<_ i^i `' .<_ ) t ) ) ) )
82	5, 6, 80, 81	syl3anbrc 1246	1 |- ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> ( .<_ i^i `' .<_ ) Er dom ( .<_ i^i `' .<_ ) )

Syntax hints:   -> wi 4   /\ wa 384   A.wal 1481   = wceq 1483   i^i cin 3573   C_ wss 3574   class class class wbr 4653   `'ccnv 5113   dom cdm 5114   Rel wrel 5119   Er wer 7739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-er 7742

This theorem is referenced by: (None)