Theorem oago3.21x 890

Description: 4-variable extension of Equation (3.21) of "Equations, states, and lattices..." paper. This shows that it holds in all OMLs, not just 4GO. (Contributed by NM, 26-Jun-2003.)

Assertion

Ref	Expression
oago3.21x	((((a →5 b) ∩ (b →5 c)) ∩ (c →5 d)) ∩ (d →5 a)) = (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))

Proof of Theorem oago3.21x

Step	Hyp	Ref	Expression
1		i5lei1 347	. . . . . 6 (a →5 b) ≤ (a →1 b)
2		i5lei2 348	. . . . . 6 (b →5 c) ≤ (b →2 c)
3	1, 2	le2an 169	. . . . 5 ((a →5 b) ∩ (b →5 c)) ≤ ((a →1 b) ∩ (b →2 c))
4		i5lei1 347	. . . . 5 (c →5 d) ≤ (c →1 d)
5	3, 4	le2an 169	. . . 4 (((a →5 b) ∩ (b →5 c)) ∩ (c →5 d)) ≤ (((a →1 b) ∩ (b →2 c)) ∩ (c →1 d))
6		i5lei2 348	. . . 4 (d →5 a) ≤ (d →2 a)
7	5, 6	le2an 169	. . 3 ((((a →5 b) ∩ (b →5 c)) ∩ (c →5 d)) ∩ (d →5 a)) ≤ ((((a →1 b) ∩ (b →2 c)) ∩ (c →1 d)) ∩ (d →2 a))
8		mhcor1 888	. . 3 ((((a →1 b) ∩ (b →2 c)) ∩ (c →1 d)) ∩ (d →2 a)) = (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))
9	7, 8	lbtr 139	. 2 ((((a →5 b) ∩ (b →5 c)) ∩ (c →5 d)) ∩ (d →5 a)) ≤ (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))
10		leid 148	. . . 4 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ≤ (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))
11		eqtr4 834	. . . . 5 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ≤ (a ≡ d)
12		bicom 96	. . . . 5 (a ≡ d) = (d ≡ a)
13	11, 12	lbtr 139	. . . 4 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ≤ (d ≡ a)
14	10, 13	ler2an 173	. . 3 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ≤ ((((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ∩ (d ≡ a))
15		u5lembi 725	. . . . . . . 8 ((a →5 b) ∩ (b →5 a)) = (a ≡ b)
16	15	ax-r1 35	. . . . . . 7 (a ≡ b) = ((a →5 b) ∩ (b →5 a))
17		lea 160	. . . . . . 7 ((a →5 b) ∩ (b →5 a)) ≤ (a →5 b)
18	16, 17	bltr 138	. . . . . 6 (a ≡ b) ≤ (a →5 b)
19		u5lembi 725	. . . . . . . 8 ((b →5 c) ∩ (c →5 b)) = (b ≡ c)
20	19	ax-r1 35	. . . . . . 7 (b ≡ c) = ((b →5 c) ∩ (c →5 b))
21		lea 160	. . . . . . 7 ((b →5 c) ∩ (c →5 b)) ≤ (b →5 c)
22	20, 21	bltr 138	. . . . . 6 (b ≡ c) ≤ (b →5 c)
23	18, 22	le2an 169	. . . . 5 ((a ≡ b) ∩ (b ≡ c)) ≤ ((a →5 b) ∩ (b →5 c))
24		u5lembi 725	. . . . . . 7 ((c →5 d) ∩ (d →5 c)) = (c ≡ d)
25	24	ax-r1 35	. . . . . 6 (c ≡ d) = ((c →5 d) ∩ (d →5 c))
26		lea 160	. . . . . 6 ((c →5 d) ∩ (d →5 c)) ≤ (c →5 d)
27	25, 26	bltr 138	. . . . 5 (c ≡ d) ≤ (c →5 d)
28	23, 27	le2an 169	. . . 4 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ≤ (((a →5 b) ∩ (b →5 c)) ∩ (c →5 d))
29		u5lembi 725	. . . . . 6 ((d →5 a) ∩ (a →5 d)) = (d ≡ a)
30	29	ax-r1 35	. . . . 5 (d ≡ a) = ((d →5 a) ∩ (a →5 d))
31		lea 160	. . . . 5 ((d →5 a) ∩ (a →5 d)) ≤ (d →5 a)
32	30, 31	bltr 138	. . . 4 (d ≡ a) ≤ (d →5 a)
33	28, 32	le2an 169	. . 3 ((((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ∩ (d ≡ a)) ≤ ((((a →5 b) ∩ (b →5 c)) ∩ (c →5 d)) ∩ (d →5 a))
34	14, 33	letr 137	. 2 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ≤ ((((a →5 b) ∩ (b →5 c)) ∩ (c →5 d)) ∩ (d →5 a))
35	9, 34	lebi 145	1 ((((a →5 b) ∩ (b →5 c)) ∩ (c →5 d)) ∩ (d →5 a)) = (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))

This proof depends on syntax axioms:   = wb 1   ≡ tb 5   ∩ wa 7   →₁ wi1 12   →₂ wi2 13   →₅ wi5 16

This proof depends on 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 proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-i5 48  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by: (None)