Metamath Proof Explorer

Theorem trer

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)

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

Proof

Step Hyp Ref Expression
1 inss2 
 |-  ( .<_ i^i `' .<_ ) C_ `' .<_
2 relcnv 
 |-  Rel `' .<_
3 relss 
 |-  ( ( .<_ i^i `' .<_ ) C_ `' .<_ -> ( Rel `' .<_ -> Rel ( .<_ i^i `' .<_ ) ) )
4 1 2 3 mp2 
 |-  Rel ( .<_ i^i `' .<_ )
5 4 a1i 
 |-  ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> Rel ( .<_ i^i `' .<_ ) )
6 eqidd 
 |-  ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> dom ( .<_ i^i `' .<_ ) = dom ( .<_ i^i `' .<_ ) )
7 brin 
 |-  ( r ( .<_ i^i `' .<_ ) s <-> ( r .<_ s /\ r `' .<_ s ) )
8 vex 
 |-  r e. _V
9 vex 
 |-  s e. _V
10 8 9 brcnv 
 |-  ( r `' .<_ s <-> s .<_ r )
11 10 anbi2i 
 |-  ( ( r .<_ s /\ r `' .<_ s ) <-> ( r .<_ s /\ s .<_ r ) )
12 7 11 bitri 
 |-  ( r ( .<_ i^i `' .<_ ) s <-> ( r .<_ s /\ s .<_ r ) )
13 brin 
 |-  ( s ( .<_ i^i `' .<_ ) t <-> ( s .<_ t /\ s `' .<_ t ) )
14 vex 
 |-  t e. _V
15 9 14 brcnv 
 |-  ( s `' .<_ t <-> t .<_ s )
16 15 anbi2i 
 |-  ( ( s .<_ t /\ s `' .<_ t ) <-> ( s .<_ t /\ t .<_ s ) )
17 13 16 bitri 
 |-  ( s ( .<_ i^i `' .<_ ) t <-> ( s .<_ t /\ t .<_ s ) )
18 12 17 anbi12i 
 |-  ( ( r ( .<_ i^i `' .<_ ) s /\ s ( .<_ i^i `' .<_ ) t ) <-> ( ( r .<_ s /\ s .<_ r ) /\ ( s .<_ t /\ t .<_ s ) ) )
19 breq1 
 |-  ( a = r -> ( a .<_ b <-> r .<_ b ) )
20 19 anbi1d 
 |-  ( a = r -> ( ( a .<_ b /\ b .<_ c ) <-> ( r .<_ b /\ b .<_ c ) ) )
21 breq1 
 |-  ( a = r -> ( a .<_ c <-> r .<_ c ) )
22 20 21 imbi12d 
 |-  ( a = r -> ( ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) <-> ( ( r .<_ b /\ b .<_ c ) -> r .<_ c ) ) )
23 22 2albidv 
 |-  ( a = r -> ( A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) <-> A. b A. c ( ( r .<_ b /\ b .<_ c ) -> r .<_ c ) ) )
24 23 spvv 
 |-  ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> A. b A. c ( ( r .<_ b /\ b .<_ c ) -> r .<_ c ) )
25 breq2 
 |-  ( b = s -> ( r .<_ b <-> r .<_ s ) )
26 breq1 
 |-  ( b = s -> ( b .<_ c <-> s .<_ c ) )
27 25 26 anbi12d 
 |-  ( b = s -> ( ( r .<_ b /\ b .<_ c ) <-> ( r .<_ s /\ s .<_ c ) ) )
28 27 imbi1d 
 |-  ( b = s -> ( ( ( r .<_ b /\ b .<_ c ) -> r .<_ c ) <-> ( ( r .<_ s /\ s .<_ c ) -> r .<_ c ) ) )
29 28 albidv 
 |-  ( b = s -> ( A. c ( ( r .<_ b /\ b .<_ c ) -> r .<_ c ) <-> A. c ( ( r .<_ s /\ s .<_ c ) -> r .<_ c ) ) )
30 29 spvv 
 |-  ( A. b A. c ( ( r .<_ b /\ b .<_ c ) -> r .<_ c ) -> A. c ( ( r .<_ s /\ s .<_ c ) -> r .<_ c ) )
31 breq2 
 |-  ( c = t -> ( s .<_ c <-> s .<_ t ) )
32 31 anbi2d 
 |-  ( c = t -> ( ( r .<_ s /\ s .<_ c ) <-> ( r .<_ s /\ s .<_ t ) ) )
33 breq2 
 |-  ( c = t -> ( r .<_ c <-> r .<_ t ) )
34 32 33 imbi12d 
 |-  ( c = t -> ( ( ( r .<_ s /\ s .<_ c ) -> r .<_ c ) <-> ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) ) )
35 34 spvv 
 |-  ( A. c ( ( r .<_ s /\ s .<_ c ) -> r .<_ c ) -> ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) )
36 pm3.3 
 |-  ( ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) -> ( r .<_ s -> ( s .<_ t -> r .<_ t ) ) )
37 36 com23 
 |-  ( ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) -> ( s .<_ t -> ( r .<_ s -> r .<_ t ) ) )
