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	⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) → ( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ) )

Proof

Step	Hyp	Ref	Expression
1		inss2	⊢ ( ≤ ∩ ◡ ≤ ) ⊆ ◡ ≤
2		relcnv	⊢ Rel ◡ ≤
3		relss	⊢ ( ( ≤ ∩ ◡ ≤ ) ⊆ ◡ ≤ → ( Rel ◡ ≤ → Rel ( ≤ ∩ ◡ ≤ ) ) )
4	1 2 3	mp2	⊢ Rel ( ≤ ∩ ◡ ≤ )
5	4	a1i	⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) → Rel ( ≤ ∩ ◡ ≤ ) )
6		eqidd	⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) → dom ( ≤ ∩ ◡ ≤ ) = dom ( ≤ ∩ ◡ ≤ ) )
7		brin	⊢ ( 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑠 ↔ ( 𝑟 ≤ 𝑠 ∧ 𝑟 ◡ ≤ 𝑠 ) )
8		vex	⊢ 𝑟 ∈ V
9		vex	⊢ 𝑠 ∈ V
10	8 9	brcnv	⊢ ( 𝑟 ◡ ≤ 𝑠 ↔ 𝑠 ≤ 𝑟 )
11	10	anbi2i	⊢ ( ( 𝑟 ≤ 𝑠 ∧ 𝑟 ◡ ≤ 𝑠 ) ↔ ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) )
12	7 11	bitri	⊢ ( 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑠 ↔ ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) )
13		brin	⊢ ( 𝑠 ( ≤ ∩ ◡ ≤ ) 𝑡 ↔ ( 𝑠 ≤ 𝑡 ∧ 𝑠 ◡ ≤ 𝑡 ) )
14		vex	⊢ 𝑡 ∈ V
15	9 14	brcnv	⊢ ( 𝑠 ◡ ≤ 𝑡 ↔ 𝑡 ≤ 𝑠 )
16	15	anbi2i	⊢ ( ( 𝑠 ≤ 𝑡 ∧ 𝑠 ◡ ≤ 𝑡 ) ↔ ( 𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠 ) )
17	13 16	bitri	⊢ ( 𝑠 ( ≤ ∩ ◡ ≤ ) 𝑡 ↔ ( 𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠 ) )
18	12 17	anbi12i	⊢ ( ( 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑠 ∧ 𝑠 ( ≤ ∩ ◡ ≤ ) 𝑡 ) ↔ ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) ∧ ( 𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠 ) ) )
19		breq1	⊢ ( 𝑎 = 𝑟 → ( 𝑎 ≤ 𝑏 ↔ 𝑟 ≤ 𝑏 ) )
20	19	anbi1d	⊢ ( 𝑎 = 𝑟 → ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) ↔ ( 𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) ) )
21		breq1	⊢ ( 𝑎 = 𝑟 → ( 𝑎 ≤ 𝑐 ↔ 𝑟 ≤ 𝑐 ) )
22	20 21	imbi12d	⊢ ( 𝑎 = 𝑟 → ( ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) ↔ ( ( 𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑟 ≤ 𝑐 ) ) )
23	22	2albidv	⊢ ( 𝑎 = 𝑟 → ( ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) ↔ ∀ 𝑏 ∀ 𝑐 ( ( 𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑟 ≤ 𝑐 ) ) )
24	23	spvv	⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) → ∀ 𝑏 ∀ 𝑐 ( ( 𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑟 ≤ 𝑐 ) )
25		breq2	⊢ ( 𝑏 = 𝑠 → ( 𝑟 ≤ 𝑏 ↔ 𝑟 ≤ 𝑠 ) )
26		breq1	⊢ ( 𝑏 = 𝑠 → ( 𝑏 ≤ 𝑐 ↔ 𝑠 ≤ 𝑐 ) )
27	25 26	anbi12d	⊢ ( 𝑏 = 𝑠 → ( ( 𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) ↔ ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐 ) ) )
28	27	imbi1d	⊢ ( 𝑏 = 𝑠 → ( ( ( 𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑟 ≤ 𝑐 ) ↔ ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐 ) → 𝑟 ≤ 𝑐 ) ) )
29	28	albidv	⊢ ( 𝑏 = 𝑠 → ( ∀ 𝑐 ( ( 𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑟 ≤ 𝑐 ) ↔ ∀ 𝑐 ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐 ) → 𝑟 ≤ 𝑐 ) ) )
30	29	spvv	⊢ ( ∀ 𝑏 ∀ 𝑐 ( ( 𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑟 ≤ 𝑐 ) → ∀ 𝑐 ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐 ) → 𝑟 ≤ 𝑐 ) )
31		breq2	⊢ ( 𝑐 = 𝑡 → ( 𝑠 ≤ 𝑐 ↔ 𝑠 ≤ 𝑡 ) )
32	31	anbi2d	⊢ ( 𝑐 = 𝑡 → ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐 ) ↔ ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡 ) ) )
33		breq2	⊢ ( 𝑐 = 𝑡 → ( 𝑟 ≤ 𝑐 ↔ 𝑟 ≤ 𝑡 ) )
34	32 33	imbi12d	⊢ ( 𝑐 = 𝑡 → ( ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐 ) → 𝑟 ≤ 𝑐 ) ↔ ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡 ) → 𝑟 ≤ 𝑡 ) ) )
35	34	spvv	⊢ ( ∀ 𝑐 ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐 ) → 𝑟 ≤ 𝑐 ) → ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡 ) → 𝑟 ≤ 𝑡 ) )
36		pm3.3	⊢ ( ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡 ) → 𝑟 ≤ 𝑡 ) → ( 𝑟 ≤ 𝑠 → ( 𝑠 ≤ 𝑡 → 𝑟 ≤ 𝑡 ) ) )
37	36	com23	⊢ ( ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡 ) → 𝑟 ≤ 𝑡 ) → ( 𝑠 ≤ 𝑡 → ( 𝑟 ≤ 𝑠 → 𝑟 ≤ 𝑡 ) ) )
38	37	adantrd	⊢ ( ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡 ) → 𝑟 ≤ 𝑡 ) → ( ( 𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠 ) → ( 𝑟 ≤ 𝑠 → 𝑟 ≤ 𝑡 ) ) )
39	38	com23	⊢ ( ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡 ) → 𝑟 ≤ 𝑡 ) → ( 𝑟 ≤ 𝑠 → ( ( 𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠 ) → 𝑟 ≤ 𝑡 ) ) )
40	39	adantrd	⊢ ( ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡 ) → 𝑟 ≤ 𝑡 ) → ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) → ( ( 𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠 ) → 𝑟 ≤ 𝑡 ) ) )
41	40	impd	⊢ ( ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡 ) → 𝑟 ≤ 𝑡 ) → ( ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) ∧ ( 𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠 ) ) → 𝑟 ≤ 𝑡 ) )
42	24 30 35 41	4syl	⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) → ( ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) ∧ ( 𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠 ) ) → 𝑟 ≤ 𝑡 ) )
43		breq1	⊢ ( 𝑎 = 𝑡 → ( 𝑎 ≤ 𝑏 ↔ 𝑡 ≤ 𝑏 ) )
44	43	anbi1d	⊢ ( 𝑎 = 𝑡 → ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) ↔ ( 𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) ) )
45		breq1	⊢ ( 𝑎 = 𝑡 → ( 𝑎 ≤ 𝑐 ↔ 𝑡 ≤ 𝑐 ) )
46	44 45	imbi12d	⊢ ( 𝑎 = 𝑡 → ( ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) ↔ ( ( 𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑡 ≤ 𝑐 ) ) )
47	46	2albidv	⊢ ( 𝑎 = 𝑡 → ( ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) ↔ ∀ 𝑏 ∀ 𝑐 ( ( 𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑡 ≤ 𝑐 ) ) )
48	47	spvv	⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) → ∀ 𝑏 ∀ 𝑐 ( ( 𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑡 ≤ 𝑐 ) )
49		breq2	⊢ ( 𝑏 = 𝑠 → ( 𝑡 ≤ 𝑏 ↔ 𝑡 ≤ 𝑠 ) )
50	49 26	anbi12d	⊢ ( 𝑏 = 𝑠 → ( ( 𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) ↔ ( 𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐 ) ) )
51	50	imbi1d	⊢ ( 𝑏 = 𝑠 → ( ( ( 𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑡 ≤ 𝑐 ) ↔ ( ( 𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐 ) → 𝑡 ≤ 𝑐 ) ) )
52	51	albidv	⊢ ( 𝑏 = 𝑠 → ( ∀ 𝑐 ( ( 𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑡 ≤ 𝑐 ) ↔ ∀ 𝑐 ( ( 𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐 ) → 𝑡 ≤ 𝑐 ) ) )
53	52	spvv	⊢ ( ∀ 𝑏 ∀ 𝑐 ( ( 𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑡 ≤ 𝑐 ) → ∀ 𝑐 ( ( 𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐 ) → 𝑡 ≤ 𝑐 ) )
54		breq2	⊢ ( 𝑐 = 𝑟 → ( 𝑠 ≤ 𝑐 ↔ 𝑠 ≤ 𝑟 ) )
55	54	anbi2d	⊢ ( 𝑐 = 𝑟 → ( ( 𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐 ) ↔ ( 𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) ) )
56		breq2	⊢ ( 𝑐 = 𝑟 → ( 𝑡 ≤ 𝑐 ↔ 𝑡 ≤ 𝑟 ) )
57	55 56	imbi12d	⊢ ( 𝑐 = 𝑟 → ( ( ( 𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐 ) → 𝑡 ≤ 𝑐 ) ↔ ( ( 𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) → 𝑡 ≤ 𝑟 ) ) )
58	57	spvv	⊢ ( ∀ 𝑐 ( ( 𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐 ) → 𝑡 ≤ 𝑐 ) → ( ( 𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) → 𝑡 ≤ 𝑟 ) )
59		pm3.3	⊢ ( ( ( 𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) → 𝑡 ≤ 𝑟 ) → ( 𝑡 ≤ 𝑠 → ( 𝑠 ≤ 𝑟 → 𝑡 ≤ 𝑟 ) ) )
60	59	adantld	⊢ ( ( ( 𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) → 𝑡 ≤ 𝑟 ) → ( ( 𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠 ) → ( 𝑠 ≤ 𝑟 → 𝑡 ≤ 𝑟 ) ) )
61	60	com23	⊢ ( ( ( 𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) → 𝑡 ≤ 𝑟 ) → ( 𝑠 ≤ 𝑟 → ( ( 𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠 ) → 𝑡 ≤ 𝑟 ) ) )
62	61	adantld	⊢ ( ( ( 𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) → 𝑡 ≤ 𝑟 ) → ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) → ( ( 𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠 ) → 𝑡 ≤ 𝑟 ) ) )
63	62	impd	⊢ ( ( ( 𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) → 𝑡 ≤ 𝑟 ) → ( ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) ∧ ( 𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠 ) ) → 𝑡 ≤ 𝑟 ) )
64	48 53 58 63	4syl	⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) → ( ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) ∧ ( 𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠 ) ) → 𝑡 ≤ 𝑟 ) )
65	42 64	jcad	⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) → ( ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) ∧ ( 𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠 ) ) → ( 𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟 ) ) )
66		brin	⊢ ( 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑡 ↔ ( 𝑟 ≤ 𝑡 ∧ 𝑟 ◡ ≤ 𝑡 ) )
67	8 14	brcnv	⊢ ( 𝑟 ◡ ≤ 𝑡 ↔ 𝑡 ≤ 𝑟 )
68	67	anbi2i	⊢ ( ( 𝑟 ≤ 𝑡 ∧ 𝑟 ◡ ≤ 𝑡 ) ↔ ( 𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟 ) )
69	66 68	bitr2i	⊢ ( ( 𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟 ) ↔ 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑡 )
70	65 69	imbitrdi	⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) → ( ( ( 𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟 ) ∧ ( 𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠 ) ) → 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑡 ) )
71	18 70	biimtrid	⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) → ( ( 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑠 ∧ 𝑠 ( ≤ ∩ ◡ ≤ ) 𝑡 ) → 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑡 ) )
72	9 8	brcnv	⊢ ( 𝑠 ◡ ≤ 𝑟 ↔ 𝑟 ≤ 𝑠 )
73	72	bicomi	⊢ ( 𝑟 ≤ 𝑠 ↔ 𝑠 ◡ ≤ 𝑟 )
74	73 10	anbi12ci	⊢ ( ( 𝑟 ≤ 𝑠 ∧ 𝑟 ◡ ≤ 𝑠 ) ↔ ( 𝑠 ≤ 𝑟 ∧ 𝑠 ◡ ≤ 𝑟 ) )
75		brin	⊢ ( 𝑠 ( ≤ ∩ ◡ ≤ ) 𝑟 ↔ ( 𝑠 ≤ 𝑟 ∧ 𝑠 ◡ ≤ 𝑟 ) )
76	74 7 75	3bitr4i	⊢ ( 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑠 ↔ 𝑠 ( ≤ ∩ ◡ ≤ ) 𝑟 )
77	76	biimpi	⊢ ( 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑠 → 𝑠 ( ≤ ∩ ◡ ≤ ) 𝑟 )
78	71 77	jctil	⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) → ( ( 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑠 → 𝑠 ( ≤ ∩ ◡ ≤ ) 𝑟 ) ∧ ( ( 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑠 ∧ 𝑠 ( ≤ ∩ ◡ ≤ ) 𝑡 ) → 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑡 ) ) )
79	78	alrimiv	⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) → ∀ 𝑡 ( ( 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑠 → 𝑠 ( ≤ ∩ ◡ ≤ ) 𝑟 ) ∧ ( ( 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑠 ∧ 𝑠 ( ≤ ∩ ◡ ≤ ) 𝑡 ) → 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑡 ) ) )
80	79	alrimivv	⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) → ∀ 𝑟 ∀ 𝑠 ∀ 𝑡 ( ( 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑠 → 𝑠 ( ≤ ∩ ◡ ≤ ) 𝑟 ) ∧ ( ( 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑠 ∧ 𝑠 ( ≤ ∩ ◡ ≤ ) 𝑡 ) → 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑡 ) ) )
81		dfer2	⊢ ( ( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ) ↔ ( Rel ( ≤ ∩ ◡ ≤ ) ∧ dom ( ≤ ∩ ◡ ≤ ) = dom ( ≤ ∩ ◡ ≤ ) ∧ ∀ 𝑟 ∀ 𝑠 ∀ 𝑡 ( ( 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑠 → 𝑠 ( ≤ ∩ ◡ ≤ ) 𝑟 ) ∧ ( ( 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑠 ∧ 𝑠 ( ≤ ∩ ◡ ≤ ) 𝑡 ) → 𝑟 ( ≤ ∩ ◡ ≤ ) 𝑡 ) ) ) )
82	5 6 80 81	syl3anbrc	⊢ ( ∀ 𝑎 ∀ 𝑏 ∀ 𝑐 ( ( 𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐 ) → 𝑎 ≤ 𝑐 ) → ( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ) )