Theorem oago3.21x 872

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.

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 339	. . . . . 6 (a →5 b) ≤ (a →1 b)
2		i5lei2 340	. . . . . 6 (b →5 c) ≤ (b →2 c)
3	1, 2	le2an 161	. . . . 5 ((a →5 b) ∩ (b →5 c)) ≤ ((a →1 b) ∩ (b →2 c))
4		i5lei1 339	. . . . 5 (c →5 d) ≤ (c →1 d)
5	3, 4	le2an 161	. . . 4 (((a →5 b) ∩ (b →5 c)) ∩ (c →5 d)) ≤ (((a →1 b) ∩ (b →2 c)) ∩ (c →1 d))
6		i5lei2 340	. . . 4 (d →5 a) ≤ (d →2 a)
7	5, 6	le2an 161	. . 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 870	. . 3 ((((a →1 b) ∩ (b →2 c)) ∩ (c →1 d)) ∩ (d →2 a)) = (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))
9	7, 8	lbtr 131	. 2 ((((a →5 b) ∩ (b →5 c)) ∩ (c →5 d)) ∩ (d →5 a)) ≤ (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))
10		leid 140	. . . 4 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ≤ (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))
11		eqtr4 816	. . . . 5 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ≤ (a ≡ d)
12		bicom 88	. . . . 5 (a ≡ d) = (d ≡ a)
13	11, 12	lbtr 131	. . . 4 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ≤ (d ≡ a)
14	10, 13	ler2an 165	. . 3 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ≤ ((((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ∩ (d ≡ a))
15		u5lembi 707	. . . . . . . 8 ((a →5 b) ∩ (b →5 a)) = (a ≡ b)
16	15	ax-r1 34	. . . . . . 7 (a ≡ b) = ((a →5 b) ∩ (b →5 a))
17		lea 152	. . . . . . 7 ((a →5 b) ∩ (b →5 a)) ≤ (a →5 b)
18	16, 17	bltr 130	. . . . . 6 (a ≡ b) ≤ (a →5 b)
19		u5lembi 707	. . . . . . . 8 ((b →5 c) ∩ (c →5 b)) = (b ≡ c)
20	19	ax-r1 34	. . . . . . 7 (b ≡ c) = ((b →5 c) ∩ (c →5 b))
21		lea 152	. . . . . . 7 ((b →5 c) ∩ (c →5 b)) ≤ (b →5 c)
22	20, 21	bltr 130	. . . . . 6 (b ≡ c) ≤ (b →5 c)
23	18, 22	le2an 161	. . . . 5 ((a ≡ b) ∩ (b ≡ c)) ≤ ((a →5 b) ∩ (b →5 c))
24		u5lembi 707	. . . . . . 7 ((c →5 d) ∩ (d →5 c)) = (c ≡ d)
25	24	ax-r1 34	. . . . . 6 (c ≡ d) = ((c →5 d) ∩ (d →5 c))
26		lea 152	. . . . . 6 ((c →5 d) ∩ (d →5 c)) ≤ (c →5 d)
27	25, 26	bltr 130	. . . . 5 (c ≡ d) ≤ (c →5 d)
28	23, 27	le2an 161	. . . 4 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ≤ (((a →5 b) ∩ (b →5 c)) ∩ (c →5 d))
29		u5lembi 707	. . . . . 6 ((d →5 a) ∩ (a →5 d)) = (d ≡ a)
30	29	ax-r1 34	. . . . 5 (d ≡ a) = ((d →5 a) ∩ (a →5 d))
31		lea 152	. . . . 5 ((d →5 a) ∩ (a →5 d)) ≤ (d →5 a)
32	30, 31	bltr 130	. . . 4 (d ≡ a) ≤ (d →5 a)
33	28, 32	le2an 161	. . 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 129	. 2 (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ≤ ((((a →5 b) ∩ (b →5 c)) ∩ (c →5 d)) ∩ (d →5 a))
35	9, 34	lebi 137	1 ((((a →5 b) ∩ (b →5 c)) ∩ (c →5 d)) ∩ (d →5 a)) = (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))

Syntax hints:   = wb 1   ≡ tb 5   ∩ wa 7   →₁ wi1 13   →₂ wi2 14   →₅ wi5 17

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-i2 44  df-i5 47  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org