Theorem go2n6 901

Description: 12-variable Godowski equation derived from 6-variable one. The last hypothesis is the 6-variable Godowski equation. (Contributed by NM, 29-Nov-1999.)

Hypotheses

Ref	Expression
go2n6.1	g ≤ h⊥
go2n6.2	h ≤ i⊥
go2n6.3	i ≤ j⊥
go2n6.4	j ≤ k⊥
go2n6.5	k ≤ m⊥
go2n6.6	m ≤ n⊥
go2n6.7	n ≤ u⊥
go2n6.8	u ≤ w⊥
go2n6.9	w ≤ x⊥
go2n6.10	x ≤ y⊥
go2n6.11	y ≤ z⊥
go2n6.12	z ≤ g⊥
go2n6.13	(((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)

Assertion

Ref	Expression
go2n6	(((g ∪ h) ∩ (i ∪ j)) ∩ (((k ∪ m) ∩ (n ∪ u)) ∩ ((w ∪ x) ∩ (y ∪ z)))) ≤ (h ∪ i)

Proof of Theorem go2n6

Step	Hyp	Ref	Expression
1		anass 76	. . . . . . . . . 10 (((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j))) = ((w ∪ x) ∩ ((n ∪ u) ∩ ((k ∪ m) ∩ (i ∪ j))))
2		ancom 74	. . . . . . . . . . . . 13 ((k ∪ m) ∩ (i ∪ j)) = ((i ∪ j) ∩ (k ∪ m))
3	2	lan 77	. . . . . . . . . . . 12 ((n ∪ u) ∩ ((k ∪ m) ∩ (i ∪ j))) = ((n ∪ u) ∩ ((i ∪ j) ∩ (k ∪ m)))
4		ancom 74	. . . . . . . . . . . 12 ((n ∪ u) ∩ ((i ∪ j) ∩ (k ∪ m))) = (((i ∪ j) ∩ (k ∪ m)) ∩ (n ∪ u))
5		anass 76	. . . . . . . . . . . 12 (((i ∪ j) ∩ (k ∪ m)) ∩ (n ∪ u)) = ((i ∪ j) ∩ ((k ∪ m) ∩ (n ∪ u)))
6	3, 4, 5	3tr 65	. . . . . . . . . . 11 ((n ∪ u) ∩ ((k ∪ m) ∩ (i ∪ j))) = ((i ∪ j) ∩ ((k ∪ m) ∩ (n ∪ u)))
7	6	lan 77	. . . . . . . . . 10 ((w ∪ x) ∩ ((n ∪ u) ∩ ((k ∪ m) ∩ (i ∪ j)))) = ((w ∪ x) ∩ ((i ∪ j) ∩ ((k ∪ m) ∩ (n ∪ u))))
8		ancom 74	. . . . . . . . . 10 ((w ∪ x) ∩ ((i ∪ j) ∩ ((k ∪ m) ∩ (n ∪ u)))) = (((i ∪ j) ∩ ((k ∪ m) ∩ (n ∪ u))) ∩ (w ∪ x))
9	1, 7, 8	3tr 65	. . . . . . . . 9 (((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j))) = (((i ∪ j) ∩ ((k ∪ m) ∩ (n ∪ u))) ∩ (w ∪ x))
10	9	ran 78	. . . . . . . 8 ((((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j))) ∩ (y ∪ z)) = ((((i ∪ j) ∩ ((k ∪ m) ∩ (n ∪ u))) ∩ (w ∪ x)) ∩ (y ∪ z))
11		anass 76	. . . . . . . 8 ((((i ∪ j) ∩ ((k ∪ m) ∩ (n ∪ u))) ∩ (w ∪ x)) ∩ (y ∪ z)) = (((i ∪ j) ∩ ((k ∪ m) ∩ (n ∪ u))) ∩ ((w ∪ x) ∩ (y ∪ z)))
12	10, 11	ax-r2 36	. . . . . . 7 ((((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j))) ∩ (y ∪ z)) = (((i ∪ j) ∩ ((k ∪ m) ∩ (n ∪ u))) ∩ ((w ∪ x) ∩ (y ∪ z)))
13	12	ax-r1 35	. . . . . 6 (((i ∪ j) ∩ ((k ∪ m) ∩ (n ∪ u))) ∩ ((w ∪ x) ∩ (y ∪ z))) = ((((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j))) ∩ (y ∪ z))
14		anass 76	. . . . . 6 (((i ∪ j) ∩ ((k ∪ m) ∩ (n ∪ u))) ∩ ((w ∪ x) ∩ (y ∪ z))) = ((i ∪ j) ∩ (((k ∪ m) ∩ (n ∪ u)) ∩ ((w ∪ x) ∩ (y ∪ z))))
15		ancom 74	. . . . . 6 ((((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j))) ∩ (y ∪ z)) = ((y ∪ z) ∩ (((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j))))
16	13, 14, 15	3tr2 64	. . . . 5 ((i ∪ j) ∩ (((k ∪ m) ∩ (n ∪ u)) ∩ ((w ∪ x) ∩ (y ∪ z)))) = ((y ∪ z) ∩ (((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j))))
17	16	lan 77	. . . 4 ((g ∪ h) ∩ ((i ∪ j) ∩ (((k ∪ m) ∩ (n ∪ u)) ∩ ((w ∪ x) ∩ (y ∪ z))))) = ((g ∪ h) ∩ ((y ∪ z) ∩ (((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j)))))
18		anass 76	. . . 4 (((g ∪ h) ∩ (i ∪ j)) ∩ (((k ∪ m) ∩ (n ∪ u)) ∩ ((w ∪ x) ∩ (y ∪ z)))) = ((g ∪ h) ∩ ((i ∪ j) ∩ (((k ∪ m) ∩ (n ∪ u)) ∩ ((w ∪ x) ∩ (y ∪ z)))))
19		anass 76	. . . 4 (((g ∪ h) ∩ (y ∪ z)) ∩ (((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j)))) = ((g ∪ h) ∩ ((y ∪ z) ∩ (((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j)))))
20	17, 18, 19	3tr1 63	. . 3 (((g ∪ h) ∩ (i ∪ j)) ∩ (((k ∪ m) ∩ (n ∪ u)) ∩ ((w ∪ x) ∩ (y ∪ z)))) = (((g ∪ h) ∩ (y ∪ z)) ∩ (((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j))))
21	20, 19	ax-r2 36	. 2 (((g ∪ h) ∩ (i ∪ j)) ∩ (((k ∪ m) ∩ (n ∪ u)) ∩ ((w ∪ x) ∩ (y ∪ z)))) = ((g ∪ h) ∩ ((y ∪ z) ∩ (((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j)))))
22		go2n6.1	. . 3 g ≤ h⊥
23		go2n6.2	. . 3 h ≤ i⊥
24		anass 76	. . . . 5 (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) = ((i →2 g) ∩ ((g →2 y) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))))
25	24	ax-r1 35	. . . 4 ((i →2 g) ∩ ((g →2 y) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i))))) = (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i))))
26		go2n6.13	. . . 4 (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)
27	25, 26	bltr 138	. . 3 ((i →2 g) ∩ ((g →2 y) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i))))) ≤ (g →2 i)
28		go2n6.11	. . . . 5 y ≤ z⊥
29		go2n6.12	. . . . 5 z ≤ g⊥
30	28, 29	govar2 897	. . . 4 (y ∪ z) ≤ (g →2 y)
31		go2n6.9	. . . . . . 7 w ≤ x⊥
32		go2n6.10	. . . . . . 7 x ≤ y⊥
33	31, 32	govar2 897	. . . . . 6 (w ∪ x) ≤ (y →2 w)
34		go2n6.7	. . . . . . 7 n ≤ u⊥
35		go2n6.8	. . . . . . 7 u ≤ w⊥
36	34, 35	govar2 897	. . . . . 6 (n ∪ u) ≤ (w →2 n)
37	33, 36	le2an 169	. . . . 5 ((w ∪ x) ∩ (n ∪ u)) ≤ ((y →2 w) ∩ (w →2 n))
38		go2n6.5	. . . . . . 7 k ≤ m⊥
39		go2n6.6	. . . . . . 7 m ≤ n⊥
40	38, 39	govar2 897	. . . . . 6 (k ∪ m) ≤ (n →2 k)
41		go2n6.3	. . . . . . 7 i ≤ j⊥
42		go2n6.4	. . . . . . 7 j ≤ k⊥
43	41, 42	govar2 897	. . . . . 6 (i ∪ j) ≤ (k →2 i)
44	40, 43	le2an 169	. . . . 5 ((k ∪ m) ∩ (i ∪ j)) ≤ ((n →2 k) ∩ (k →2 i))
45	37, 44	le2an 169	. . . 4 (((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j))) ≤ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))
46	30, 45	le2an 169	. . 3 ((y ∪ z) ∩ (((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j)))) ≤ ((g →2 y) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i))))
47	22, 23, 27, 46	gon2n 898	. 2 ((g ∪ h) ∩ ((y ∪ z) ∩ (((w ∪ x) ∩ (n ∪ u)) ∩ ((k ∪ m) ∩ (i ∪ j))))) ≤ (h ∪ i)
48	21, 47	bltr 138	1 (((g ∪ h) ∩ (i ∪ j)) ∩ (((k ∪ m) ∩ (n ∪ u)) ∩ ((w ∪ x) ∩ (y ∪ z)))) ≤ (h ∪ i)

Syntax hints:   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   →₂ wi2 13

This theorem was proved from 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 theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  gomaex3lem5  918