Theorem trer 33777

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 4156	. . . 4 ⊢ ( ≤ ∩ ◡ ≤ ) ⊆ ◡ ≤
2		relcnv 5934	. . . 4 ⊢ Rel ◡ ≤
3		relss 5620	. . . 4 ⊢ (( ≤ ∩ ◡ ≤ ) ⊆ ◡ ≤ → (Rel ◡ ≤ → Rel ( ≤ ∩ ◡ ≤ )))
4	1, 2, 3	mp2 9	. . 3 ⊢ Rel ( ≤ ∩ ◡ ≤ )
5	4	a1i 11	. 2 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → Rel ( ≤ ∩ ◡ ≤ ))
6		eqidd 2799	. 2 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → dom ( ≤ ∩ ◡ ≤ ) = dom ( ≤ ∩ ◡ ≤ ))
7		brin 5082	. . . . . . . 8 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 ↔ (𝑟 ≤ 𝑠 ∧ 𝑟◡ ≤ 𝑠))
8		vex 3444	. . . . . . . . . 10 ⊢ 𝑟 ∈ V
9		vex 3444	. . . . . . . . . 10 ⊢ 𝑠 ∈ V
10	8, 9	brcnv 5717	. . . . . . . . 9 ⊢ (𝑟◡ ≤ 𝑠 ↔ 𝑠 ≤ 𝑟)
11	10	anbi2i 625	. . . . . . . 8 ⊢ ((𝑟 ≤ 𝑠 ∧ 𝑟◡ ≤ 𝑠) ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟))
12	7, 11	bitri 278	. . . . . . 7 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟))
13		brin 5082	. . . . . . . 8 ⊢ (𝑠( ≤ ∩ ◡ ≤ )𝑡 ↔ (𝑠 ≤ 𝑡 ∧ 𝑠◡ ≤ 𝑡))
14		vex 3444	. . . . . . . . . 10 ⊢ 𝑡 ∈ V
15	9, 14	brcnv 5717	. . . . . . . . 9 ⊢ (𝑠◡ ≤ 𝑡 ↔ 𝑡 ≤ 𝑠)
16	15	anbi2i 625	. . . . . . . 8 ⊢ ((𝑠 ≤ 𝑡 ∧ 𝑠◡ ≤ 𝑡) ↔ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠))
17	13, 16	bitri 278	. . . . . . 7 ⊢ (𝑠( ≤ ∩ ◡ ≤ )𝑡 ↔ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠))
18	12, 17	anbi12i 629	. . . . . 6 ⊢ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) ↔ ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)))
19		breq1 5033	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑟 → (𝑎 ≤ 𝑏 ↔ 𝑟 ≤ 𝑏))
20	19	anbi1d 632	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑟 → ((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐)))
21		breq1 5033	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑟 → (𝑎 ≤ 𝑐 ↔ 𝑟 ≤ 𝑐))
22	20, 21	imbi12d 348	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑟 → (((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
23	22	2albidv 1924	. . . . . . . . . 10 ⊢ (𝑎 = 𝑟 → (∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ∀𝑏∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
24	23	spvv 2003	. . . . . . . . 9 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑏∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐))
25		breq2 5034	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑠 → (𝑟 ≤ 𝑏 ↔ 𝑟 ≤ 𝑠))
26		breq1 5033	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑠 → (𝑏 ≤ 𝑐 ↔ 𝑠 ≤ 𝑐))
27	25, 26	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑠 → ((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐)))
28	27	imbi1d 345	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑠 → (((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐) ↔ ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
29	28	albidv 1921	. . . . . . . . . 10 ⊢ (𝑏 = 𝑠 → (∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐) ↔ ∀𝑐((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
30	29	spvv 2003	. . . . . . . . 9 ⊢ (∀𝑏∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐) → ∀𝑐((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐))
31		breq2 5034	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑡 → (𝑠 ≤ 𝑐 ↔ 𝑠 ≤ 𝑡))
32	31	anbi2d 631	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑡 → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡)))
33		breq2 5034	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑡 → (𝑟 ≤ 𝑐 ↔ 𝑟 ≤ 𝑡))
34	32, 33	imbi12d 348	. . . . . . . . . 10 ⊢ (𝑐 = 𝑡 → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐) ↔ ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡)))
35	34	spvv 2003	. . . . . . . . 9 ⊢ (∀𝑐((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐) → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡))
36		pm3.3 452	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (𝑟 ≤ 𝑠 → (𝑠 ≤ 𝑡 → 𝑟 ≤ 𝑡)))
37	36	com23 86	. . . . . . . . . . . . 13 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (𝑠 ≤ 𝑡 → (𝑟 ≤ 𝑠 → 𝑟 ≤ 𝑡)))
38	37	adantrd 495	. . . . . . . . . . . 12 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → (𝑟 ≤ 𝑠 → 𝑟 ≤ 𝑡)))
39	38	com23 86	. . . . . . . . . . 11 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (𝑟 ≤ 𝑠 → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑟 ≤ 𝑡)))
40	39	adantrd 495	. . . . . . . . . 10 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑟 ≤ 𝑡)))
41	40	impd 414	. . . . . . . . 9 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑟 ≤ 𝑡))
42	24, 30, 35, 41	4syl 19	. . . . . . . 8 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑟 ≤ 𝑡))
43		breq1 5033	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑡 → (𝑎 ≤ 𝑏 ↔ 𝑡 ≤ 𝑏))
44	43	anbi1d 632	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑡 → ((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐)))
45		breq1 5033	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑡 → (𝑎 ≤ 𝑐 ↔ 𝑡 ≤ 𝑐))
46	44, 45	imbi12d 348	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑡 → (((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
47	46	2albidv 1924	. . . . . . . . . 10 ⊢ (𝑎 = 𝑡 → (∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ∀𝑏∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
48	47	spvv 2003	. . . . . . . . 9 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑏∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐))
49		breq2 5034	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑠 → (𝑡 ≤ 𝑏 ↔ 𝑡 ≤ 𝑠))
50	49, 26	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑠 → ((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐)))
51	50	imbi1d 345	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑠 → (((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐) ↔ ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
52	51	albidv 1921	. . . . . . . . . 10 ⊢ (𝑏 = 𝑠 → (∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐) ↔ ∀𝑐((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
53	52	spvv 2003	. . . . . . . . 9 ⊢ (∀𝑏∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐) → ∀𝑐((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐))
54		breq2 5034	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑟 → (𝑠 ≤ 𝑐 ↔ 𝑠 ≤ 𝑟))
55	54	anbi2d 631	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑟 → ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) ↔ (𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟)))
56		breq2 5034	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑟 → (𝑡 ≤ 𝑐 ↔ 𝑡 ≤ 𝑟))
57	55, 56	imbi12d 348	. . . . . . . . . 10 ⊢ (𝑐 = 𝑟 → (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐) ↔ ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟)))
58	57	spvv 2003	. . . . . . . . 9 ⊢ (∀𝑐((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐) → ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟))
59		pm3.3 452	. . . . . . . . . . . . 13 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → (𝑡 ≤ 𝑠 → (𝑠 ≤ 𝑟 → 𝑡 ≤ 𝑟)))
60	59	adantld 494	. . . . . . . . . . . 12 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → (𝑠 ≤ 𝑟 → 𝑡 ≤ 𝑟)))
61	60	com23 86	. . . . . . . . . . 11 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → (𝑠 ≤ 𝑟 → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑡 ≤ 𝑟)))
62	61	adantld 494	. . . . . . . . . 10 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑡 ≤ 𝑟)))
63	62	impd 414	. . . . . . . . 9 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑡 ≤ 𝑟))
64	48, 53, 58, 63	4syl 19	. . . . . . . 8 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑡 ≤ 𝑟))
65	42, 64	jcad 516	. . . . . . 7 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → (𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟)))
66		brin 5082	. . . . . . . 8 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑡 ↔ (𝑟 ≤ 𝑡 ∧ 𝑟◡ ≤ 𝑡))
67	8, 14	brcnv 5717	. . . . . . . . 9 ⊢ (𝑟◡ ≤ 𝑡 ↔ 𝑡 ≤ 𝑟)
68	67	anbi2i 625	. . . . . . . 8 ⊢ ((𝑟 ≤ 𝑡 ∧ 𝑟◡ ≤ 𝑡) ↔ (𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟))
69	66, 68	bitr2i 279	. . . . . . 7 ⊢ ((𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟) ↔ 𝑟( ≤ ∩ ◡ ≤ )𝑡)
70	65, 69	syl6ib 254	. . . . . 6 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑟( ≤ ∩ ◡ ≤ )𝑡))
71	18, 70	syl5bi 245	. . . . 5 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡))
72	9, 8	brcnv 5717	. . . . . . . . 9 ⊢ (𝑠◡ ≤ 𝑟 ↔ 𝑟 ≤ 𝑠)
73	72	bicomi 227	. . . . . . . 8 ⊢ (𝑟 ≤ 𝑠 ↔ 𝑠◡ ≤ 𝑟)
74	73, 10	anbi12ci 630	. . . . . . 7 ⊢ ((𝑟 ≤ 𝑠 ∧ 𝑟◡ ≤ 𝑠) ↔ (𝑠 ≤ 𝑟 ∧ 𝑠◡ ≤ 𝑟))
75		brin 5082	. . . . . . 7 ⊢ (𝑠( ≤ ∩ ◡ ≤ )𝑟 ↔ (𝑠 ≤ 𝑟 ∧ 𝑠◡ ≤ 𝑟))
76	74, 7, 75	3bitr4i 306	. . . . . 6 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 ↔ 𝑠( ≤ ∩ ◡ ≤ )𝑟)
77	76	biimpi 219	. . . . 5 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟)
78	71, 77	jctil 523	. . . 4 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡)))
79	78	alrimiv 1928	. . 3 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑡((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡)))
80	79	alrimivv 1929	. 2 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑟∀𝑠∀𝑡((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡)))
81		dfer2 8273	. 2 ⊢ (( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ) ↔ (Rel ( ≤ ∩ ◡ ≤ ) ∧ dom ( ≤ ∩ ◡ ≤ ) = dom ( ≤ ∩ ◡ ≤ ) ∧ ∀𝑟∀𝑠∀𝑡((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡))))
82	5, 6, 80, 81	syl3anbrc 1340	1 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ))

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1536   = wceq 1538   ∩ cin 3880   ⊆ wss 3881   class class class wbr 5030  ^◡ccnv 5518  dom cdm 5519  Rel wrel 5524   Er wer 8269

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-er 8272

This theorem is referenced by: (None)