Theorem gomaex3lem5 918

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
gomaex3lem5	(((g ∪ h) ∩ (i ∪ j)) ∩ (((k ∪ m) ∩ (n ∪ u)) ∩ ((w ∪ x) ∩ (y ∪ z)))) ≤ (h ∪ i)

Proof of Theorem gomaex3lem5

Step	Hyp	Ref	Expression
1		gomaex3lem5.1	. . 3 a ≤ b⊥
2		gomaex3lem5.12	. . 3 g = a
3		gomaex3lem5.13	. . 3 h = b
4	1, 2, 3	gomaex3h1 902	. 2 g ≤ h⊥
5		gomaex3lem5.2	. . 3 b ≤ c⊥
6		gomaex3lem5.14	. . 3 i = c
7	5, 3, 6	gomaex3h2 903	. 2 h ≤ i⊥
8		gomaex3lem5.15	. . 3 j = (c ∪ d)⊥
9	6, 8	gomaex3h3 904	. 2 i ≤ j⊥
10		gomaex3lem5.11	. . 3 r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))
11		gomaex3lem5.16	. . 3 k = r
12	10, 8, 11	gomaex3h4 905	. 2 j ≤ k⊥
13		gomaex3lem5.17	. . 3 m = (p⊥ →1 q)
14	10, 11, 13	gomaex3h5 906	. 2 k ≤ m⊥
15		gomaex3lem5.18	. . 3 n = (p⊥ →1 q)⊥
16	13, 15	gomaex3h6 907	. 2 m ≤ n⊥
17		gomaex3lem5.19	. . 3 u = (p⊥ ∩ q)
18	15, 17	gomaex3h7 908	. 2 n ≤ u⊥
19		gomaex3lem5.20	. . 3 w = q⊥
20	17, 19	gomaex3h8 909	. 2 u ≤ w⊥
21		gomaex3lem5.21	. . 3 x = q
22	19, 21	gomaex3h9 910	. 2 w ≤ x⊥
23		gomaex3lem5.10	. . 3 q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥
24		gomaex3lem5.22	. . 3 y = (e ∪ f)⊥
25	23, 21, 24	gomaex3h10 911	. 2 x ≤ y⊥
26		gomaex3lem5.23	. . 3 z = f
27	24, 26	gomaex3h11 912	. 2 y ≤ z⊥
28		gomaex3lem5.6	. . 3 f ≤ a⊥
29	28, 2, 26	gomaex3h12 913	. 2 z ≤ g⊥
30		gomaex3lem5.8	. 2 (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)
31	4, 7, 9, 12, 14, 16, 18, 20, 22, 25, 27, 29, 30	go2n6 901	1 (((g ∪ h) ∩ (i ∪ j)) ∩ (((k ∪ m) ∩ (n ∪ u)) ∩ ((w ∪ x) ∩ (y ∪ z)))) ≤ (h ∪ i)

This proof depends on syntax axioms:   = wb 1   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   →₁ 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:  gomaex3lem6  919