Theorem trer 34505

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 4163	. . . 4 ⊢ ( ≤ ∩ ◡ ≤ ) ⊆ ◡ ≤
2		relcnv 6012	. . . 4 ⊢ Rel ◡ ≤
3		relss 5692	. . . 4 ⊢ (( ≤ ∩ ◡ ≤ ) ⊆ ◡ ≤ → (Rel ◡ ≤ → Rel ( ≤ ∩ ◡ ≤ )))
4	1, 2, 3	mp2 9	. . 3 ⊢ Rel ( ≤ ∩ ◡ ≤ )
5	4	a1i 11	. 2 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → Rel ( ≤ ∩ ◡ ≤ ))
6		eqidd 2739	. 2 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → dom ( ≤ ∩ ◡ ≤ ) = dom ( ≤ ∩ ◡ ≤ ))
7		brin 5126	. . . . . . . 8 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 ↔ (𝑟 ≤ 𝑠 ∧ 𝑟◡ ≤ 𝑠))
8		vex 3436	. . . . . . . . . 10 ⊢ 𝑟 ∈ V
9		vex 3436	. . . . . . . . . 10 ⊢ 𝑠 ∈ V
10	8, 9	brcnv 5791	. . . . . . . . 9 ⊢ (𝑟◡ ≤ 𝑠 ↔ 𝑠 ≤ 𝑟)
11	10	anbi2i 623	. . . . . . . 8 ⊢ ((𝑟 ≤ 𝑠 ∧ 𝑟◡ ≤ 𝑠) ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟))
12	7, 11	bitri 274	. . . . . . 7 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟))
13		brin 5126	. . . . . . . 8 ⊢ (𝑠( ≤ ∩ ◡ ≤ )𝑡 ↔ (𝑠 ≤ 𝑡 ∧ 𝑠◡ ≤ 𝑡))
14		vex 3436	. . . . . . . . . 10 ⊢ 𝑡 ∈ V
15	9, 14	brcnv 5791	. . . . . . . . 9 ⊢ (𝑠◡ ≤ 𝑡 ↔ 𝑡 ≤ 𝑠)
16	15	anbi2i 623	. . . . . . . 8 ⊢ ((𝑠 ≤ 𝑡 ∧ 𝑠◡ ≤ 𝑡) ↔ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠))
17	13, 16	bitri 274	. . . . . . 7 ⊢ (𝑠( ≤ ∩ ◡ ≤ )𝑡 ↔ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠))
18	12, 17	anbi12i 627	. . . . . 6 ⊢ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) ↔ ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)))
19		breq1 5077	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑟 → (𝑎 ≤ 𝑏 ↔ 𝑟 ≤ 𝑏))
20	19	anbi1d 630	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑟 → ((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐)))
21		breq1 5077	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑟 → (𝑎 ≤ 𝑐 ↔ 𝑟 ≤ 𝑐))
22	20, 21	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑟 → (((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
23	22	2albidv 1926	. . . . . . . . . 10 ⊢ (𝑎 = 𝑟 → (∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ∀𝑏∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
24	23	spvv 2000	. . . . . . . . 9 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑏∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐))
25		breq2 5078	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑠 → (𝑟 ≤ 𝑏 ↔ 𝑟 ≤ 𝑠))
26		breq1 5077	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑠 → (𝑏 ≤ 𝑐 ↔ 𝑠 ≤ 𝑐))
27	25, 26	anbi12d 631	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑠 → ((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐)))
28	27	imbi1d 342	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑠 → (((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐) ↔ ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
29	28	albidv 1923	. . . . . . . . . 10 ⊢ (𝑏 = 𝑠 → (∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐) ↔ ∀𝑐((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
30	29	spvv 2000	. . . . . . . . 9 ⊢ (∀𝑏∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐) → ∀𝑐((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐))
31		breq2 5078	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑡 → (𝑠 ≤ 𝑐 ↔ 𝑠 ≤ 𝑡))
32	31	anbi2d 629	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑡 → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡)))
33		breq2 5078	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑡 → (𝑟 ≤ 𝑐 ↔ 𝑟 ≤ 𝑡))
34	32, 33	imbi12d 345	. . . . . . . . . 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 5077	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑡 → (𝑎 ≤ 𝑏 ↔ 𝑡 ≤ 𝑏))
44	43	anbi1d 630	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑡 → ((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐)))
45		breq1 5077	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑡 → (𝑎 ≤ 𝑐 ↔ 𝑡 ≤ 𝑐))
46	44, 45	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑡 → (((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
47	46	2albidv 1926	. . . . . . . . . 10 ⊢ (𝑎 = 𝑡 → (∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ∀𝑏∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
48	47	spvv 2000	. . . . . . . . 9 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑏∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐))
49		breq2 5078	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑠 → (𝑡 ≤ 𝑏 ↔ 𝑡 ≤ 𝑠))
50	49, 26	anbi12d 631	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑠 → ((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐)))
51	50	imbi1d 342	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑠 → (((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐) ↔ ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
52	51	albidv 1923	. . . . . . . . . 10 ⊢ (𝑏 = 𝑠 → (∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐) ↔ ∀𝑐((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
53	52	spvv 2000	. . . . . . . . 9 ⊢ (∀𝑏∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐) → ∀𝑐((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐))
54		breq2 5078	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑟 → (𝑠 ≤ 𝑐 ↔ 𝑠 ≤ 𝑟))
55	54	anbi2d 629	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑟 → ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) ↔ (𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟)))
56		breq2 5078	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑟 → (𝑡 ≤ 𝑐 ↔ 𝑡 ≤ 𝑟))
57	55, 56	imbi12d 345	. . . . . . . . . 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 5126	. . . . . . . 8 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑡 ↔ (𝑟 ≤ 𝑡 ∧ 𝑟◡ ≤ 𝑡))
67	8, 14	brcnv 5791	. . . . . . . . 9 ⊢ (𝑟◡ ≤ 𝑡 ↔ 𝑡 ≤ 𝑟)
68	67	anbi2i 623	. . . . . . . 8 ⊢ ((𝑟 ≤ 𝑡 ∧ 𝑟◡ ≤ 𝑡) ↔ (𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟))
69	66, 68	bitr2i 275	. . . . . . 7 ⊢ ((𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟) ↔ 𝑟( ≤ ∩ ◡ ≤ )𝑡)
70	65, 69	syl6ib 250	. . . . . 6 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑟( ≤ ∩ ◡ ≤ )𝑡))
71	18, 70	syl5bi 241	. . . . 5 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡))
72	9, 8	brcnv 5791	. . . . . . . . 9 ⊢ (𝑠◡ ≤ 𝑟 ↔ 𝑟 ≤ 𝑠)
73	72	bicomi 223	. . . . . . . 8 ⊢ (𝑟 ≤ 𝑠 ↔ 𝑠◡ ≤ 𝑟)
74	73, 10	anbi12ci 628	. . . . . . 7 ⊢ ((𝑟 ≤ 𝑠 ∧ 𝑟◡ ≤ 𝑠) ↔ (𝑠 ≤ 𝑟 ∧ 𝑠◡ ≤ 𝑟))
75		brin 5126	. . . . . . 7 ⊢ (𝑠( ≤ ∩ ◡ ≤ )𝑟 ↔ (𝑠 ≤ 𝑟 ∧ 𝑠◡ ≤ 𝑟))
76	74, 7, 75	3bitr4i 303	. . . . . 6 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 ↔ 𝑠( ≤ ∩ ◡ ≤ )𝑟)
77	76	biimpi 215	. . . . 5 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟)
78	71, 77	jctil 520	. . . 4 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡)))
79	78	alrimiv 1930	. . 3 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑡((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡)))
80	79	alrimivv 1931	. 2 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑟∀𝑠∀𝑡((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡)))
81		dfer2 8499	. 2 ⊢ (( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ) ↔ (Rel ( ≤ ∩ ◡ ≤ ) ∧ dom ( ≤ ∩ ◡ ≤ ) = dom ( ≤ ∩ ◡ ≤ ) ∧ ∀𝑟∀𝑠∀𝑡((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡))))
82	5, 6, 80, 81	syl3anbrc 1342	1 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ))

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1537   = wceq 1539   ∩ cin 3886   ⊆ wss 3887   class class class wbr 5074  ^◡ccnv 5588  dom cdm 5589  Rel wrel 5594   Er wer 8495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-er 8498

This theorem is referenced by: (None)