Theorem gomaex3lem6 899

Description: Lemma for Godowski 6-var -> Mayet Example 3.

Hypotheses

Ref	Expression
gomaex3lem5.1	a =< b_|_
gomaex3lem5.2	b =< c_|_
gomaex3lem5.3	c =< d_|_
gomaex3lem5.5	e =< f_|_
gomaex3lem5.6	f =< a_|_
gomaex3lem5.8	(((i ->2 g) ^ (g ->2 y)) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i)))) =< (g ->2 i)
gomaex3lem5.9	p = ((a v b) ->1 (d v e)_|_)_|_
gomaex3lem5.10	q = ((e v f) ->1 (b v c)_|_)_|_
gomaex3lem5.11	r = ((p_|_ ->1 q)_|_ ^ (c v d))
gomaex3lem5.12	g = a
gomaex3lem5.13	h = b
gomaex3lem5.14	i = c
gomaex3lem5.15	j = (c v d)_|_
gomaex3lem5.16	k = r
gomaex3lem5.17	m = (p_|_ ->1 q)
gomaex3lem5.18	n = (p_|_ ->1 q)_|_
gomaex3lem5.19	u = (p_|_ ^ q)
gomaex3lem5.20	w = q_|_
gomaex3lem5.21	x = q
gomaex3lem5.22	y = (e v f)_|_
gomaex3lem5.23	z = f

Assertion

Ref	Expression
gomaex3lem6	(((a v b) ^ (c v (c v d)_|_)) ^ (((r v (p_|_ ->1 q)) ^ ((p_|_ ->1 q)_|_ v (p_|_ ^ q))) ^ ((q_|_ v q) ^ ((e v f)_|_ v f)))) =< (b v c)

Proof of Theorem gomaex3lem6

Step	Hyp	Ref	Expression
1		gomaex3lem5.1	. . 3 a =< b_|_
2		gomaex3lem5.2	. . 3 b =< c_|_
3		gomaex3lem5.3	. . 3 c =< d_|_
4		gomaex3lem5.5	. . 3 e =< f_|_
5		gomaex3lem5.6	. . 3 f =< a_|_
6		gomaex3lem5.8	. . 3 (((i ->2 g) ^ (g ->2 y)) ^ (((y ->2 w) ^ (w ->2 n)) ^ ((n ->2 k) ^ (k ->2 i)))) =< (g ->2 i)
7		gomaex3lem5.9	. . 3 p = ((a v b) ->1 (d v e)_|_)_|_
8		gomaex3lem5.10	. . 3 q = ((e v f) ->1 (b v c)_|_)_|_
9		gomaex3lem5.11	. . 3 r = ((p_|_ ->1 q)_|_ ^ (c v d))
10		gomaex3lem5.12	. . 3 g = a
11		gomaex3lem5.13	. . 3 h = b
12		gomaex3lem5.14	. . 3 i = c
13		gomaex3lem5.15	. . 3 j = (c v d)_|_
14		gomaex3lem5.16	. . 3 k = r
15		gomaex3lem5.17	. . 3 m = (p_|_ ->1 q)
16		gomaex3lem5.18	. . 3 n = (p_|_ ->1 q)_|_
17		gomaex3lem5.19	. . 3 u = (p_|_ ^ q)
18		gomaex3lem5.20	. . 3 w = q_|_
19		gomaex3lem5.21	. . 3 x = q
20		gomaex3lem5.22	. . 3 y = (e v f)_|_
21		gomaex3lem5.23	. . 3 z = f
22	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21	gomaex3lem5 898	. 2 (((g v h) ^ (i v j)) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))) =< (h v i)
23	10, 11	2or 67	. . . 4 (g v h) = (a v b)
24	12, 13	2or 67	. . . 4 (i v j) = (c v (c v d)_|_)
25	23, 24	2an 72	. . 3 ((g v h) ^ (i v j)) = ((a v b) ^ (c v (c v d)_|_))
26	14, 15	2or 67	. . . . 5 (k v m) = (r v (p_|_ ->1 q))
27	16, 17	2or 67	. . . . 5 (n v u) = ((p_|_ ->1 q)_|_ v (p_|_ ^ q))
28	26, 27	2an 72	. . . 4 ((k v m) ^ (n v u)) = ((r v (p_|_ ->1 q)) ^ ((p_|_ ->1 q)_|_ v (p_|_ ^ q)))
29	18, 19	2or 67	. . . . 5 (w v x) = (q_|_ v q)
30	20, 21	2or 67	. . . . 5 (y v z) = ((e v f)_|_ v f)
31	29, 30	2an 72	. . . 4 ((w v x) ^ (y v z)) = ((q_|_ v q) ^ ((e v f)_|_ v f))
32	28, 31	2an 72	. . 3 (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z))) = (((r v (p_|_ ->1 q)) ^ ((p_|_ ->1 q)_|_ v (p_|_ ^ q))) ^ ((q_|_ v q) ^ ((e v f)_|_ v f)))
33	25, 32	2an 72	. 2 (((g v h) ^ (i v j)) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))) = (((a v b) ^ (c v (c v d)_|_)) ^ (((r v (p_|_ ->1 q)) ^ ((p_|_ ->1 q)_|_ v (p_|_ ^ q))) ^ ((q_|_ v q) ^ ((e v f)_|_ v f))))
34	11, 12	2or 67	. 2 (h v i) = (b v c)
35	22, 33, 34	le3tr2 133	1 (((a v b) ^ (c v (c v d)_|_)) ^ (((r v (p_|_ ->1 q)) ^ ((p_|_ ->1 q)_|_ v (p_|_ ^ q))) ^ ((q_|_ v q) ^ ((e v f)_|_ v f)))) =< (b v c)

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

This theorem is referenced by:  gomaex3lem7 900

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

metamath.org