38 37 adantrd 
 |-  ( ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) -> ( ( s .<_ t /\ t .<_ s ) -> ( r .<_ s -> r .<_ t ) ) )
39 38 com23 
 |-  ( ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) -> ( r .<_ s -> ( ( s .<_ t /\ t .<_ s ) -> r .<_ t ) ) )
40 39 adantrd 
 |-  ( ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) -> ( ( r .<_ s /\ s .<_ r ) -> ( ( s .<_ t /\ t .<_ s ) -> r .<_ t ) ) )
41 40 impd 
 |-  ( ( ( r .<_ s /\ s .<_ t ) -> r .<_ t ) -> ( ( ( r .<_ s /\ s .<_ r ) /\ ( s .<_ t /\ t .<_ s ) ) -> r .<_ t ) )
42 24 30 35 41 4syl 
 |-  ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> ( ( ( r .<_ s /\ s .<_ r ) /\ ( s .<_ t /\ t .<_ s ) ) -> r .<_ t ) )
43 breq1 
 |-  ( a = t -> ( a .<_ b <-> t .<_ b ) )
44 43 anbi1d 
 |-  ( a = t -> ( ( a .<_ b /\ b .<_ c ) <-> ( t .<_ b /\ b .<_ c ) ) )
45 breq1 
 |-  ( a = t -> ( a .<_ c <-> t .<_ c ) )
46 44 45 imbi12d 
 |-  ( a = t -> ( ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) <-> ( ( t .<_ b /\ b .<_ c ) -> t .<_ c ) ) )
47 46 2albidv 
 |-  ( a = t -> ( A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) <-> A. b A. c ( ( t .<_ b /\ b .<_ c ) -> t .<_ c ) ) )
48 47 spvv 
 |-  ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> A. b A. c ( ( t .<_ b /\ b .<_ c ) -> t .<_ c ) )
49 breq2 
 |-  ( b = s -> ( t .<_ b <-> t .<_ s ) )
50 49 26 anbi12d 
 |-  ( b = s -> ( ( t .<_ b /\ b .<_ c ) <-> ( t .<_ s /\ s .<_ c ) ) )
51 50 imbi1d 
 |-  ( b = s -> ( ( ( t .<_ b /\ b .<_ c ) -> t .<_ c ) <-> ( ( t .<_ s /\ s .<_ c ) -> t .<_ c ) ) )
52 51 albidv 
 |-  ( b = s -> ( A. c ( ( t .<_ b /\ b .<_ c ) -> t .<_ c ) <-> A. c ( ( t .<_ s /\ s .<_ c ) -> t .<_ c ) ) )
