Theorem mlaoml 815

Description: Mladen's OML.

Assertion

Ref	Expression
mlaoml	((a ≡ b) ∩ (b ≡ c)) ≤ (a ≡ c)

Proof of Theorem mlaoml

Step	Hyp	Ref	Expression
1		u1lembi 702	. . . . 5 ((a →1 b) ∩ (b →1 a)) = (a ≡ b)
2	1	ran 71	. . . 4 (((a →1 b) ∩ (b →1 a)) ∩ (b →1 c)) = ((a ≡ b) ∩ (b →1 c))
3		mlalem 814	. . . 4 ((a ≡ b) ∩ (b →1 c)) ≤ (a →1 c)
4	2, 3	bltr 130	. . 3 (((a →1 b) ∩ (b →1 a)) ∩ (b →1 c)) ≤ (a →1 c)
5		ancom 68	. . . . . 6 ((b →1 a) ∩ (c →1 b)) = ((c →1 b) ∩ (b →1 a))
6	5	ran 71	. . . . 5 (((b →1 a) ∩ (c →1 b)) ∩ (b →1 c)) = (((c →1 b) ∩ (b →1 a)) ∩ (b →1 c))
7		an32 76	. . . . 5 (((c →1 b) ∩ (b →1 a)) ∩ (b →1 c)) = (((c →1 b) ∩ (b →1 c)) ∩ (b →1 a))
8		u1lembi 702	. . . . . 6 ((c →1 b) ∩ (b →1 c)) = (c ≡ b)
9	8	ran 71	. . . . 5 (((c →1 b) ∩ (b →1 c)) ∩ (b →1 a)) = ((c ≡ b) ∩ (b →1 a))
10	6, 7, 9	3tr 62	. . . 4 (((b →1 a) ∩ (c →1 b)) ∩ (b →1 c)) = ((c ≡ b) ∩ (b →1 a))
11		mlalem 814	. . . 4 ((c ≡ b) ∩ (b →1 a)) ≤ (c →1 a)
12	10, 11	bltr 130	. . 3 (((b →1 a) ∩ (c →1 b)) ∩ (b →1 c)) ≤ (c →1 a)
13	4, 12	le2an 161	. 2 ((((a →1 b) ∩ (b →1 a)) ∩ (b →1 c)) ∩ (((b →1 a) ∩ (c →1 b)) ∩ (b →1 c))) ≤ ((a →1 c) ∩ (c →1 a))
14		an12 74	. . . . . 6 ((b →1 a) ∩ ((a →1 b) ∩ (c →1 b))) = ((a →1 b) ∩ ((b →1 a) ∩ (c →1 b)))
15		ancom 68	. . . . . . . 8 ((a →1 b) ∩ (b →1 a)) = ((b →1 a) ∩ (a →1 b))
16	15	ran 71	. . . . . . 7 (((a →1 b) ∩ (b →1 a)) ∩ ((b →1 a) ∩ (c →1 b))) = (((b →1 a) ∩ (a →1 b)) ∩ ((b →1 a) ∩ (c →1 b)))
17		id 58	. . . . . . 7 (((a →1 b) ∩ (b →1 a)) ∩ ((b →1 a) ∩ (c →1 b))) = (((a →1 b) ∩ (b →1 a)) ∩ ((b →1 a) ∩ (c →1 b)))
18		anandi 106	. . . . . . 7 ((b →1 a) ∩ ((a →1 b) ∩ (c →1 b))) = (((b →1 a) ∩ (a →1 b)) ∩ ((b →1 a) ∩ (c →1 b)))
19	16, 17, 18	3tr1 60	. . . . . 6 (((a →1 b) ∩ (b →1 a)) ∩ ((b →1 a) ∩ (c →1 b))) = ((b →1 a) ∩ ((a →1 b) ∩ (c →1 b)))
20		anass 69	. . . . . 6 (((a →1 b) ∩ (b →1 a)) ∩ (c →1 b)) = ((a →1 b) ∩ ((b →1 a) ∩ (c →1 b)))
21	14, 19, 20	3tr1 60	. . . . 5 (((a →1 b) ∩ (b →1 a)) ∩ ((b →1 a) ∩ (c →1 b))) = (((a →1 b) ∩ (b →1 a)) ∩ (c →1 b))
22	21	ran 71	. . . 4 ((((a →1 b) ∩ (b →1 a)) ∩ ((b →1 a) ∩ (c →1 b))) ∩ (b →1 c)) = ((((a →1 b) ∩ (b →1 a)) ∩ (c →1 b)) ∩ (b →1 c))
23		anandir 107	. . . 4 ((((a →1 b) ∩ (b →1 a)) ∩ ((b →1 a) ∩ (c →1 b))) ∩ (b →1 c)) = ((((a →1 b) ∩ (b →1 a)) ∩ (b →1 c)) ∩ (((b →1 a) ∩ (c →1 b)) ∩ (b →1 c)))
24		an32 76	. . . 4 ((((a →1 b) ∩ (b →1 a)) ∩ (c →1 b)) ∩ (b →1 c)) = ((((a →1 b) ∩ (b →1 a)) ∩ (b →1 c)) ∩ (c →1 b))
25	22, 23, 24	3tr2 61	. . 3 ((((a →1 b) ∩ (b →1 a)) ∩ (b →1 c)) ∩ (((b →1 a) ∩ (c →1 b)) ∩ (b →1 c))) = ((((a →1 b) ∩ (b →1 a)) ∩ (b →1 c)) ∩ (c →1 b))
26		anass 69	. . 3 ((((a →1 b) ∩ (b →1 a)) ∩ (b →1 c)) ∩ (c →1 b)) = (((a →1 b) ∩ (b →1 a)) ∩ ((b →1 c) ∩ (c →1 b)))
27		u1lembi 702	. . . 4 ((b →1 c) ∩ (c →1 b)) = (b ≡ c)
28	1, 27	2an 72	. . 3 (((a →1 b) ∩ (b →1 a)) ∩ ((b →1 c) ∩ (c →1 b))) = ((a ≡ b) ∩ (b ≡ c))
29	25, 26, 28	3tr 62	. 2 ((((a →1 b) ∩ (b →1 a)) ∩ (b →1 c)) ∩ (((b →1 a) ∩ (c →1 b)) ∩ (b →1 c))) = ((a ≡ b) ∩ (b ≡ c))
30		u1lembi 702	. 2 ((a →1 c) ∩ (c →1 a)) = (a ≡ c)
31	13, 29, 30	le3tr2 133	1 ((a ≡ b) ∩ (b ≡ c)) ≤ (a ≡ c)

Syntax hints:   ≤ wle 2   ≡ tb 5   ∩ wa 7   →₁ wi1 13

This theorem is referenced by:  eqtr4 816  mlaconj4 826

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org