Theorem gomaex3lem7 920

Description: Lemma for Godowski 6-var -> Mayet Example 3. (Contributed by NM, 29-Nov-1999.)

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 ∪ b) →1 (d ∪ e)⊥ )⊥
gomaex3lem5.10	q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥
gomaex3lem5.11	r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))
gomaex3lem5.12	g = a
gomaex3lem5.13	h = b
gomaex3lem5.14	i = c
gomaex3lem5.15	j = (c ∪ 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 ∪ f)⊥
gomaex3lem5.23	z = f

Assertion

Ref	Expression
gomaex3lem7	(((a ∪ b) ∩ d⊥ ) ∩ (((r ∪ (p⊥ →1 q)) ∩ p⊥ ) ∩ e⊥ )) ≤ (b ∪ c)

Proof of Theorem gomaex3lem7

Step	Hyp	Ref	Expression
1		gomaex3lem5.3	. . . . . 6 c ≤ d⊥
2	1	gomaex3lem1 914	. . . . 5 (c ∪ (c ∪ d)⊥ ) = d⊥
3	2	lan 77	. . . 4 ((a ∪ b) ∩ (c ∪ (c ∪ d)⊥ )) = ((a ∪ b) ∩ d⊥ )
4		gomaex3lem3 916	. . . . . 6 ((p⊥ →1 q)⊥ ∪ (p⊥ ∩ q)) = p⊥
5	4	lan 77	. . . . 5 ((r ∪ (p⊥ →1 q)) ∩ ((p⊥ →1 q)⊥ ∪ (p⊥ ∩ q))) = ((r ∪ (p⊥ →1 q)) ∩ p⊥ )
6		ancom 74	. . . . . 6 ((q⊥ ∪ q) ∩ ((e ∪ f)⊥ ∪ f)) = (((e ∪ f)⊥ ∪ f) ∩ (q⊥ ∪ q))
7		gomaex3lem5.5	. . . . . . . 8 e ≤ f⊥
8	7	gomaex3lem2 915	. . . . . . 7 ((e ∪ f)⊥ ∪ f) = e⊥
9		ax-a2 31	. . . . . . . 8 (q⊥ ∪ q) = (q ∪ q⊥ )
10		df-t 41	. . . . . . . . 9 1 = (q ∪ q⊥ )
11	10	ax-r1 35	. . . . . . . 8 (q ∪ q⊥ ) = 1
12	9, 11	ax-r2 36	. . . . . . 7 (q⊥ ∪ q) = 1
13	8, 12	2an 79	. . . . . 6 (((e ∪ f)⊥ ∪ f) ∩ (q⊥ ∪ q)) = (e⊥ ∩ 1)
14		an1 106	. . . . . 6 (e⊥ ∩ 1) = e⊥
15	6, 13, 14	3tr 65	. . . . 5 ((q⊥ ∪ q) ∩ ((e ∪ f)⊥ ∪ f)) = e⊥
16	5, 15	2an 79	. . . 4 (((r ∪ (p⊥ →1 q)) ∩ ((p⊥ →1 q)⊥ ∪ (p⊥ ∩ q))) ∩ ((q⊥ ∪ q) ∩ ((e ∪ f)⊥ ∪ f))) = (((r ∪ (p⊥ →1 q)) ∩ p⊥ ) ∩ e⊥ )
17	3, 16	2an 79	. . 3 (((a ∪ b) ∩ (c ∪ (c ∪ d)⊥ )) ∩ (((r ∪ (p⊥ →1 q)) ∩ ((p⊥ →1 q)⊥ ∪ (p⊥ ∩ q))) ∩ ((q⊥ ∪ q) ∩ ((e ∪ f)⊥ ∪ f)))) = (((a ∪ b) ∩ d⊥ ) ∩ (((r ∪ (p⊥ →1 q)) ∩ p⊥ ) ∩ e⊥ ))
18	17	ax-r1 35	. 2 (((a ∪ b) ∩ d⊥ ) ∩ (((r ∪ (p⊥ →1 q)) ∩ p⊥ ) ∩ e⊥ )) = (((a ∪ b) ∩ (c ∪ (c ∪ d)⊥ )) ∩ (((r ∪ (p⊥ →1 q)) ∩ ((p⊥ →1 q)⊥ ∪ (p⊥ ∩ q))) ∩ ((q⊥ ∪ q) ∩ ((e ∪ f)⊥ ∪ f))))
19		gomaex3lem5.1	. . 3 a ≤ b⊥
20		gomaex3lem5.2	. . 3 b ≤ c⊥
21		gomaex3lem5.6	. . 3 f ≤ a⊥
22		gomaex3lem5.8	. . 3 (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)
23		gomaex3lem5.9	. . 3 p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥
24		gomaex3lem5.10	. . 3 q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥
25		gomaex3lem5.11	. . 3 r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))
26		gomaex3lem5.12	. . 3 g = a
27		gomaex3lem5.13	. . 3 h = b
28		gomaex3lem5.14	. . 3 i = c
29		gomaex3lem5.15	. . 3 j = (c ∪ d)⊥
30		gomaex3lem5.16	. . 3 k = r
31		gomaex3lem5.17	. . 3 m = (p⊥ →1 q)
32		gomaex3lem5.18	. . 3 n = (p⊥ →1 q)⊥
33		gomaex3lem5.19	. . 3 u = (p⊥ ∩ q)
34		gomaex3lem5.20	. . 3 w = q⊥
35		gomaex3lem5.21	. . 3 x = q
36		gomaex3lem5.22	. . 3 y = (e ∪ f)⊥
37		gomaex3lem5.23	. . 3 z = f
38	19, 20, 1, 7, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37	gomaex3lem6 919	. 2 (((a ∪ b) ∩ (c ∪ (c ∪ d)⊥ )) ∩ (((r ∪ (p⊥ →1 q)) ∩ ((p⊥ →1 q)⊥ ∪ (p⊥ ∩ q))) ∩ ((q⊥ ∪ q) ∩ ((e ∪ f)⊥ ∪ f)))) ≤ (b ∪ c)
39	18, 38	bltr 138	1 (((a ∪ b) ∩ d⊥ ) ∩ (((r ∪ (p⊥ →1 q)) ∩ p⊥ ) ∩ e⊥ )) ≤ (b ∪ c)

This proof depends on syntax axioms:   = wb 1   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   →₁ wi1 12   →₂ wi2 13

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-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by:  gomaex3lem8  921