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	$$⊢\forall a\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\to \left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)\mathrm{Er}\mathrm{dom}\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		inss2	$$⊢\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\subseteq {\underset{\dot{}}{\le }}^{-1}$$
2		relcnv	$$⊢\mathrm{Rel}{\underset{\dot{}}{\le }}^{-1}$$
3		relss	$$⊢\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\subseteq {\underset{\dot{}}{\le }}^{-1}\to \left(\mathrm{Rel}{\underset{\dot{}}{\le }}^{-1}\to \mathrm{Rel}\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)\right)$$
4	1 2 3	mp2	$$⊢\mathrm{Rel}\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)$$
5	4	a1i	$$⊢\forall a\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\to \mathrm{Rel}\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)$$
6		eqidd	$$⊢\forall a\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\to \mathrm{dom}\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)=\mathrm{dom}\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)$$
7		brin	$$⊢r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)s\leftrightarrow \left(r\underset{\dot{}}{\le }s\wedge r{\underset{\dot{}}{\le }}^{-1}s\right)$$
8		vex	$$⊢r\in \mathrm{V}$$
9		vex	$$⊢s\in \mathrm{V}$$
10	8 9	brcnv	$$⊢r{\underset{\dot{}}{\le }}^{-1}s\leftrightarrow s\underset{\dot{}}{\le }r$$
11	10	anbi2i	$$⊢\left(r\underset{\dot{}}{\le }s\wedge r{\underset{\dot{}}{\le }}^{-1}s\right)\leftrightarrow \left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)$$
12	7 11	bitri	$$⊢r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)s\leftrightarrow \left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)$$
13		brin	$$⊢s\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t\leftrightarrow \left(s\underset{\dot{}}{\le }t\wedge s{\underset{\dot{}}{\le }}^{-1}t\right)$$
14		vex	$$⊢t\in \mathrm{V}$$
15	9 14	brcnv	$$⊢s{\underset{\dot{}}{\le }}^{-1}t\leftrightarrow t\underset{\dot{}}{\le }s$$
16	15	anbi2i	$$⊢\left(s\underset{\dot{}}{\le }t\wedge s{\underset{\dot{}}{\le }}^{-1}t\right)\leftrightarrow \left(s\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }s\right)$$
17	13 16	bitri	$$⊢s\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t\leftrightarrow \left(s\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }s\right)$$
18	12 17	anbi12i	$$⊢\left(r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)s\wedge s\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t\right)\leftrightarrow \left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\wedge \left(s\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }s\right)\right)$$
19		breq1	$$⊢a=r\to \left(a\underset{\dot{}}{\le }b\leftrightarrow r\underset{\dot{}}{\le }b\right)$$
20	19	anbi1d	$$⊢a=r\to \left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\leftrightarrow \left(r\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\right)$$
21		breq1	$$⊢a=r\to \left(a\underset{\dot{}}{\le }c\leftrightarrow r\underset{\dot{}}{\le }c\right)$$
22	20 21	imbi12d	$$⊢a=r\to \left(\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\leftrightarrow \left(\left(r\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to r\underset{\dot{}}{\le }c\right)\right)$$
23	22	2albidv	$$⊢a=r\to \left(\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\leftrightarrow \forall b\forall c\left(\left(r\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to r\underset{\dot{}}{\le }c\right)\right)$$
24	23	spvv	$$⊢\forall a\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\to \forall b\forall c\left(\left(r\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to r\underset{\dot{}}{\le }c\right)$$
25		breq2	$$⊢b=s\to \left(r\underset{\dot{}}{\le }b\leftrightarrow r\underset{\dot{}}{\le }s\right)$$
26		breq1	$$⊢b=s\to \left(b\underset{\dot{}}{\le }c\leftrightarrow s\underset{\dot{}}{\le }c\right)$$
27	25 26	anbi12d	$$⊢b=s\to \left(\left(r\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\leftrightarrow \left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }c\right)\right)$$
28	27	imbi1d	$$⊢b=s\to \left(\left(\left(r\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to r\underset{\dot{}}{\le }c\right)\leftrightarrow \left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }c\right)\to r\underset{\dot{}}{\le }c\right)\right)$$
29	28	albidv	$$⊢b=s\to \left(\forall c\left(\left(r\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to r\underset{\dot{}}{\le }c\right)\leftrightarrow \forall c\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }c\right)\to r\underset{\dot{}}{\le }c\right)\right)$$
30	29	spvv	$$⊢\forall b\forall c\left(\left(r\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to r\underset{\dot{}}{\le }c\right)\to \forall c\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }c\right)\to r\underset{\dot{}}{\le }c\right)$$
31		breq2	$$⊢c=t\to \left(s\underset{\dot{}}{\le }c\leftrightarrow s\underset{\dot{}}{\le }t\right)$$
32	31	anbi2d	$$⊢c=t\to \left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }c\right)\leftrightarrow \left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }t\right)\right)$$
33		breq2	$$⊢c=t\to \left(r\underset{\dot{}}{\le }c\leftrightarrow r\underset{\dot{}}{\le }t\right)$$
34	32 33	imbi12d	$$⊢c=t\to \left(\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }c\right)\to r\underset{\dot{}}{\le }c\right)\leftrightarrow \left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }t\right)\to r\underset{\dot{}}{\le }t\right)\right)$$
35	34	spvv	$$⊢\forall c\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }c\right)\to r\underset{\dot{}}{\le }c\right)\to \left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }t\right)\to r\underset{\dot{}}{\le }t\right)$$
36		pm3.3	$$⊢\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }t\right)\to r\underset{\dot{}}{\le }t\right)\to \left(r\underset{\dot{}}{\le }s\to \left(s\underset{\dot{}}{\le }t\to r\underset{\dot{}}{\le }t\right)\right)$$
37	36	com23	$$⊢\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }t\right)\to r\underset{\dot{}}{\le }t\right)\to \left(s\underset{\dot{}}{\le }t\to \left(r\underset{\dot{}}{\le }s\to r\underset{\dot{}}{\le }t\right)\right)$$
38	37	adantrd	$$⊢\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }t\right)\to r\underset{\dot{}}{\le }t\right)\to \left(\left(s\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }s\right)\to \left(r\underset{\dot{}}{\le }s\to r\underset{\dot{}}{\le }t\right)\right)$$
39	38	com23	$$⊢\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }t\right)\to r\underset{\dot{}}{\le }t\right)\to \left(r\underset{\dot{}}{\le }s\to \left(\left(s\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }s\right)\to r\underset{\dot{}}{\le }t\right)\right)$$
40	39	adantrd	$$⊢\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }t\right)\to r\underset{\dot{}}{\le }t\right)\to \left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\to \left(\left(s\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }s\right)\to r\underset{\dot{}}{\le }t\right)\right)$$
41	40	impd	$$⊢\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }t\right)\to r\underset{\dot{}}{\le }t\right)\to \left(\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\wedge \left(s\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }s\right)\right)\to r\underset{\dot{}}{\le }t\right)$$
42	24 30 35 41	4syl	$$⊢\forall a\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\to \left(\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\wedge \left(s\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }s\right)\right)\to r\underset{\dot{}}{\le }t\right)$$
43		breq1	$$⊢a=t\to \left(a\underset{\dot{}}{\le }b\leftrightarrow t\underset{\dot{}}{\le }b\right)$$
44	43	anbi1d	$$⊢a=t\to \left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\leftrightarrow \left(t\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\right)$$
45		breq1	$$⊢a=t\to \left(a\underset{\dot{}}{\le }c\leftrightarrow t\underset{\dot{}}{\le }c\right)$$
46	44 45	imbi12d	$$⊢a=t\to \left(\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\leftrightarrow \left(\left(t\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to t\underset{\dot{}}{\le }c\right)\right)$$
47	46	2albidv	$$⊢a=t\to \left(\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\leftrightarrow \forall b\forall c\left(\left(t\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to t\underset{\dot{}}{\le }c\right)\right)$$
48	47	spvv	$$⊢\forall a\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\to \forall b\forall c\left(\left(t\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to t\underset{\dot{}}{\le }c\right)$$
49		breq2	$$⊢b=s\to \left(t\underset{\dot{}}{\le }b\leftrightarrow t\underset{\dot{}}{\le }s\right)$$
50	49 26	anbi12d	$$⊢b=s\to \left(\left(t\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\leftrightarrow \left(t\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }c\right)\right)$$
51	50	imbi1d	$$⊢b=s\to \left(\left(\left(t\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to t\underset{\dot{}}{\le }c\right)\leftrightarrow \left(\left(t\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }c\right)\to t\underset{\dot{}}{\le }c\right)\right)$$
52	51	albidv	$$⊢b=s\to \left(\forall c\left(\left(t\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to t\underset{\dot{}}{\le }c\right)\leftrightarrow \forall c\left(\left(t\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }c\right)\to t\underset{\dot{}}{\le }c\right)\right)$$
53	52	spvv	$$⊢\forall b\forall c\left(\left(t\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to t\underset{\dot{}}{\le }c\right)\to \forall c\left(\left(t\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }c\right)\to t\underset{\dot{}}{\le }c\right)$$
54		breq2	$$⊢c=r\to \left(s\underset{\dot{}}{\le }c\leftrightarrow s\underset{\dot{}}{\le }r\right)$$
55	54	anbi2d	$$⊢c=r\to \left(\left(t\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }c\right)\leftrightarrow \left(t\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\right)$$
56		breq2	$$⊢c=r\to \left(t\underset{\dot{}}{\le }c\leftrightarrow t\underset{\dot{}}{\le }r\right)$$
57	55 56	imbi12d	$$⊢c=r\to \left(\left(\left(t\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }c\right)\to t\underset{\dot{}}{\le }c\right)\leftrightarrow \left(\left(t\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\to t\underset{\dot{}}{\le }r\right)\right)$$
58	57	spvv	$$⊢\forall c\left(\left(t\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }c\right)\to t\underset{\dot{}}{\le }c\right)\to \left(\left(t\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\to t\underset{\dot{}}{\le }r\right)$$
59		pm3.3	$$⊢\left(\left(t\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\to t\underset{\dot{}}{\le }r\right)\to \left(t\underset{\dot{}}{\le }s\to \left(s\underset{\dot{}}{\le }r\to t\underset{\dot{}}{\le }r\right)\right)$$
60	59	adantld	$$⊢\left(\left(t\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\to t\underset{\dot{}}{\le }r\right)\to \left(\left(s\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }s\right)\to \left(s\underset{\dot{}}{\le }r\to t\underset{\dot{}}{\le }r\right)\right)$$
61	60	com23	$$⊢\left(\left(t\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\to t\underset{\dot{}}{\le }r\right)\to \left(s\underset{\dot{}}{\le }r\to \left(\left(s\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }s\right)\to t\underset{\dot{}}{\le }r\right)\right)$$
62	61	adantld	$$⊢\left(\left(t\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\to t\underset{\dot{}}{\le }r\right)\to \left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\to \left(\left(s\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }s\right)\to t\underset{\dot{}}{\le }r\right)\right)$$
63	62	impd	$$⊢\left(\left(t\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\to t\underset{\dot{}}{\le }r\right)\to \left(\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\wedge \left(s\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }s\right)\right)\to t\underset{\dot{}}{\le }r\right)$$
64	48 53 58 63	4syl	$$⊢\forall a\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\to \left(\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\wedge \left(s\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }s\right)\right)\to t\underset{\dot{}}{\le }r\right)$$
65	42 64	jcad	$$⊢\forall a\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\to \left(\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\wedge \left(s\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }s\right)\right)\to \left(r\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }r\right)\right)$$
66		brin	$$⊢r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t\leftrightarrow \left(r\underset{\dot{}}{\le }t\wedge r{\underset{\dot{}}{\le }}^{-1}t\right)$$
67	8 14	brcnv	$$⊢r{\underset{\dot{}}{\le }}^{-1}t\leftrightarrow t\underset{\dot{}}{\le }r$$
68	67	anbi2i	$$⊢\left(r\underset{\dot{}}{\le }t\wedge r{\underset{\dot{}}{\le }}^{-1}t\right)\leftrightarrow \left(r\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }r\right)$$
69	66 68	bitr2i	$$⊢\left(r\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }r\right)\leftrightarrow r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t$$
70	65 69	syl6ib	$$⊢\forall a\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\to \left(\left(\left(r\underset{\dot{}}{\le }s\wedge s\underset{\dot{}}{\le }r\right)\wedge \left(s\underset{\dot{}}{\le }t\wedge t\underset{\dot{}}{\le }s\right)\right)\to r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t\right)$$
71	18 70	syl5bi	$$⊢\forall a\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\to \left(\left(r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)s\wedge s\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t\right)\to r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t\right)$$
72	9 8	brcnv	$$⊢s{\underset{\dot{}}{\le }}^{-1}r\leftrightarrow r\underset{\dot{}}{\le }s$$
73	72	bicomi	$$⊢r\underset{\dot{}}{\le }s\leftrightarrow s{\underset{\dot{}}{\le }}^{-1}r$$
74	73 10	anbi12ci	$$⊢\left(r\underset{\dot{}}{\le }s\wedge r{\underset{\dot{}}{\le }}^{-1}s\right)\leftrightarrow \left(s\underset{\dot{}}{\le }r\wedge s{\underset{\dot{}}{\le }}^{-1}r\right)$$
75		brin	$$⊢s\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)r\leftrightarrow \left(s\underset{\dot{}}{\le }r\wedge s{\underset{\dot{}}{\le }}^{-1}r\right)$$
76	74 7 75	3bitr4i	$$⊢r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)s\leftrightarrow s\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)r$$
77	76	biimpi	$$⊢r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)s\to s\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)r$$
78	71 77	jctil	$$⊢\forall a\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\to \left(\left(r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)s\to s\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)r\right)\wedge \left(\left(r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)s\wedge s\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t\right)\to r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t\right)\right)$$
79	78	alrimiv	$$⊢\forall a\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\to \forall t\left(\left(r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)s\to s\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)r\right)\wedge \left(\left(r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)s\wedge s\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t\right)\to r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t\right)\right)$$
80	79	alrimivv	$$⊢\forall a\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\to \forall r\forall s\forall t\left(\left(r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)s\to s\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)r\right)\wedge \left(\left(r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)s\wedge s\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t\right)\to r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t\right)\right)$$
81		dfer2	$$⊢\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)\mathrm{Er}\mathrm{dom}\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)\leftrightarrow \left(\mathrm{Rel}\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)\wedge \mathrm{dom}\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)=\mathrm{dom}\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)\wedge \forall r\forall s\forall t\left(\left(r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)s\to s\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)r\right)\wedge \left(\left(r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)s\wedge s\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t\right)\to r\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)t\right)\right)\right)$$
82	5 6 80 81	syl3anbrc	$$⊢\forall a\forall b\forall c\left(\left(a\underset{\dot{}}{\le }b\wedge b\underset{\dot{}}{\le }c\right)\to a\underset{\dot{}}{\le }c\right)\to \left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)\mathrm{Er}\mathrm{dom}\left(\underset{\dot{}}{\le }\cap {\underset{\dot{}}{\le }}^{-1}\right)$$