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 syl6ib
 |-  ( 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
 |-  ( 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 `' .<_ ) )