Theorem mlaoml 833

Description: Mladen's OML. (Contributed by NM, 4-Nov-1998.)

Assertion

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

Proof of Theorem mlaoml

Step	Hyp	Ref	Expression
1		u1lembi 720	. . . . 5 ((a →1 b) ∩ (b →1 a)) = (a ≡ b)
2	1	ran 78	. . . 4 (((a →1 b) ∩ (b →1 a)) ∩ (b →1 c)) = ((a ≡ b) ∩ (b →1 c))
3		mlalem 832	. . . 4 ((a ≡ b) ∩ (b →1 c)) ≤ (a →1 c)
4	2, 3	bltr 138	. . 3 (((a →1 b) ∩ (b →1 a)) ∩ (b →1 c)) ≤ (a →1 c)
5		ancom 74	. . . . . 6 ((b →1 a) ∩ (c →1 b)) = ((c →1 b) ∩ (b →1 a))
6	5	ran 78	. . . . 5 (((b →1 a) ∩ (c →1 b)) ∩ (b →1 c)) = (((c →1 b) ∩ (b →1 a)) ∩ (b →1 c))
7		an32 83	. . . . 5 (((c →1 b) ∩ (b →1 a)) ∩ (b →1 c)) = (((c →1 b) ∩ (b →1 c)) ∩ (b →1 a))
8		u1lembi 720	. . . . . 6 ((c →1 b) ∩ (b →1 c)) = (c ≡ b)
9	8	ran 78	. . . . 5 (((c →1 b) ∩ (b →1 c)) ∩ (b →1 a)) = ((c ≡ b) ∩ (b →1 a))
10	6, 7, 9	3tr 65	. . . 4 (((b →1 a) ∩ (c →1 b)) ∩ (b →1 c)) = ((c ≡ b) ∩ (b →1 a))
11		mlalem 832	. . . 4 ((c ≡ b) ∩ (b →1 a)) ≤ (c →1 a)
12	10, 11	bltr 138	. . 3 (((b →1 a) ∩ (c →1 b)) ∩ (b →1 c)) ≤ (c →1 a)
13	4, 12	le2an 169	. 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 81	. . . . . 6 ((b →1 a) ∩ ((a →1 b) ∩ (c →1 b))) = ((a →1 b) ∩ ((b →1 a) ∩ (c →1 b)))
15		ancom 74	. . . . . . . 8 ((a →1 b) ∩ (b →1 a)) = ((b →1 a) ∩ (a →1 b))
16	15	ran 78	. . . . . . 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 59	. . . . . . 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 114	. . . . . . 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 63	. . . . . 6 (((a →1 b) ∩ (b →1 a)) ∩ ((b →1 a) ∩ (c →1 b))) = ((b →1 a) ∩ ((a →1 b) ∩ (c →1 b)))
20		anass 76	. . . . . 6 (((a →1 b) ∩ (b →1 a)) ∩ (c →1 b)) = ((a →1 b) ∩ ((b →1 a) ∩ (c →1 b)))
21	14, 19, 20	3tr1 63	. . . . 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 78	. . . 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 115	. . . 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 83	. . . 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 64	. . 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 76	. . 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 720	. . . 4 ((b →1 c) ∩ (c →1 b)) = (b ≡ c)
28	1, 27	2an 79	. . 3 (((a →1 b) ∩ (b →1 a)) ∩ ((b →1 c) ∩ (c →1 b))) = ((a ≡ b) ∩ (b ≡ c))
29	25, 26, 28	3tr 65	. 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 720	. 2 ((a →1 c) ∩ (c →1 a)) = (a ≡ c)
31	13, 29, 30	le3tr2 141	1 ((a ≡ b) ∩ (b ≡ c)) ≤ (a ≡ c)

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

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

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  eqtr4  834  mlaconj4  844