Theorem oa4to4u2 974

Description: A weaker-looking "universal" proper 4-OA. (Contributed by NM, 29-Dec-1998.)

Hypotheses

Ref	Expression
oa4to4u.1	((e →1 d) ∩ (e ∪ (f ∩ (((e ∩ f) ∪ ((e →1 d) ∩ (f →1 d))) ∪ (((e ∩ g) ∪ ((e →1 d) ∩ (g →1 d))) ∩ ((f ∩ g) ∪ ((f →1 d) ∩ (g →1 d)))))))) ≤ (((e ∩ d) ∪ (f ∩ d)) ∪ (g ∩ d))
oa4to4u.2	e = (a⊥ →1 d)
oa4to4u3	f = (b⊥ →1 d)
oa4to4u.4	g = (c⊥ →1 d)

Assertion

Ref	Expression
oa4to4u2	((a →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))))) ≤ d

Proof of Theorem oa4to4u2

Step	Hyp	Ref	Expression
1		oa4to4u.1	. . 3 ((e →1 d) ∩ (e ∪ (f ∩ (((e ∩ f) ∪ ((e →1 d) ∩ (f →1 d))) ∪ (((e ∩ g) ∪ ((e →1 d) ∩ (g →1 d))) ∩ ((f ∩ g) ∪ ((f →1 d) ∩ (g →1 d)))))))) ≤ (((e ∩ d) ∪ (f ∩ d)) ∪ (g ∩ d))
2		oa4to4u.2	. . 3 e = (a⊥ →1 d)
3		oa4to4u3	. . 3 f = (b⊥ →1 d)
4		oa4to4u.4	. . 3 g = (c⊥ →1 d)
5	1, 2, 3, 4	oa4to4u 973	. 2 ((a →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))))) ≤ ((((a →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (b⊥ →1 d))) ∪ ((c →1 d) ∩ (c⊥ →1 d)))
6		u1lem8 776	. . . . 5 ((a →1 d) ∩ (a⊥ →1 d)) = ((a ∩ d) ∪ (a⊥ ∩ d))
7		lear 161	. . . . . 6 (a ∩ d) ≤ d
8		lear 161	. . . . . 6 (a⊥ ∩ d) ≤ d
9	7, 8	lel2or 170	. . . . 5 ((a ∩ d) ∪ (a⊥ ∩ d)) ≤ d
10	6, 9	bltr 138	. . . 4 ((a →1 d) ∩ (a⊥ →1 d)) ≤ d
11		u1lem8 776	. . . . 5 ((b →1 d) ∩ (b⊥ →1 d)) = ((b ∩ d) ∪ (b⊥ ∩ d))
12		lear 161	. . . . . 6 (b ∩ d) ≤ d
13		lear 161	. . . . . 6 (b⊥ ∩ d) ≤ d
14	12, 13	lel2or 170	. . . . 5 ((b ∩ d) ∪ (b⊥ ∩ d)) ≤ d
15	11, 14	bltr 138	. . . 4 ((b →1 d) ∩ (b⊥ →1 d)) ≤ d
16	10, 15	lel2or 170	. . 3 (((a →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (b⊥ →1 d))) ≤ d
17		u1lem8 776	. . . 4 ((c →1 d) ∩ (c⊥ →1 d)) = ((c ∩ d) ∪ (c⊥ ∩ d))
18		lear 161	. . . . 5 (c ∩ d) ≤ d
19		lear 161	. . . . 5 (c⊥ ∩ d) ≤ d
20	18, 19	lel2or 170	. . . 4 ((c ∩ d) ∪ (c⊥ ∩ d)) ≤ d
21	17, 20	bltr 138	. . 3 ((c →1 d) ∩ (c⊥ →1 d)) ≤ d
22	16, 21	lel2or 170	. 2 ((((a →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (b⊥ →1 d))) ∪ ((c →1 d) ∩ (c⊥ →1 d))) ≤ d
23	5, 22	letr 137	1 ((a →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))))) ≤ d

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

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

This theorem is used by:  4oa  1039