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 abca˙bb˙ca˙c˙˙-1Erdom˙˙-1

Proof

Step Hyp Ref Expression
1 inss2 ˙˙-1˙-1
2 relcnv Rel˙-1
3 relss ˙˙-1˙-1Rel˙-1Rel˙˙-1
4 1 2 3 mp2 Rel˙˙-1
5 4 a1i abca˙bb˙ca˙cRel˙˙-1
6 eqidd abca˙bb˙ca˙cdom˙˙-1=dom˙˙-1
7 brin r˙˙-1sr˙sr˙-1s
8 vex rV
9 vex sV
10 8 9 brcnv r˙-1ss˙r
11 10 anbi2i r˙sr˙-1sr˙ss˙r
12 7 11 bitri r˙˙-1sr˙ss˙r
13 brin s˙˙-1ts˙ts˙-1t
14 vex tV
15 9 14 brcnv s˙-1tt˙s
16 15 anbi2i s˙ts˙-1ts˙tt˙s
17 13 16 bitri s˙˙-1ts˙tt˙s
18 12 17 anbi12i r˙˙-1ss˙˙-1tr˙ss˙rs˙tt˙s
19 breq1 a=ra˙br˙b
20 19 anbi1d a=ra˙bb˙cr˙bb˙c
21 breq1 a=ra˙cr˙c
22 20 21 imbi12d a=ra˙bb˙ca˙cr˙bb˙cr˙c
23 22 2albidv a=rbca˙bb˙ca˙cbcr˙bb˙cr˙c
24 23 spvv abca˙bb˙ca˙cbcr˙bb˙cr˙c
25 breq2 b=sr˙br˙s
26 breq1 b=sb˙cs˙c
27 25 26 anbi12d b=sr˙bb˙cr˙ss˙c
28 27 imbi1d b=sr˙bb˙cr˙cr˙ss˙cr˙c
29 28 albidv b=scr˙bb˙cr˙ccr˙ss˙cr˙c
30 29 spvv bcr˙bb˙cr˙ccr˙ss˙cr˙c
31 breq2 c=ts˙cs˙t
32 31 anbi2d c=tr˙ss˙cr˙ss˙t
33 breq2 c=tr˙cr˙t
34 32 33 imbi12d c=tr˙ss˙cr˙cr˙ss˙tr˙t
35 34 spvv cr˙ss˙cr˙cr˙ss˙tr˙t
36 pm3.3 r˙ss˙tr˙tr˙ss˙tr˙t
37 36 com23 r˙ss˙tr˙ts˙tr˙sr˙t
38 37 adantrd r˙ss˙tr˙ts˙tt˙sr˙sr˙t
39 38 com23 r˙ss˙tr˙tr˙ss˙tt˙sr˙t
40 39 adantrd r˙ss˙tr˙tr˙ss˙rs˙tt˙sr˙t
41 40 impd r˙ss˙tr˙tr˙ss˙rs˙tt˙sr˙t
42 24 30 35 41 4syl abca˙bb˙ca˙cr˙ss˙rs˙tt˙sr˙t
43 breq1 a=ta˙bt˙b
44 43 anbi1d a=ta˙bb˙ct˙bb˙c
45 breq1 a=ta˙ct˙c
46 44 45 imbi12d a=ta˙bb˙ca˙ct˙bb˙ct˙c
47 46 2albidv a=tbca˙bb˙ca˙cbct˙bb˙ct˙c
48 47 spvv abca˙bb˙ca˙cbct˙bb˙ct˙c
49 breq2 b=st˙bt˙s
50 49 26 anbi12d b=st˙bb˙ct˙ss˙c
51 50 imbi1d b=st˙bb˙ct˙ct˙ss˙ct˙c
52 51 albidv b=sct˙bb˙ct˙cct˙ss˙ct˙c
53 52 spvv bct˙bb˙ct˙cct˙ss˙ct˙c
54 breq2 c=rs˙cs˙r
55 54 anbi2d c=rt˙ss˙ct˙ss˙r
56 breq2 c=rt˙ct˙r
57 55 56 imbi12d c=rt˙ss˙ct˙ct˙ss˙rt˙r
58 57 spvv ct˙ss˙ct˙ct˙ss˙rt˙r
59 pm3.3 t˙ss˙rt˙rt˙ss˙rt˙r
60 59 adantld t˙ss˙rt˙rs˙tt˙ss˙rt˙r
61 60 com23 t˙ss˙rt˙rs˙rs˙tt˙st˙r
62 61 adantld t˙ss˙rt˙rr˙ss˙rs˙tt˙st˙r
63 62 impd t˙ss˙rt˙rr˙ss˙rs˙tt˙st˙r
64 48 53 58 63 4syl abca˙bb˙ca˙cr˙ss˙rs˙tt˙st˙r
65 42 64 jcad abca˙bb˙ca˙cr˙ss˙rs˙tt˙sr˙tt˙r
66 brin r˙˙-1tr˙tr˙-1t
67 8 14 brcnv r˙-1tt˙r
68 67 anbi2i r˙tr˙-1tr˙tt˙r
69 66 68 bitr2i r˙tt˙rr˙˙-1t
70 65 69 syl6ib abca˙bb˙ca˙cr˙ss˙rs˙tt˙sr˙˙-1t
71 18 70 syl5bi abca˙bb˙ca˙cr˙˙-1ss˙˙-1tr˙˙-1t
72 9 8 brcnv s˙-1rr˙s
73 72 bicomi r˙ss˙-1r
74 73 10 anbi12ci r˙sr˙-1ss˙rs˙-1r
75 brin s˙˙-1rs˙rs˙-1r
76 74 7 75 3bitr4i r˙˙-1ss˙˙-1r
77 76 biimpi r˙˙-1ss˙˙-1r
78 71 77 jctil abca˙bb˙ca˙cr˙˙-1ss˙˙-1rr˙˙-1ss˙˙-1tr˙˙-1t
79 78 alrimiv abca˙bb˙ca˙ctr˙˙-1ss˙˙-1rr˙˙-1ss˙˙-1tr˙˙-1t
80 79 alrimivv abca˙bb˙ca˙crstr˙˙-1ss˙˙-1rr˙˙-1ss˙˙-1tr˙˙-1t
81 dfer2 ˙˙-1Erdom˙˙-1Rel˙˙-1dom˙˙-1=dom˙˙-1rstr˙˙-1ss˙˙-1rr˙˙-1ss˙˙-1tr˙˙-1t
82 5 6 80 81 syl3anbrc abca˙bb˙ca˙c˙˙-1Erdom˙˙-1