53 52 spvv 
 |-  ( A. b A. c ( ( t .<_ b /\ b .<_ c ) -> t .<_ c ) -> A. c ( ( t .<_ s /\ s .<_ c ) -> t .<_ c ) )
54 breq2 
 |-  ( c = r -> ( s .<_ c <-> s .<_ r ) )
55 54 anbi2d 
 |-  ( c = r -> ( ( t .<_ s /\ s .<_ c ) <-> ( t .<_ s /\ s .<_ r ) ) )
56 breq2 
 |-  ( c = r -> ( t .<_ c <-> t .<_ r ) )
57 55 56 imbi12d 
 |-  ( c = r -> ( ( ( t .<_ s /\ s .<_ c ) -> t .<_ c ) <-> ( ( t .<_ s /\ s .<_ r ) -> t .<_ r ) ) )
58 57 spvv 
 |-  ( A. c ( ( t .<_ s /\ s .<_ c ) -> t .<_ c ) -> ( ( t .<_ s /\ s .<_ r ) -> t .<_ r ) )
59 pm3.3 
 |-  ( ( ( t .<_ s /\ s .<_ r ) -> t .<_ r ) -> ( t .<_ s -> ( s .<_ r -> t .<_ r ) ) )
60 59 adantld 
 |-  ( ( ( t .<_ s /\ s .<_ r ) -> t .<_ r ) -> ( ( s .<_ t /\ t .<_ s ) -> ( s .<_ r -> t .<_ r ) ) )
61 60 com23 
 |-  ( ( ( t .<_ s /\ s .<_ r ) -> t .<_ r ) -> ( s .<_ r -> ( ( s .<_ t /\ t .<_ s ) -> t .<_ r ) ) )
62 61 adantld 
 |-  ( ( ( t .<_ s /\ s .<_ r ) -> t .<_ r ) -> ( ( r .<_ s /\ s .<_ r ) -> ( ( s .<_ t /\ t .<_ s ) -> t .<_ r ) ) )
63 62 impd 
 |-  ( ( ( t .<_ s /\ s .<_ r ) -> t .<_ r ) -> ( ( ( r .<_ s /\ s .<_ r ) /\ ( s .<_ t /\ t .<_ s ) ) -> t .<_ r ) )
64 48 53 58 63 4syl 
 |-  ( 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 
 |-  ( 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 
 |-  ( r ( .<_ i^i `' .<_ ) t <-> ( r .<_ t /\ r `' .<_ t ) )
67 8 14 brcnv 
 |-  ( r `' .<_ t <-> t .<_ r )
68 67 anbi2i 
 |-  ( ( r .<_ t /\ r `' .<_ t ) <-> ( r .<_ t /\ t .<_ r ) )
69 66 68 bitr2i 
 |-  ( ( r .<_ t /\ t .<_ r ) <-> r ( .<_ i^i `' .<_ ) t )
70 65 69 imbitrdi 
 |-  ( 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 biimtrid 
 |-  ( 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 
 |-  ( s `' .<_ r <-> r .<_ s )
73 72 bicomi 
 |-  ( r .<_ s <-> s `' .<_ r )
74 73 10 anbi12ci 
 |-  ( ( r .<_ s /\ r `' .<_ s ) <-> ( s .<_ r /\ s `' .<_ r ) )
75 brin 
 |-  ( s ( .<_ i^i `' .<_ ) r <-> ( s .<_ r /\ s `' .<_ r ) )
76 74 7 75 3bitr4i 
 |-  ( r ( .<_ i^i `' .<_ ) s <-> s ( .<_ i^i `' .<_ ) r )
77 76 biimpi 
 |-  ( r ( .<_ i^i `' .<_ ) s -> s ( .<_ i^i `' .<_ ) r )
78 71 77 jctil 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( ( .<_ 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 
 |-  ( A. a A. b A. c ( ( a .<_ b /\ b .<_ c ) -> a .<_ c ) -> ( .<_ i^i `' .<_ ) Er dom ( .<_ i^i `' .<_ ) )