Theorem ud3lem3 576

Description: Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)

Assertion

Ref	Expression
ud3lem3	((a →3 b) →3 (a ∪ b)) = (a ∪ b)

Proof of Theorem ud3lem3

Step	Hyp	Ref	Expression
1		df-i3 46	. 2 ((a →3 b) →3 (a ∪ b)) = ((((a →3 b)⊥ ∩ (a ∪ b)) ∪ ((a →3 b)⊥ ∩ (a ∪ b)⊥ )) ∪ ((a →3 b) ∩ ((a →3 b)⊥ ∪ (a ∪ b))))
2		ud3lem3a 572	. . . . . . 7 ((a →3 b)⊥ ∩ (a ∪ b)) = (a →3 b)⊥
3		ud3lem0c 279	. . . . . . 7 (a →3 b)⊥ = (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ )))
4	2, 3	ax-r2 36	. . . . . 6 ((a →3 b)⊥ ∩ (a ∪ b)) = (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ )))
5		ud3lem3b 573	. . . . . 6 ((a →3 b)⊥ ∩ (a ∪ b)⊥ ) = 0
6	4, 5	2or 72	. . . . 5 (((a →3 b)⊥ ∩ (a ∪ b)) ∪ ((a →3 b)⊥ ∩ (a ∪ b)⊥ )) = ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∪ 0)
7		or0 102	. . . . 5 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∪ 0) = (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ )))
8	6, 7	ax-r2 36	. . . 4 (((a →3 b)⊥ ∩ (a ∪ b)) ∪ ((a →3 b)⊥ ∩ (a ∪ b)⊥ )) = (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ )))
9		ud3lem3d 575	. . . 4 ((a →3 b) ∩ ((a →3 b)⊥ ∪ (a ∪ b))) = ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))
10	8, 9	2or 72	. . 3 ((((a →3 b)⊥ ∩ (a ∪ b)) ∪ ((a →3 b)⊥ ∩ (a ∪ b)⊥ )) ∪ ((a →3 b) ∩ ((a →3 b)⊥ ∪ (a ∪ b)))) = ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))))
11		coman1 185	. . . . . . . . . 10 (a⊥ ∩ b) C a⊥
12	11	comcom7 460	. . . . . . . . 9 (a⊥ ∩ b) C a
13		coman2 186	. . . . . . . . . 10 (a⊥ ∩ b) C b
14	13	comcom2 183	. . . . . . . . 9 (a⊥ ∩ b) C b⊥
15	12, 14	com2or 483	. . . . . . . 8 (a⊥ ∩ b) C (a ∪ b⊥ )
16	12, 13	com2or 483	. . . . . . . 8 (a⊥ ∩ b) C (a ∪ b)
17	15, 16	com2an 484	. . . . . . 7 (a⊥ ∩ b) C ((a ∪ b⊥ ) ∩ (a ∪ b))
18	17	comcom 453	. . . . . 6 ((a ∪ b⊥ ) ∩ (a ∪ b)) C (a⊥ ∩ b)
19		comorr 184	. . . . . . . . 9 a C (a ∪ b⊥ )
20		comorr 184	. . . . . . . . 9 a C (a ∪ b)
21	19, 20	com2an 484	. . . . . . . 8 a C ((a ∪ b⊥ ) ∩ (a ∪ b))
22	21	comcom 453	. . . . . . 7 ((a ∪ b⊥ ) ∩ (a ∪ b)) C a
23		comor1 461	. . . . . . . . . . 11 (a⊥ ∪ b) C a⊥
24	23	comcom7 460	. . . . . . . . . 10 (a⊥ ∪ b) C a
25		comor2 462	. . . . . . . . . . 11 (a⊥ ∪ b) C b
26	25	comcom2 183	. . . . . . . . . 10 (a⊥ ∪ b) C b⊥
27	24, 26	com2or 483	. . . . . . . . 9 (a⊥ ∪ b) C (a ∪ b⊥ )
28	24, 25	com2or 483	. . . . . . . . 9 (a⊥ ∪ b) C (a ∪ b)
29	27, 28	com2an 484	. . . . . . . 8 (a⊥ ∪ b) C ((a ∪ b⊥ ) ∩ (a ∪ b))
30	29	comcom 453	. . . . . . 7 ((a ∪ b⊥ ) ∩ (a ∪ b)) C (a⊥ ∪ b)
31	22, 30	com2an 484	. . . . . 6 ((a ∪ b⊥ ) ∩ (a ∪ b)) C (a ∩ (a⊥ ∪ b))
32	18, 31	com2or 483	. . . . 5 ((a ∪ b⊥ ) ∩ (a ∪ b)) C ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))
33	19	comcom3 454	. . . . . . . 8 a⊥ C (a ∪ b⊥ )
34	20	comcom3 454	. . . . . . . 8 a⊥ C (a ∪ b)
35	33, 34	com2an 484	. . . . . . 7 a⊥ C ((a ∪ b⊥ ) ∩ (a ∪ b))
36	35	comcom 453	. . . . . 6 ((a ∪ b⊥ ) ∩ (a ∪ b)) C a⊥
37		coman1 185	. . . . . . . . 9 (a ∩ b⊥ ) C a
38		coman2 186	. . . . . . . . 9 (a ∩ b⊥ ) C b⊥
39	37, 38	com2or 483	. . . . . . . 8 (a ∩ b⊥ ) C (a ∪ b⊥ )
40	38	comcom7 460	. . . . . . . . 9 (a ∩ b⊥ ) C b
41	37, 40	com2or 483	. . . . . . . 8 (a ∩ b⊥ ) C (a ∪ b)
42	39, 41	com2an 484	. . . . . . 7 (a ∩ b⊥ ) C ((a ∪ b⊥ ) ∩ (a ∪ b))
43	42	comcom 453	. . . . . 6 ((a ∪ b⊥ ) ∩ (a ∪ b)) C (a ∩ b⊥ )
44	36, 43	com2or 483	. . . . 5 ((a ∪ b⊥ ) ∩ (a ∪ b)) C (a⊥ ∪ (a ∩ b⊥ ))
45	32, 44	fh4r 476	. . . 4 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) = ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) ∩ ((a⊥ ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))))
46		comor1 461	. . . . . . . . . . 11 (a ∪ b⊥ ) C a
47	46	comcom2 183	. . . . . . . . . 10 (a ∪ b⊥ ) C a⊥
48		comor2 462	. . . . . . . . . . 11 (a ∪ b⊥ ) C b⊥
49	48	comcom7 460	. . . . . . . . . 10 (a ∪ b⊥ ) C b
50	47, 49	com2an 484	. . . . . . . . 9 (a ∪ b⊥ ) C (a⊥ ∩ b)
51	47, 49	com2or 483	. . . . . . . . . 10 (a ∪ b⊥ ) C (a⊥ ∪ b)
52	46, 51	com2an 484	. . . . . . . . 9 (a ∪ b⊥ ) C (a ∩ (a⊥ ∪ b))
53	50, 52	com2or 483	. . . . . . . 8 (a ∪ b⊥ ) C ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))
54	46, 49	com2or 483	. . . . . . . 8 (a ∪ b⊥ ) C (a ∪ b)
55	53, 54	fh4r 476	. . . . . . 7 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) = (((a ∪ b⊥ ) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) ∩ ((a ∪ b) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))))
56		ax-a3 32	. . . . . . . . . . 11 (((a ∪ b⊥ ) ∪ (a⊥ ∩ b)) ∪ (a ∩ (a⊥ ∪ b))) = ((a ∪ b⊥ ) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))))
57	56	ax-r1 35	. . . . . . . . . 10 ((a ∪ b⊥ ) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) = (((a ∪ b⊥ ) ∪ (a⊥ ∩ b)) ∪ (a ∩ (a⊥ ∪ b)))
58		anor2 89	. . . . . . . . . . . . . 14 (a⊥ ∩ b) = (a ∪ b⊥ )⊥
59	58	lor 70	. . . . . . . . . . . . 13 ((a ∪ b⊥ ) ∪ (a⊥ ∩ b)) = ((a ∪ b⊥ ) ∪ (a ∪ b⊥ )⊥ )
60		df-t 41	. . . . . . . . . . . . . 14 1 = ((a ∪ b⊥ ) ∪ (a ∪ b⊥ )⊥ )
61	60	ax-r1 35	. . . . . . . . . . . . 13 ((a ∪ b⊥ ) ∪ (a ∪ b⊥ )⊥ ) = 1
62	59, 61	ax-r2 36	. . . . . . . . . . . 12 ((a ∪ b⊥ ) ∪ (a⊥ ∩ b)) = 1
63	62	ax-r5 38	. . . . . . . . . . 11 (((a ∪ b⊥ ) ∪ (a⊥ ∩ b)) ∪ (a ∩ (a⊥ ∪ b))) = (1 ∪ (a ∩ (a⊥ ∪ b)))
64		or1r 105	. . . . . . . . . . 11 (1 ∪ (a ∩ (a⊥ ∪ b))) = 1
65	63, 64	ax-r2 36	. . . . . . . . . 10 (((a ∪ b⊥ ) ∪ (a⊥ ∩ b)) ∪ (a ∩ (a⊥ ∪ b))) = 1
66	57, 65	ax-r2 36	. . . . . . . . 9 ((a ∪ b⊥ ) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) = 1
67		ax-a2 31	. . . . . . . . . 10 ((a ∪ b) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) = (((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∪ (a ∪ b))
68		lear 161	. . . . . . . . . . . . 13 (a⊥ ∩ b) ≤ b
69		leor 159	. . . . . . . . . . . . 13 b ≤ (a ∪ b)
70	68, 69	letr 137	. . . . . . . . . . . 12 (a⊥ ∩ b) ≤ (a ∪ b)
71		lea 160	. . . . . . . . . . . . 13 (a ∩ (a⊥ ∪ b)) ≤ a
72		leo 158	. . . . . . . . . . . . 13 a ≤ (a ∪ b)
73	71, 72	letr 137	. . . . . . . . . . . 12 (a ∩ (a⊥ ∪ b)) ≤ (a ∪ b)
74	70, 73	lel2or 170	. . . . . . . . . . 11 ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ≤ (a ∪ b)
75	74	df-le2 131	. . . . . . . . . 10 (((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))) ∪ (a ∪ b)) = (a ∪ b)
76	67, 75	ax-r2 36	. . . . . . . . 9 ((a ∪ b) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) = (a ∪ b)
77	66, 76	2an 79	. . . . . . . 8 (((a ∪ b⊥ ) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) ∩ ((a ∪ b) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))))) = (1 ∩ (a ∪ b))
78		an1r 107	. . . . . . . 8 (1 ∩ (a ∪ b)) = (a ∪ b)
79	77, 78	ax-r2 36	. . . . . . 7 (((a ∪ b⊥ ) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) ∩ ((a ∪ b) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))))) = (a ∪ b)
80	55, 79	ax-r2 36	. . . . . 6 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) = (a ∪ b)
81		or12 80	. . . . . . 7 ((a⊥ ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) = ((a⊥ ∩ b) ∪ ((a⊥ ∪ (a ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b))))
82		df-a 40	. . . . . . . . . . . 12 (a ∩ (a⊥ ∪ b)) = (a⊥ ∪ (a⊥ ∪ b)⊥ )⊥
83		anor1 88	. . . . . . . . . . . . . . 15 (a ∩ b⊥ ) = (a⊥ ∪ b)⊥
84	83	ax-r1 35	. . . . . . . . . . . . . 14 (a⊥ ∪ b)⊥ = (a ∩ b⊥ )
85	84	lor 70	. . . . . . . . . . . . 13 (a⊥ ∪ (a⊥ ∪ b)⊥ ) = (a⊥ ∪ (a ∩ b⊥ ))
86	85	ax-r4 37	. . . . . . . . . . . 12 (a⊥ ∪ (a⊥ ∪ b)⊥ )⊥ = (a⊥ ∪ (a ∩ b⊥ ))⊥
87	82, 86	ax-r2 36	. . . . . . . . . . 11 (a ∩ (a⊥ ∪ b)) = (a⊥ ∪ (a ∩ b⊥ ))⊥
88	87	lor 70	. . . . . . . . . 10 ((a⊥ ∪ (a ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b))) = ((a⊥ ∪ (a ∩ b⊥ )) ∪ (a⊥ ∪ (a ∩ b⊥ ))⊥ )
89		df-t 41	. . . . . . . . . . 11 1 = ((a⊥ ∪ (a ∩ b⊥ )) ∪ (a⊥ ∪ (a ∩ b⊥ ))⊥ )
90	89	ax-r1 35	. . . . . . . . . 10 ((a⊥ ∪ (a ∩ b⊥ )) ∪ (a⊥ ∪ (a ∩ b⊥ ))⊥ ) = 1
91	88, 90	ax-r2 36	. . . . . . . . 9 ((a⊥ ∪ (a ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b))) = 1
92	91	lor 70	. . . . . . . 8 ((a⊥ ∩ b) ∪ ((a⊥ ∪ (a ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b)))) = ((a⊥ ∩ b) ∪ 1)
93		or1 104	. . . . . . . 8 ((a⊥ ∩ b) ∪ 1) = 1
94	92, 93	ax-r2 36	. . . . . . 7 ((a⊥ ∩ b) ∪ ((a⊥ ∪ (a ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b)))) = 1
95	81, 94	ax-r2 36	. . . . . 6 ((a⊥ ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) = 1
96	80, 95	2an 79	. . . . 5 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) ∩ ((a⊥ ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))))) = ((a ∪ b) ∩ 1)
97		an1 106	. . . . 5 ((a ∪ b) ∩ 1) = (a ∪ b)
98	96, 97	ax-r2 36	. . . 4 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) ∩ ((a⊥ ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b))))) = (a ∪ b)
99	45, 98	ax-r2 36	. . 3 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∪ ((a⊥ ∩ b) ∪ (a ∩ (a⊥ ∪ b)))) = (a ∪ b)
100	10, 99	ax-r2 36	. 2 ((((a →3 b)⊥ ∩ (a ∪ b)) ∪ ((a →3 b)⊥ ∩ (a ∪ b)⊥ )) ∪ ((a →3 b) ∩ ((a →3 b)⊥ ∪ (a ∪ b)))) = (a ∪ b)
101	1, 100	ax-r2 36	1 ((a →3 b) →3 (a ∪ b)) = (a ∪ b)

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8  0wf 9   →₃ wi3 14

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

This theorem is referenced by:  ud3  597