Theorem sa5 818

Description: Possible axiom for a "Sasaki algebra" for orthoarguesian lattices.

Hypothesis

Ref	Expression
sa5.1	(a ->1 c) =< (b ->1 c)

Assertion

Ref	Expression
sa5	(b_|_ ->1 c) =< ((a_|_ ->1 c) v c)

Proof of Theorem sa5

Step	Hyp	Ref	Expression
1		leor 151	. . . . 5 b =< (c v b)
2		ax-a2 30	. . . . . . . . . 10 (b_|_ v c_|_) = (c_|_ v b_|_)
3	2	lan 70	. . . . . . . . 9 (b ^ (b_|_ v c_|_)) = (b ^ (c_|_ v b_|_))
4	3	ax-r5 37	. . . . . . . 8 ((b ^ (b_|_ v c_|_)) v c) = ((b ^ (c_|_ v b_|_)) v c)
5		ax-a2 30	. . . . . . . 8 ((b ^ (c_|_ v b_|_)) v c) = (c v (b ^ (c_|_ v b_|_)))
6		oml6 470	. . . . . . . 8 (c v (b ^ (c_|_ v b_|_))) = (c v b)
7	4, 5, 6	3tr 62	. . . . . . 7 ((b ^ (b_|_ v c_|_)) v c) = (c v b)
8	7	ax-r1 34	. . . . . 6 (c v b) = ((b ^ (b_|_ v c_|_)) v c)
9		sa5.1	. . . . . . . . . 10 (a ->1 c) =< (b ->1 c)
10	9	lecon 146	. . . . . . . . 9 (b ->1 c)_|_ =< (a ->1 c)_|_
11		ud1lem0c 269	. . . . . . . . 9 (b ->1 c)_|_ = (b ^ (b_|_ v c_|_))
12		ud1lem0c 269	. . . . . . . . 9 (a ->1 c)_|_ = (a ^ (a_|_ v c_|_))
13	10, 11, 12	le3tr2 133	. . . . . . . 8 (b ^ (b_|_ v c_|_)) =< (a ^ (a_|_ v c_|_))
14		lea 152	. . . . . . . 8 (a ^ (a_|_ v c_|_)) =< a
15	13, 14	letr 129	. . . . . . 7 (b ^ (b_|_ v c_|_)) =< a
16	15	leror 144	. . . . . 6 ((b ^ (b_|_ v c_|_)) v c) =< (a v c)
17	8, 16	bltr 130	. . . . 5 (c v b) =< (a v c)
18	1, 17	letr 129	. . . 4 b =< (a v c)
19		ax-a1 29	. . . 4 b = b_|__|_
20		ax-a1 29	. . . . . 6 a = a_|__|_
21		ax-a2 30	. . . . . . 7 (c v (c ^ a_|_)) = ((c ^ a_|_) v c)
22		a5b 112	. . . . . . 7 (c v (c ^ a_|_)) = c
23		ancom 68	. . . . . . . 8 (c ^ a_|_) = (a_|_ ^ c)
24	23	ax-r5 37	. . . . . . 7 ((c ^ a_|_) v c) = ((a_|_ ^ c) v c)
25	21, 22, 24	3tr2 61	. . . . . 6 c = ((a_|_ ^ c) v c)
26	20, 25	2or 67	. . . . 5 (a v c) = (a_|__|_ v ((a_|_ ^ c) v c))
27		ax-a3 31	. . . . . 6 ((a_|__|_ v (a_|_ ^ c)) v c) = (a_|__|_ v ((a_|_ ^ c) v c))
28	27	ax-r1 34	. . . . 5 (a_|__|_ v ((a_|_ ^ c) v c)) = ((a_|__|_ v (a_|_ ^ c)) v c)
29	26, 28	ax-r2 35	. . . 4 (a v c) = ((a_|__|_ v (a_|_ ^ c)) v c)
30	18, 19, 29	le3tr2 133	. . 3 b_|__|_ =< ((a_|__|_ v (a_|_ ^ c)) v c)
31		lear 153	. . . 4 (b_|_ ^ c) =< c
32		leor 151	. . . 4 c =< ((a_|__|_ v (a_|_ ^ c)) v c)
33	31, 32	letr 129	. . 3 (b_|_ ^ c) =< ((a_|__|_ v (a_|_ ^ c)) v c)
34	30, 33	lel2or 162	. 2 (b_|__|_ v (b_|_ ^ c)) =< ((a_|__|_ v (a_|_ ^ c)) v c)
35		df-i1 43	. 2 (b_|_ ->1 c) = (b_|__|_ v (b_|_ ^ c))
36		df-i1 43	. . 3 (a_|_ ->1 c) = (a_|__|_ v (a_|_ ^ c))
37	36	ax-r5 37	. 2 ((a_|_ ->1 c) v c) = ((a_|__|_ v (a_|_ ^ c)) v c)
38	34, 35, 37	le3tr1 132	1 (b_|_ ->1 c) =< ((a_|_ ->1 c) v c)

Syntax hints:   =< wle 2  _|_wn 4   v wo 6   ^ wa 7   ->1 wi1 13

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