Theorem trer 34788

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.)

Assertion

Ref	Expression
trer	⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ))

Distinct variable group:   𝑎,𝑏,𝑐, ≤

Proof of Theorem trer

Dummy variables 𝑟 𝑠 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss2 4189	. . . 4 ⊢ ( ≤ ∩ ◡ ≤ ) ⊆ ◡ ≤
2		relcnv 6056	. . . 4 ⊢ Rel ◡ ≤
3		relss 5737	. . . 4 ⊢ (( ≤ ∩ ◡ ≤ ) ⊆ ◡ ≤ → (Rel ◡ ≤ → Rel ( ≤ ∩ ◡ ≤ )))
4	1, 2, 3	mp2 9	. . 3 ⊢ Rel ( ≤ ∩ ◡ ≤ )
5	4	a1i 11	. 2 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → Rel ( ≤ ∩ ◡ ≤ ))
6		eqidd 2737	. 2 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → dom ( ≤ ∩ ◡ ≤ ) = dom ( ≤ ∩ ◡ ≤ ))
7		brin 5157	. . . . . . . 8 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 ↔ (𝑟 ≤ 𝑠 ∧ 𝑟◡ ≤ 𝑠))
8		vex 3449	. . . . . . . . . 10 ⊢ 𝑟 ∈ V
9		vex 3449	. . . . . . . . . 10 ⊢ 𝑠 ∈ V
10	8, 9	brcnv 5838	. . . . . . . . 9 ⊢ (𝑟◡ ≤ 𝑠 ↔ 𝑠 ≤ 𝑟)
11	10	anbi2i 623	. . . . . . . 8 ⊢ ((𝑟 ≤ 𝑠 ∧ 𝑟◡ ≤ 𝑠) ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟))
12	7, 11	bitri 274	. . . . . . 7 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟))
13		brin 5157	. . . . . . . 8 ⊢ (𝑠( ≤ ∩ ◡ ≤ )𝑡 ↔ (𝑠 ≤ 𝑡 ∧ 𝑠◡ ≤ 𝑡))
14		vex 3449	. . . . . . . . . 10 ⊢ 𝑡 ∈ V
15	9, 14	brcnv 5838	. . . . . . . . 9 ⊢ (𝑠◡ ≤ 𝑡 ↔ 𝑡 ≤ 𝑠)
16	15	anbi2i 623	. . . . . . . 8 ⊢ ((𝑠 ≤ 𝑡 ∧ 𝑠◡ ≤ 𝑡) ↔ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠))
17	13, 16	bitri 274	. . . . . . 7 ⊢ (𝑠( ≤ ∩ ◡ ≤ )𝑡 ↔ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠))
18	12, 17	anbi12i 627	. . . . . 6 ⊢ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) ↔ ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)))
19		breq1 5108	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑟 → (𝑎 ≤ 𝑏 ↔ 𝑟 ≤ 𝑏))
20	19	anbi1d 630	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑟 → ((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐)))
21		breq1 5108	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑟 → (𝑎 ≤ 𝑐 ↔ 𝑟 ≤ 𝑐))
22	20, 21	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑟 → (((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
23	22	2albidv 1926	. . . . . . . . . 10 ⊢ (𝑎 = 𝑟 → (∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ∀𝑏∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
24	23	spvv 2000	. . . . . . . . 9 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑏∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐))
25		breq2 5109	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑠 → (𝑟 ≤ 𝑏 ↔ 𝑟 ≤ 𝑠))
26		breq1 5108	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑠 → (𝑏 ≤ 𝑐 ↔ 𝑠 ≤ 𝑐))
27	25, 26	anbi12d 631	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑠 → ((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐)))
28	27	imbi1d 341	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑠 → (((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐) ↔ ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
29	28	albidv 1923	. . . . . . . . . 10 ⊢ (𝑏 = 𝑠 → (∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐) ↔ ∀𝑐((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
30	29	spvv 2000	. . . . . . . . 9 ⊢ (∀𝑏∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐) → ∀𝑐((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐))
31		breq2 5109	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑡 → (𝑠 ≤ 𝑐 ↔ 𝑠 ≤ 𝑡))
32	31	anbi2d 629	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑡 → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡)))
33		breq2 5109	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑡 → (𝑟 ≤ 𝑐 ↔ 𝑟 ≤ 𝑡))
34	32, 33	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑐 = 𝑡 → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐) ↔ ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡)))
35	34	spvv 2000	. . . . . . . . 9 ⊢ (∀𝑐((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐) → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡))
36		pm3.3 449	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (𝑟 ≤ 𝑠 → (𝑠 ≤ 𝑡 → 𝑟 ≤ 𝑡)))
37	36	com23 86	. . . . . . . . . . . . 13 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (𝑠 ≤ 𝑡 → (𝑟 ≤ 𝑠 → 𝑟 ≤ 𝑡)))
38	37	adantrd 492	. . . . . . . . . . . 12 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → (𝑟 ≤ 𝑠 → 𝑟 ≤ 𝑡)))
39	38	com23 86	. . . . . . . . . . 11 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (𝑟 ≤ 𝑠 → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑟 ≤ 𝑡)))
40	39	adantrd 492	. . . . . . . . . 10 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑟 ≤ 𝑡)))
41	40	impd 411	. . . . . . . . 9 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑟 ≤ 𝑡))
42	24, 30, 35, 41	4syl 19	. . . . . . . 8 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑟 ≤ 𝑡))
43		breq1 5108	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑡 → (𝑎 ≤ 𝑏 ↔ 𝑡 ≤ 𝑏))
44	43	anbi1d 630	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑡 → ((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐)))
45		breq1 5108	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑡 → (𝑎 ≤ 𝑐 ↔ 𝑡 ≤ 𝑐))
46	44, 45	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑡 → (((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
47	46	2albidv 1926	. . . . . . . . . 10 ⊢ (𝑎 = 𝑡 → (∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ∀𝑏∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
48	47	spvv 2000	. . . . . . . . 9 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑏∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐))
49		breq2 5109	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑠 → (𝑡 ≤ 𝑏 ↔ 𝑡 ≤ 𝑠))
50	49, 26	anbi12d 631	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑠 → ((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐)))
51	50	imbi1d 341	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑠 → (((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐) ↔ ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
52	51	albidv 1923	. . . . . . . . . 10 ⊢ (𝑏 = 𝑠 → (∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐) ↔ ∀𝑐((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
53	52	spvv 2000	. . . . . . . . 9 ⊢ (∀𝑏∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐) → ∀𝑐((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐))
54		breq2 5109	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑟 → (𝑠 ≤ 𝑐 ↔ 𝑠 ≤ 𝑟))
55	54	anbi2d 629	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑟 → ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) ↔ (𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟)))
56		breq2 5109	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑟 → (𝑡 ≤ 𝑐 ↔ 𝑡 ≤ 𝑟))
57	55, 56	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑐 = 𝑟 → (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐) ↔ ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟)))
58	57	spvv 2000	. . . . . . . . 9 ⊢ (∀𝑐((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐) → ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟))
59		pm3.3 449	. . . . . . . . . . . . 13 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → (𝑡 ≤ 𝑠 → (𝑠 ≤ 𝑟 → 𝑡 ≤ 𝑟)))
60	59	adantld 491	. . . . . . . . . . . 12 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → (𝑠 ≤ 𝑟 → 𝑡 ≤ 𝑟)))
61	60	com23 86	. . . . . . . . . . 11 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → (𝑠 ≤ 𝑟 → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑡 ≤ 𝑟)))
62	61	adantld 491	. . . . . . . . . 10 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑡 ≤ 𝑟)))
63	62	impd 411	. . . . . . . . 9 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑡 ≤ 𝑟))
64	48, 53, 58, 63	4syl 19	. . . . . . . 8 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑡 ≤ 𝑟))
65	42, 64	jcad 513	. . . . . . 7 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → (𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟)))
66		brin 5157	. . . . . . . 8 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑡 ↔ (𝑟 ≤ 𝑡 ∧ 𝑟◡ ≤ 𝑡))
67	8, 14	brcnv 5838	. . . . . . . . 9 ⊢ (𝑟◡ ≤ 𝑡 ↔ 𝑡 ≤ 𝑟)
68	67	anbi2i 623	. . . . . . . 8 ⊢ ((𝑟 ≤ 𝑡 ∧ 𝑟◡ ≤ 𝑡) ↔ (𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟))
69	66, 68	bitr2i 275	. . . . . . 7 ⊢ ((𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟) ↔ 𝑟( ≤ ∩ ◡ ≤ )𝑡)
70	65, 69	syl6ib 250	. . . . . 6 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑟( ≤ ∩ ◡ ≤ )𝑡))
71	18, 70	biimtrid 241	. . . . 5 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡))
72	9, 8	brcnv 5838	. . . . . . . . 9 ⊢ (𝑠◡ ≤ 𝑟 ↔ 𝑟 ≤ 𝑠)
73	72	bicomi 223	. . . . . . . 8 ⊢ (𝑟 ≤ 𝑠 ↔ 𝑠◡ ≤ 𝑟)
74	73, 10	anbi12ci 628	. . . . . . 7 ⊢ ((𝑟 ≤ 𝑠 ∧ 𝑟◡ ≤ 𝑠) ↔ (𝑠 ≤ 𝑟 ∧ 𝑠◡ ≤ 𝑟))
75		brin 5157	. . . . . . 7 ⊢ (𝑠( ≤ ∩ ◡ ≤ )𝑟 ↔ (𝑠 ≤ 𝑟 ∧ 𝑠◡ ≤ 𝑟))
76	74, 7, 75	3bitr4i 302	. . . . . 6 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 ↔ 𝑠( ≤ ∩ ◡ ≤ )𝑟)
77	76	biimpi 215	. . . . 5 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟)
78	71, 77	jctil 520	. . . 4 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡)))
79	78	alrimiv 1930	. . 3 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑡((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡)))
80	79	alrimivv 1931	. 2 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑟∀𝑠∀𝑡((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡)))
81		dfer2 8649	. 2 ⊢ (( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ) ↔ (Rel ( ≤ ∩ ◡ ≤ ) ∧ dom ( ≤ ∩ ◡ ≤ ) = dom ( ≤ ∩ ◡ ≤ ) ∧ ∀𝑟∀𝑠∀𝑡((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡))))
82	5, 6, 80, 81	syl3anbrc 1343	1 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ))

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1539   = wceq 1541   ∩ cin 3909   ⊆ wss 3910   class class class wbr 5105  ^◡ccnv 5632  dom cdm 5633  Rel wrel 5638   Er wer 8645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-br 5106  df-opab 5168  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-er 8648

This theorem is referenced by: (None)