Theorem oa4to4u 953

Description: A "universal" 4-OA. The hypotheses are the standard proper 4-OA and substitutions into it.

Hypotheses

Ref	Expression
oa4to4u.1	((e ->1 d) ^ (e v (f ^ (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->1 d)))))))) =< (((e ^ d) v (f ^ d)) v (g ^ d))
oa4to4u.2	e = (a_|_ ->1 d)
oa4to4u3	f = (b_|_ ->1 d)
oa4to4u.4	g = (c_|_ ->1 d)

Assertion

Ref	Expression
oa4to4u	((a ->1 d) ^ ((a_|_ ->1 d) v ((b_|_ ->1 d) ^ ((((a ->1 d) ^ (b ->1 d)) v ((a_|_ ->1 d) ^ (b_|_ ->1 d))) v ((((a ->1 d) ^ (c ->1 d)) v ((a_|_ ->1 d) ^ (c_|_ ->1 d))) ^ (((b ->1 d) ^ (c ->1 d)) v ((b_|_ ->1 d) ^ (c_|_ ->1 d)))))))) =< ((((a ->1 d) ^ (a_|_ ->1 d)) v ((b ->1 d) ^ (b_|_ ->1 d))) v ((c ->1 d) ^ (c_|_ ->1 d)))

Proof of Theorem oa4to4u

Step	Hyp	Ref	Expression
1		oa4to4u.1	. . 3 ((e ->1 d) ^ (e v (f ^ (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->1 d)))))))) =< (((e ^ d) v (f ^ d)) v (g ^ d))
2		oa4to4u.2	. . . . 5 e = (a_|_ ->1 d)
3	2	ud1lem0b 248	. . . 4 (e ->1 d) = ((a_|_ ->1 d) ->1 d)
4		oa4to4u3	. . . . . 6 f = (b_|_ ->1 d)
5	2, 4	2an 72	. . . . . . . 8 (e ^ f) = ((a_|_ ->1 d) ^ (b_|_ ->1 d))
6	4	ud1lem0b 248	. . . . . . . . 9 (f ->1 d) = ((b_|_ ->1 d) ->1 d)
7	3, 6	2an 72	. . . . . . . 8 ((e ->1 d) ^ (f ->1 d)) = (((a_|_ ->1 d) ->1 d) ^ ((b_|_ ->1 d) ->1 d))
8	5, 7	2or 67	. . . . . . 7 ((e ^ f) v ((e ->1 d) ^ (f ->1 d))) = (((a_|_ ->1 d) ^ (b_|_ ->1 d)) v (((a_|_ ->1 d) ->1 d) ^ ((b_|_ ->1 d) ->1 d)))
9		oa4to4u.4	. . . . . . . . . 10 g = (c_|_ ->1 d)
10	2, 9	2an 72	. . . . . . . . 9 (e ^ g) = ((a_|_ ->1 d) ^ (c_|_ ->1 d))
11	9	ud1lem0b 248	. . . . . . . . . 10 (g ->1 d) = ((c_|_ ->1 d) ->1 d)
12	3, 11	2an 72	. . . . . . . . 9 ((e ->1 d) ^ (g ->1 d)) = (((a_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d))
13	10, 12	2or 67	. . . . . . . 8 ((e ^ g) v ((e ->1 d) ^ (g ->1 d))) = (((a_|_ ->1 d) ^ (c_|_ ->1 d)) v (((a_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d)))
14	4, 9	2an 72	. . . . . . . . 9 (f ^ g) = ((b_|_ ->1 d) ^ (c_|_ ->1 d))
15	6, 11	2an 72	. . . . . . . . 9 ((f ->1 d) ^ (g ->1 d)) = (((b_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d))
16	14, 15	2or 67	. . . . . . . 8 ((f ^ g) v ((f ->1 d) ^ (g ->1 d))) = (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v (((b_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d)))
17	13, 16	2an 72	. . . . . . 7 (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->1 d)))) = ((((a_|_ ->1 d) ^ (c_|_ ->1 d)) v (((a_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d))) ^ (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v (((b_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d))))
18	8, 17	2or 67	. . . . . 6 (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->1 d))))) = ((((a_|_ ->1 d) ^ (b_|_ ->1 d)) v (((a_|_ ->1 d) ->1 d) ^ ((b_|_ ->1 d) ->1 d))) v ((((a_|_ ->1 d) ^ (c_|_ ->1 d)) v (((a_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d))) ^ (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v (((b_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d)))))
19	4, 18	2an 72	. . . . 5 (f ^ (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->1 d)))))) = ((b_|_ ->1 d) ^ ((((a_|_ ->1 d) ^ (b_|_ ->1 d)) v (((a_|_ ->1 d) ->1 d) ^ ((b_|_ ->1 d) ->1 d))) v ((((a_|_ ->1 d) ^ (c_|_ ->1 d)) v (((a_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d))) ^ (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v (((b_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d))))))
20	2, 19	2or 67	. . . 4 (e v (f ^ (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->1 d))))))) = ((a_|_ ->1 d) v ((b_|_ ->1 d) ^ ((((a_|_ ->1 d) ^ (b_|_ ->1 d)) v (((a_|_ ->1 d) ->1 d) ^ ((b_|_ ->1 d) ->1 d))) v ((((a_|_ ->1 d) ^ (c_|_ ->1 d)) v (((a_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d))) ^ (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v (((b_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d)))))))
21	3, 20	2an 72	. . 3 ((e ->1 d) ^ (e v (f ^ (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->1 d)))))))) = (((a_|_ ->1 d) ->1 d) ^ ((a_|_ ->1 d) v ((b_|_ ->1 d) ^ ((((a_|_ ->1 d) ^ (b_|_ ->1 d)) v (((a_|_ ->1 d) ->1 d) ^ ((b_|_ ->1 d) ->1 d))) v ((((a_|_ ->1 d) ^ (c_|_ ->1 d)) v (((a_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d))) ^ (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v (((b_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d))))))))
22	2	ran 71	. . . . 5 (e ^ d) = ((a_|_ ->1 d) ^ d)
23	4	ran 71	. . . . 5 (f ^ d) = ((b_|_ ->1 d) ^ d)
24	22, 23	2or 67	. . . 4 ((e ^ d) v (f ^ d)) = (((a_|_ ->1 d) ^ d) v ((b_|_ ->1 d) ^ d))
25	9	ran 71	. . . 4 (g ^ d) = ((c_|_ ->1 d) ^ d)
26	24, 25	2or 67	. . 3 (((e ^ d) v (f ^ d)) v (g ^ d)) = ((((a_|_ ->1 d) ^ d) v ((b_|_ ->1 d) ^ d)) v ((c_|_ ->1 d) ^ d))
27	1, 21, 26	le3tr2 133	. 2 (((a_|_ ->1 d) ->1 d) ^ ((a_|_ ->1 d) v ((b_|_ ->1 d) ^ ((((a_|_ ->1 d) ^ (b_|_ ->1 d)) v (((a_|_ ->1 d) ->1 d) ^ ((b_|_ ->1 d) ->1 d))) v ((((a_|_ ->1 d) ^ (c_|_ ->1 d)) v (((a_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d))) ^ (((b_|_ ->1 d) ^ (c_|_ ->1 d)) v (((b_|_ ->1 d) ->1 d) ^ ((c_|_ ->1 d) ->1 d)))))))) =< ((((a_|_ ->1 d) ^ d) v ((b_|_ ->1 d) ^ d)) v ((c_|_ ->1 d) ^ d)