Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa4to4u GIF version

Theorem oa4to4u 973
 Description: A "universal" 4-OA. The hypotheses are the standard proper 4-OA and substitutions into it. (Contributed by NM, 28-Dec-1998.)
Hypotheses
Ref Expression
oa4to4u.1 ((e1 d) ∩ (e ∪ (f ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))))))) ≤ (((ed) ∪ (fd)) ∪ (gd))
oa4to4u.2 e = (a1 d)
oa4to4u3 f = (b1 d)
oa4to4u.4 g = (c1 d)
Assertion
Ref Expression
oa4to4u ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ ((((a1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (b1 d))) ∪ ((c1 d) ∩ (c1 d)))

Proof of Theorem oa4to4u
StepHypRef Expression
1 oa4to4u.1 . . 3 ((e1 d) ∩ (e ∪ (f ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))))))) ≤ (((ed) ∪ (fd)) ∪ (gd))
2 oa4to4u.2 . . . . 5 e = (a1 d)
32ud1lem0b 256 . . . 4 (e1 d) = ((a1 d) →1 d)
4 oa4to4u3 . . . . . 6 f = (b1 d)
52, 42an 79 . . . . . . . 8 (ef) = ((a1 d) ∩ (b1 d))
64ud1lem0b 256 . . . . . . . . 9 (f1 d) = ((b1 d) →1 d)
73, 62an 79 . . . . . . . 8 ((e1 d) ∩ (f1 d)) = (((a1 d) →1 d) ∩ ((b1 d) →1 d))
85, 72or 72 . . . . . . 7 ((ef) ∪ ((e1 d) ∩ (f1 d))) = (((a1 d) ∩ (b1 d)) ∪ (((a1 d) →1 d) ∩ ((b1 d) →1 d)))
9 oa4to4u.4 . . . . . . . . . 10 g = (c1 d)
102, 92an 79 . . . . . . . . 9 (eg) = ((a1 d) ∩ (c1 d))
119ud1lem0b 256 . . . . . . . . . 10 (g1 d) = ((c1 d) →1 d)
123, 112an 79 . . . . . . . . 9 ((e1 d) ∩ (g1 d)) = (((a1 d) →1 d) ∩ ((c1 d) →1 d))
1310, 122or 72 . . . . . . . 8 ((eg) ∪ ((e1 d) ∩ (g1 d))) = (((a1 d) ∩ (c1 d)) ∪ (((a1 d) →1 d) ∩ ((c1 d) →1 d)))
144, 92an 79 . . . . . . . . 9 (fg) = ((b1 d) ∩ (c1 d))
156, 112an 79 . . . . . . . . 9 ((f1 d) ∩ (g1 d)) = (((b1 d) →1 d) ∩ ((c1 d) →1 d))
1614, 152or 72 . . . . . . . 8 ((fg) ∪ ((f1 d) ∩ (g1 d))) = (((b1 d) ∩ (c1 d)) ∪ (((b1 d) →1 d) ∩ ((c1 d) →1 d)))
1713, 162an 79 . . . . . . 7 (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))) = ((((a1 d) ∩ (c1 d)) ∪ (((a1 d) →1 d) ∩ ((c1 d) →1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ (((b1 d) →1 d) ∩ ((c1 d) →1 d))))
188, 172or 72 . . . . . 6 (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d))))) = ((((a1 d) ∩ (b1 d)) ∪ (((a1 d) →1 d) ∩ ((b1 d) →1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ (((a1 d) →1 d) ∩ ((c1 d) →1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ (((b1 d) →1 d) ∩ ((c1 d) →1 d)))))
194, 182an 79 . . . . 5 (f ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))))) = ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ (((a1 d) →1 d) ∩ ((b1 d) →1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ (((a1 d) →1 d) ∩ ((c1 d) →1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ (((b1 d) →1 d) ∩ ((c1 d) →1 d))))))
202, 192or 72 . . . 4 (e ∪ (f ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d))))))) = ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ (((a1 d) →1 d) ∩ ((b1 d) →1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ (((a1 d) →1 d) ∩ ((c1 d) →1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ (((b1 d) →1 d) ∩ ((c1 d) →1 d)))))))
213, 202an 79 . . 3 ((e1 d) ∩ (e ∪ (f ∩ (((ef) ∪ ((e1 d) ∩ (f1 d))) ∪ (((eg) ∪ ((e1 d) ∩ (g1 d))) ∩ ((fg) ∪ ((f1 d) ∩ (g1 d)))))))) = (((a1 d) →1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ (((a1 d) →1 d) ∩ ((b1 d) →1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ (((a1 d) →1 d) ∩ ((c1 d) →1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ (((b1 d) →1 d) ∩ ((c1 d) →1 d))))))))
222ran 78 . . . . 5 (ed) = ((a1 d) ∩ d)
234ran 78 . . . . 5 (fd) = ((b1 d) ∩ d)
2422, 232or 72 . . . 4 ((ed) ∪ (fd)) = (((a1 d) ∩ d) ∪ ((b1 d) ∩ d))
259ran 78 . . . 4 (gd) = ((c1 d) ∩ d)
2624, 252or 72 . . 3 (((ed) ∪ (fd)) ∪ (gd)) = ((((a1 d) ∩ d) ∪ ((b1 d) ∩ d)) ∪ ((c1 d) ∩ d))
271, 21, 26le3tr2 141 . 2 (((a1 d) →1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ (((a1 d) →1 d) ∩ ((b1 d) →1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ (((a1 d) →1 d) ∩ ((c1 d) →1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ (((b1 d) →1 d) ∩ ((c1 d) →1 d)))))))) ≤ ((((a1 d) ∩ d) ∪ ((b1 d) ∩ d)) ∪ ((c1 d) ∩ d))
28 u1lem11 780 . . 3 ((a1 d) →1 d) = (a1 d)
29 ax-a2 31 . . . . . . 7 (((a1 d) ∩ (b1 d)) ∪ (((a1 d) →1 d) ∩ ((b1 d) →1 d))) = ((((a1 d) →1 d) ∩ ((b1 d) →1 d)) ∪ ((a1 d) ∩ (b1 d)))
30 u1lem11 780 . . . . . . . . 9 ((b1 d) →1 d) = (b1 d)
3128, 302an 79 . . . . . . . 8 (((a1 d) →1 d) ∩ ((b1 d) →1 d)) = ((a1 d) ∩ (b1 d))
3231ax-r5 38 . . . . . . 7 ((((a1 d) →1 d) ∩ ((b1 d) →1 d)) ∪ ((a1 d) ∩ (b1 d))) = (((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d)))
3329, 32ax-r2 36 . . . . . 6 (((a1 d) ∩ (b1 d)) ∪ (((a1 d) →1 d) ∩ ((b1 d) →1 d))) = (((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d)))
34 ax-a2 31 . . . . . . . 8 (((a1 d) ∩ (c1 d)) ∪ (((a1 d) →1 d) ∩ ((c1 d) →1 d))) = ((((a1 d) →1 d) ∩ ((c1 d) →1 d)) ∪ ((a1 d) ∩ (c1 d)))
35 u1lem11 780 . . . . . . . . . 10 ((c1 d) →1 d) = (c1 d)
3628, 352an 79 . . . . . . . . 9 (((a1 d) →1 d) ∩ ((c1 d) →1 d)) = ((a1 d) ∩ (c1 d))
3736ax-r5 38 . . . . . . . 8 ((((a1 d) →1 d) ∩ ((c1 d) →1 d)) ∪ ((a1 d) ∩ (c1 d))) = (((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d)))
3834, 37ax-r2 36 . . . . . . 7 (((a1 d) ∩ (c1 d)) ∪ (((a1 d) →1 d) ∩ ((c1 d) →1 d))) = (((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d)))
39 ax-a2 31 . . . . . . . 8 (((b1 d) ∩ (c1 d)) ∪ (((b1 d) →1 d) ∩ ((c1 d) →1 d))) = ((((b1 d) →1 d) ∩ ((c1 d) →1 d)) ∪ ((b1 d) ∩ (c1 d)))
4030, 352an 79 . . . . . . . . 9 (((b1 d) →1 d) ∩ ((c1 d) →1 d)) = ((b1 d) ∩ (c1 d))
4140ax-r5 38 . . . . . . . 8 ((((b1 d) →1 d) ∩ ((c1 d) →1 d)) ∪ ((b1 d) ∩ (c1 d))) = (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))
4239, 41ax-r2 36 . . . . . . 7 (((b1 d) ∩ (c1 d)) ∪ (((b1 d) →1 d) ∩ ((c1 d) →1 d))) = (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))
4338, 422an 79 . . . . . 6 ((((a1 d) ∩ (c1 d)) ∪ (((a1 d) →1 d) ∩ ((c1 d) →1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ (((b1 d) →1 d) ∩ ((c1 d) →1 d)))) = ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))
4433, 432or 72 . . . . 5 ((((a1 d) ∩ (b1 d)) ∪ (((a1 d) →1 d) ∩ ((b1 d) →1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ (((a1 d) →1 d) ∩ ((c1 d) →1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ (((b1 d) →1 d) ∩ ((c1 d) →1 d))))) = ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))
4544lan 77 . . . 4 ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ (((a1 d) →1 d) ∩ ((b1 d) →1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ (((a1 d) →1 d) ∩ ((c1 d) →1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ (((b1 d) →1 d) ∩ ((c1 d) →1 d)))))) = ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))))
4645lor 70 . . 3 ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ (((a1 d) →1 d) ∩ ((b1 d) →1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ (((a1 d) →1 d) ∩ ((c1 d) →1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ (((b1 d) →1 d) ∩ ((c1 d) →1 d))))))) = ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))
4728, 462an 79 . 2 (((a1 d) →1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ (((a1 d) →1 d) ∩ ((b1 d) →1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ (((a1 d) →1 d) ∩ ((c1 d) →1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ (((b1 d) →1 d) ∩ ((c1 d) →1 d)))))))) = ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d))))))))
48 u1lemab 610 . . . . 5 ((a1 d) ∩ d) = ((ad) ∪ (a d))
49 u1lem8 776 . . . . . . 7 ((a1 d) ∩ (a1 d)) = ((ad) ∪ (ad))
50 ax-a2 31 . . . . . . 7 ((ad) ∪ (ad)) = ((ad) ∪ (ad))
51 ax-a1 30 . . . . . . . . 9 a = a
5251ran 78 . . . . . . . 8 (ad) = (a d)
5352lor 70 . . . . . . 7 ((ad) ∪ (ad)) = ((ad) ∪ (a d))
5449, 50, 533tr 65 . . . . . 6 ((a1 d) ∩ (a1 d)) = ((ad) ∪ (a d))
5554ax-r1 35 . . . . 5 ((ad) ∪ (a d)) = ((a1 d) ∩ (a1 d))
5648, 55ax-r2 36 . . . 4 ((a1 d) ∩ d) = ((a1 d) ∩ (a1 d))
57 u1lemab 610 . . . . 5 ((b1 d) ∩ d) = ((bd) ∪ (b d))
58 u1lem8 776 . . . . . . 7 ((b1 d) ∩ (b1 d)) = ((bd) ∪ (bd))
59 ax-a2 31 . . . . . . 7 ((bd) ∪ (bd)) = ((bd) ∪ (bd))
60 ax-a1 30 . . . . . . . . 9 b = b
6160ran 78 . . . . . . . 8 (bd) = (b d)
6261lor 70 . . . . . . 7 ((bd) ∪ (bd)) = ((bd) ∪ (b d))
6358, 59, 623tr 65 . . . . . 6 ((b1 d) ∩ (b1 d)) = ((bd) ∪ (b d))
6463ax-r1 35 . . . . 5 ((bd) ∪ (b d)) = ((b1 d) ∩ (b1 d))
6557, 64ax-r2 36 . . . 4 ((b1 d) ∩ d) = ((b1 d) ∩ (b1 d))
6656, 652or 72 . . 3 (((a1 d) ∩ d) ∪ ((b1 d) ∩ d)) = (((a1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (b1 d)))
67 u1lemab 610 . . . 4 ((c1 d) ∩ d) = ((cd) ∪ (c d))
68 u1lem8 776 . . . . . 6 ((c1 d) ∩ (c1 d)) = ((cd) ∪ (cd))
69 ax-a2 31 . . . . . 6 ((cd) ∪ (cd)) = ((cd) ∪ (cd))
70 ax-a1 30 . . . . . . . 8 c = c
7170ran 78 . . . . . . 7 (cd) = (c d)
7271lor 70 . . . . . 6 ((cd) ∪ (cd)) = ((cd) ∪ (c d))
7368, 69, 723tr 65 . . . . 5 ((c1 d) ∩ (c1 d)) = ((cd) ∪ (c d))
7473ax-r1 35 . . . 4 ((cd) ∪ (c d)) = ((c1 d) ∩ (c1 d))
7567, 74ax-r2 36 . . 3 ((c1 d) ∩ d) = ((c1 d) ∩ (c1 d))
7666, 752or 72 . 2 ((((a1 d) ∩ d) ∪ ((b1 d) ∩ d)) ∪ ((c1 d) ∩ d)) = ((((a1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (b1 d))) ∪ ((c1 d) ∩ (c1 d)))
7727, 47, 76le3tr2 141 1 ((a1 d) ∩ ((a1 d) ∪ ((b1 d) ∩ ((((a1 d) ∩ (b1 d)) ∪ ((a1 d) ∩ (b1 d))) ∪ ((((a1 d) ∩ (c1 d)) ∪ ((a1 d) ∩ (c1 d))) ∩ (((b1 d) ∩ (c1 d)) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ ((((a1 d) ∩ (a1 d)) ∪ ((b1 d) ∩ (b1 d))) ∪ ((c1 d) ∩ (c1 d)))
 Colors of variables: term Syntax hints:   = wb 1   ≤ wle 2  ⊥ wn 4   ∪ wo 6   ∩ wa 7   →1 wi1 12 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-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133 This theorem is referenced by:  oa4to4u2  974
 Copyright terms: Public domain W3C validator