Theorem trer 37074

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 4183	. . . 4 ⊢ ( ≤ ∩ ◡ ≤ ) ⊆ ◡ ≤
2		relcnv 6098	. . . 4 ⊢ Rel ◡ ≤
3		relss 5758	. . . 4 ⊢ (( ≤ ∩ ◡ ≤ ) ⊆ ◡ ≤ → (Rel ◡ ≤ → Rel ( ≤ ∩ ◡ ≤ )))
4	1, 2, 3	mp2 9	. . 3 ⊢ Rel ( ≤ ∩ ◡ ≤ )
5	4	a1i 11	. 2 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → Rel ( ≤ ∩ ◡ ≤ ))
6		eqidd 2762	. 2 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → dom ( ≤ ∩ ◡ ≤ ) = dom ( ≤ ∩ ◡ ≤ ))
7		brin 5157	. . . . . . . 8 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 ↔ (𝑟 ≤ 𝑠 ∧ 𝑟◡ ≤ 𝑠))
8		vex 3455	. . . . . . . . . 10 ⊢ 𝑟 ∈ V
9		vex 3455	. . . . . . . . . 10 ⊢ 𝑠 ∈ V
10	8, 9	brcnv 5860	. . . . . . . . 9 ⊢ (𝑟◡ ≤ 𝑠 ↔ 𝑠 ≤ 𝑟)
11	10	anbi2i 635	. . . . . . . 8 ⊢ ((𝑟 ≤ 𝑠 ∧ 𝑟◡ ≤ 𝑠) ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟))
12	7, 11	bitri 278	. . . . . . 7 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟))
13		brin 5157	. . . . . . . 8 ⊢ (𝑠( ≤ ∩ ◡ ≤ )𝑡 ↔ (𝑠 ≤ 𝑡 ∧ 𝑠◡ ≤ 𝑡))
14		vex 3455	. . . . . . . . . 10 ⊢ 𝑡 ∈ V
15	9, 14	brcnv 5860	. . . . . . . . 9 ⊢ (𝑠◡ ≤ 𝑡 ↔ 𝑡 ≤ 𝑠)
16	15	anbi2i 635	. . . . . . . 8 ⊢ ((𝑠 ≤ 𝑡 ∧ 𝑠◡ ≤ 𝑡) ↔ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠))
17	13, 16	bitri 278	. . . . . . 7 ⊢ (𝑠( ≤ ∩ ◡ ≤ )𝑡 ↔ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠))
18	12, 17	anbi12i 640	. . . . . 6 ⊢ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) ↔ ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)))
19		breq1 5106	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑟 → (𝑎 ≤ 𝑏 ↔ 𝑟 ≤ 𝑏))
20	19	anbi1d 643	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑟 → ((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐)))
21		breq1 5106	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑟 → (𝑎 ≤ 𝑐 ↔ 𝑟 ≤ 𝑐))
22	20, 21	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑟 → (((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
23	22	2albidv 1956	. . . . . . . . . 10 ⊢ (𝑎 = 𝑟 → (∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ∀𝑏∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
24	23	spvv 2021	. . . . . . . . 9 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑏∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐))
25		breq2 5107	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑠 → (𝑟 ≤ 𝑏 ↔ 𝑟 ≤ 𝑠))
26		breq1 5106	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑠 → (𝑏 ≤ 𝑐 ↔ 𝑠 ≤ 𝑐))
27	25, 26	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑠 → ((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐)))
28	27	imbi1d 344	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑠 → (((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐) ↔ ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
29	28	albidv 1953	. . . . . . . . . 10 ⊢ (𝑏 = 𝑠 → (∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐) ↔ ∀𝑐((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐)))
30	29	spvv 2021	. . . . . . . . 9 ⊢ (∀𝑏∀𝑐((𝑟 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑟 ≤ 𝑐) → ∀𝑐((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐))
31		breq2 5107	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑡 → (𝑠 ≤ 𝑐 ↔ 𝑠 ≤ 𝑡))
32	31	anbi2d 642	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑡 → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) ↔ (𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡)))
33		breq2 5107	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑡 → (𝑟 ≤ 𝑐 ↔ 𝑟 ≤ 𝑡))
34	32, 33	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑐 = 𝑡 → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐) ↔ ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡)))
35	34	spvv 2021	. . . . . . . . 9 ⊢ (∀𝑐((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑟 ≤ 𝑐) → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡))
36		pm3.3 454	. . . . . . . . . . . . . 14 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (𝑟 ≤ 𝑠 → (𝑠 ≤ 𝑡 → 𝑟 ≤ 𝑡)))
37	36	com23 87	. . . . . . . . . . . . 13 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (𝑠 ≤ 𝑡 → (𝑟 ≤ 𝑠 → 𝑟 ≤ 𝑡)))
38	37	adantrd 497	. . . . . . . . . . . 12 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → (𝑟 ≤ 𝑠 → 𝑟 ≤ 𝑡)))
39	38	com23 87	. . . . . . . . . . 11 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (𝑟 ≤ 𝑠 → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑟 ≤ 𝑡)))
40	39	adantrd 497	. . . . . . . . . 10 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑟 ≤ 𝑡)))
41	40	impd 416	. . . . . . . . 9 ⊢ (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑡) → 𝑟 ≤ 𝑡) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑟 ≤ 𝑡))
42	24, 30, 35, 41	4syl 20	. . . . . . . 8 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑟 ≤ 𝑡))
43		breq1 5106	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑡 → (𝑎 ≤ 𝑏 ↔ 𝑡 ≤ 𝑏))
44	43	anbi1d 643	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑡 → ((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐)))
45		breq1 5106	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑡 → (𝑎 ≤ 𝑐 ↔ 𝑡 ≤ 𝑐))
46	44, 45	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑡 → (((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
47	46	2albidv 1956	. . . . . . . . . 10 ⊢ (𝑎 = 𝑡 → (∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) ↔ ∀𝑏∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
48	47	spvv 2021	. . . . . . . . 9 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑏∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐))
49		breq2 5107	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑠 → (𝑡 ≤ 𝑏 ↔ 𝑡 ≤ 𝑠))
50	49, 26	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑠 → ((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) ↔ (𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐)))
51	50	imbi1d 344	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑠 → (((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐) ↔ ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
52	51	albidv 1953	. . . . . . . . . 10 ⊢ (𝑏 = 𝑠 → (∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐) ↔ ∀𝑐((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐)))
53	52	spvv 2021	. . . . . . . . 9 ⊢ (∀𝑏∀𝑐((𝑡 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑡 ≤ 𝑐) → ∀𝑐((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐))
54		breq2 5107	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑟 → (𝑠 ≤ 𝑐 ↔ 𝑠 ≤ 𝑟))
55	54	anbi2d 642	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑟 → ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) ↔ (𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟)))
56		breq2 5107	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑟 → (𝑡 ≤ 𝑐 ↔ 𝑡 ≤ 𝑟))
57	55, 56	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑐 = 𝑟 → (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐) ↔ ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟)))
58	57	spvv 2021	. . . . . . . . 9 ⊢ (∀𝑐((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑐) → 𝑡 ≤ 𝑐) → ((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟))
59		pm3.3 454	. . . . . . . . . . . . 13 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → (𝑡 ≤ 𝑠 → (𝑠 ≤ 𝑟 → 𝑡 ≤ 𝑟)))
60	59	adantld 496	. . . . . . . . . . . 12 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → (𝑠 ≤ 𝑟 → 𝑡 ≤ 𝑟)))
61	60	com23 87	. . . . . . . . . . 11 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → (𝑠 ≤ 𝑟 → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑡 ≤ 𝑟)))
62	61	adantld 496	. . . . . . . . . 10 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → ((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → ((𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠) → 𝑡 ≤ 𝑟)))
63	62	impd 416	. . . . . . . . 9 ⊢ (((𝑡 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) → 𝑡 ≤ 𝑟) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑡 ≤ 𝑟))
64	48, 53, 58, 63	4syl 20	. . . . . . . 8 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑡 ≤ 𝑟))
65	42, 64	jcad 522	. . . . . . 7 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → (𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟)))
66		brin 5157	. . . . . . . 8 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑡 ↔ (𝑟 ≤ 𝑡 ∧ 𝑟◡ ≤ 𝑡))
67	8, 14	brcnv 5860	. . . . . . . . 9 ⊢ (𝑟◡ ≤ 𝑡 ↔ 𝑡 ≤ 𝑟)
68	67	anbi2i 635	. . . . . . . 8 ⊢ ((𝑟 ≤ 𝑡 ∧ 𝑟◡ ≤ 𝑡) ↔ (𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟))
69	66, 68	bitr2i 279	. . . . . . 7 ⊢ ((𝑟 ≤ 𝑡 ∧ 𝑡 ≤ 𝑟) ↔ 𝑟( ≤ ∩ ◡ ≤ )𝑡)
70	65, 69	imbitrdi 254	. . . . . 6 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → (((𝑟 ≤ 𝑠 ∧ 𝑠 ≤ 𝑟) ∧ (𝑠 ≤ 𝑡 ∧ 𝑡 ≤ 𝑠)) → 𝑟( ≤ ∩ ◡ ≤ )𝑡))
71	18, 70	biimtrid 245	. . . . 5 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡))
72	9, 8	brcnv 5860	. . . . . . . . 9 ⊢ (𝑠◡ ≤ 𝑟 ↔ 𝑟 ≤ 𝑠)
73	72	bicomi 227	. . . . . . . 8 ⊢ (𝑟 ≤ 𝑠 ↔ 𝑠◡ ≤ 𝑟)
74	73, 10	anbi12ci 641	. . . . . . 7 ⊢ ((𝑟 ≤ 𝑠 ∧ 𝑟◡ ≤ 𝑠) ↔ (𝑠 ≤ 𝑟 ∧ 𝑠◡ ≤ 𝑟))
75		brin 5157	. . . . . . 7 ⊢ (𝑠( ≤ ∩ ◡ ≤ )𝑟 ↔ (𝑠 ≤ 𝑟 ∧ 𝑠◡ ≤ 𝑟))
76	74, 7, 75	3bitr4i 306	. . . . . 6 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 ↔ 𝑠( ≤ ∩ ◡ ≤ )𝑟)
77	76	biimpi 219	. . . . 5 ⊢ (𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟)
78	71, 77	jctil 529	. . . 4 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡)))
79	78	alrimiv 1960	. . 3 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑡((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡)))
80	79	alrimivv 1961	. 2 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ∀𝑟∀𝑠∀𝑡((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡)))
81		dfer2 8702	. 2 ⊢ (( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ) ↔ (Rel ( ≤ ∩ ◡ ≤ ) ∧ dom ( ≤ ∩ ◡ ≤ ) = dom ( ≤ ∩ ◡ ≤ ) ∧ ∀𝑟∀𝑠∀𝑡((𝑟( ≤ ∩ ◡ ≤ )𝑠 → 𝑠( ≤ ∩ ◡ ≤ )𝑟) ∧ ((𝑟( ≤ ∩ ◡ ≤ )𝑠 ∧ 𝑠( ≤ ∩ ◡ ≤ )𝑡) → 𝑟( ≤ ∩ ◡ ≤ )𝑡))))
82	5, 6, 80, 81	syl3anbrc 1362	1 ⊢ (∀𝑎∀𝑏∀𝑐((𝑎 ≤ 𝑏 ∧ 𝑏 ≤ 𝑐) → 𝑎 ≤ 𝑐) → ( ≤ ∩ ◡ ≤ ) Er dom ( ≤ ∩ ◡ ≤ ))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568   = wceq 1570   ∩ cin 3898   ⊆ wss 3899   class class class wbr 5103  ^◡ccnv 5650  dom cdm 5651  Rel wrel 5656   Er wer 8698

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-er 8701

This theorem is used by: (None)