Theorem trer 36317

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 4238	. . . 4 ⊢ ( ≤ ∩ ◡ ≤ ) ⊆ ◡ ≤
2		relcnv 6122	. . . 4 ⊢ Rel ◡ ≤
3		relss 5791	. . . 4 ⊢ (( ≤ ∩ ◡ ≤ ) ⊆ ◡ ≤ → (Rel ◡ ≤ → Rel ( ≤ ∩ ◡ ≤ )))
4	1, 2, 3	mp2 9	. . 3 ⊢ Rel ( ≤ ∩ ◡ ≤ )
5	4	a1i 11	. 2 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → Rel ( ≤ ∩ ◡ ≤ ))
6		eqidd 2738	. 2 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → dom ( ≤ ∩ ◡ ≤ ) = dom ( ≤ ∩ ◡ ≤ ))
7		brin 5195	. . . . . . . 8 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 ↔ (𝑟 ≤ 𝑠 ∧ 𝑟◡ ≤ 𝑠))
8		vex 3484	. . . . . . . . . 10 ⊢ 𝑟 ∈ V
9		vex 3484	. . . . . . . . . 10 ⊢ 𝑠 ∈ V
10	8, 9	brcnv 5893	. . . . . . . . 9 ⊢ (𝑟◡ ≤ 𝑠 ↔ 𝑠 ≤ 𝑟)
11	10	anbi2i 623	. . . . . . . 8 ⊢ ((𝑟 ≤ 𝑠 ∧ 𝑟◡ ≤ 𝑠) ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟))
12	7, 11	bitri 275	. . . . . . 7 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟))
13		brin 5195	. . . . . . . 8 ⊢ (𝑠( ≤ ∩ ◡ ≤ )𝑡 ↔ (𝑠 ≤ 𝑡 ∧ 𝑠◡ ≤ 𝑡))
14		vex 3484	. . . . . . . . . 10 ⊢ 𝑡 ∈ V
15	9, 14	brcnv 5893	. . . . . . . . 9 ⊢ (𝑠◡ ≤ 𝑡 ↔ 𝑡 ≤ 𝑠)
16	15	anbi2i 623	. . . . . . . 8 ⊢ ((𝑠 ≤ 𝑡 ∧ 𝑠◡ ≤ 𝑡) ↔ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠))
17	13, 16	bitri 275	. . . . . . 7 ⊢ (𝑠( ≤ ∩ ◡ ≤ )𝑡 ↔ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠))
18	12, 17	anbi12i 628	. . . . . 6 ⊢ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) ↔ ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)))
19		breq1 5146	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑟 → (𝑎 ≤ 𝑏 ↔ 𝑟 ≤ 𝑏))
20	19	anbi1d 631	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑟 → ((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐)))
21		breq1 5146	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑟 → (𝑎 ≤ 𝑐 ↔ 𝑟 ≤ 𝑐))
22	20, 21	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑟 → (((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
23	22	2albidv 1923	. . . . . . . . . 10 ⊢ (𝑎 = 𝑟 → (∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ∀𝑏∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
24	23	spvv 1996	. . . . . . . . 9 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑏∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐))
25		breq2 5147	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑠 → (𝑟 ≤ 𝑏 ↔ 𝑟 ≤ 𝑠))
26		breq1 5146	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑠 → (𝑏 ≤ 𝑐 ↔ 𝑠 ≤ 𝑐))
27	25, 26	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑠 → ((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐)))
28	27	imbi1d 341	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑠 → (((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐) ↔ ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
29	28	albidv 1920	. . . . . . . . . 10 ⊢ (𝑏 = 𝑠 → (∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐) ↔ ∀𝑐((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
30	29	spvv 1996	. . . . . . . . 9 ⊢ (∀𝑏∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐) → ∀𝑐((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐))
31		breq2 5147	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑡 → (𝑠 ≤ 𝑐 ↔ 𝑠 ≤ 𝑡))
32	31	anbi2d 630	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑡 → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡)))
33		breq2 5147	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑡 → (𝑟 ≤ 𝑐 ↔ 𝑟 ≤ 𝑡))
34	32, 33	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑐 = 𝑡 → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐) ↔ ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡)))
35	34	spvv 1996	. . . . . . . . 9 ⊢ (∀𝑐((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐) → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡))
36		pm3.3 448	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (𝑟 ≤ 𝑠 → (𝑠 ≤ 𝑡 → 𝑟 ≤ 𝑡)))
37	36	com23 86	. . . . . . . . . . . . 13 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (𝑠 ≤ 𝑡 → (𝑟 ≤ 𝑠 → 𝑟 ≤ 𝑡)))
38	37	adantrd 491	. . . . . . . . . . . 12 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → (𝑟 ≤ 𝑠 → 𝑟 ≤ 𝑡)))
39	38	com23 86	. . . . . . . . . . 11 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (𝑟 ≤ 𝑠 → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑟 ≤ 𝑡)))
40	39	adantrd 491	. . . . . . . . . 10 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑟 ≤ 𝑡)))
41	40	impd 410	. . . . . . . . 9 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑟 ≤ 𝑡))
42	24, 30, 35, 41	4syl 19	. . . . . . . 8 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑟 ≤ 𝑡))
43		breq1 5146	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑡 → (𝑎 ≤ 𝑏 ↔ 𝑡 ≤ 𝑏))
44	43	anbi1d 631	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑡 → ((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐)))
45		breq1 5146	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑡 → (𝑎 ≤ 𝑐 ↔ 𝑡 ≤ 𝑐))
46	44, 45	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑡 → (((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
47	46	2albidv 1923	. . . . . . . . . 10 ⊢ (𝑎 = 𝑡 → (∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ∀𝑏∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
48	47	spvv 1996	. . . . . . . . 9 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑏∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐))
49		breq2 5147	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑠 → (𝑡 ≤ 𝑏 ↔ 𝑡 ≤ 𝑠))
50	49, 26	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑠 → ((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐)))
51	50	imbi1d 341	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑠 → (((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐) ↔ ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
52	51	albidv 1920	. . . . . . . . . 10 ⊢ (𝑏 = 𝑠 → (∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐) ↔ ∀𝑐((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
53	52	spvv 1996	. . . . . . . . 9 ⊢ (∀𝑏∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐) → ∀𝑐((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐))
54		breq2 5147	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑟 → (𝑠 ≤ 𝑐 ↔ 𝑠 ≤ 𝑟))
55	54	anbi2d 630	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑟 → ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) ↔ (𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟)))
56		breq2 5147	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑟 → (𝑡 ≤ 𝑐 ↔ 𝑡 ≤ 𝑟))
57	55, 56	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑐 = 𝑟 → (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐) ↔ ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟)))
58	57	spvv 1996	. . . . . . . . 9 ⊢ (∀𝑐((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐) → ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟))
59		pm3.3 448	. . . . . . . . . . . . 13 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → (𝑡 ≤ 𝑠 → (𝑠 ≤ 𝑟 → 𝑡 ≤ 𝑟)))
60	59	adantld 490	. . . . . . . . . . . 12 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → (𝑠 ≤ 𝑟 → 𝑡 ≤ 𝑟)))
61	60	com23 86	. . . . . . . . . . 11 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → (𝑠 ≤ 𝑟 → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑡 ≤ 𝑟)))
62	61	adantld 490	. . . . . . . . . 10 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑡 ≤ 𝑟)))
63	62	impd 410	. . . . . . . . 9 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑡 ≤ 𝑟))
64	48, 53, 58, 63	4syl 19	. . . . . . . 8 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑡 ≤ 𝑟))
65	42, 64	jcad 512	. . . . . . 7 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → (𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟)))
66		brin 5195	. . . . . . . 8 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑡 ↔ (𝑟 ≤ 𝑡 ∧ 𝑟◡ ≤ 𝑡))
67	8, 14	brcnv 5893	. . . . . . . . 9 ⊢ (𝑟◡ ≤ 𝑡 ↔ 𝑡 ≤ 𝑟)
68	67	anbi2i 623	. . . . . . . 8 ⊢ ((𝑟 ≤ 𝑡 ∧ 𝑟◡ ≤ 𝑡) ↔ (𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟))
69	66, 68	bitr2i 276	. . . . . . 7 ⊢ ((𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟) ↔ 𝑟( ≤ ∩ ◡ ≤ )𝑡)
70	65, 69	imbitrdi 251	. . . . . 6 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑟( ≤ ∩ ◡ ≤ )𝑡))
71	18, 70	biimtrid 242	. . . . 5 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡))
72	9, 8	brcnv 5893	. . . . . . . . 9 ⊢ (𝑠◡ ≤ 𝑟 ↔ 𝑟 ≤ 𝑠)
73	72	bicomi 224	. . . . . . . 8 ⊢ (𝑟 ≤ 𝑠 ↔ 𝑠◡ ≤ 𝑟)
74	73, 10	anbi12ci 629	. . . . . . 7 ⊢ ((𝑟 ≤ 𝑠 ∧ 𝑟◡ ≤ 𝑠) ↔ (𝑠 ≤ 𝑟 ∧ 𝑠◡ ≤ 𝑟))
75		brin 5195	. . . . . . 7 ⊢ (𝑠( ≤ ∩ ◡ ≤ )𝑟 ↔ (𝑠 ≤ 𝑟 ∧ 𝑠◡ ≤ 𝑟))
76	74, 7, 75	3bitr4i 303	. . . . . 6 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 ↔ 𝑠( ≤ ∩ ◡ ≤ )𝑟)
77	76	biimpi 216	. . . . 5 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟)
78	71, 77	jctil 519	. . . 4 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡)))
79	78	alrimiv 1927	. . 3 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑡((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡)))
80	79	alrimivv 1928	. 2 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑟∀𝑠∀𝑡((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡)))
81		dfer2 8746	. 2 ⊢ (( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ) ↔ (Rel ( ≤ ∩ ◡ ≤ ) ∧ dom ( ≤ ∩ ◡ ≤ ) = dom ( ≤ ∩ ◡ ≤ ) ∧ ∀𝑟∀𝑠∀𝑡((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡))))
82	5, 6, 80, 81	syl3anbrc 1344	1 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ))

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538   = wceq 1540   ∩ cin 3950   ⊆ wss 3951   class class class wbr 5143  ^◡ccnv 5684  dom cdm 5685  Rel wrel 5690   Er wer 8742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-er 8745

This theorem is referenced by: (None)