Theorem u3lem11 786

Description: Lemma for unified implication study. (Contributed by NM, 18-Jan-1998.)

Assertion

Ref	Expression
u3lem11	(a →3 (b⊥ ∩ (a ∪ b))) = (a →3 b⊥ )

Proof of Theorem u3lem11

Step	Hyp	Ref	Expression
1		df-i3 46	. 2 (a →3 (b⊥ ∩ (a ∪ b))) = (((a⊥ ∩ (b⊥ ∩ (a ∪ b))) ∪ (a⊥ ∩ (b⊥ ∩ (a ∪ b))⊥ )) ∪ (a ∩ (a⊥ ∪ (b⊥ ∩ (a ∪ b)))))
2		ax-a1 30	. . . . . 6 b = b⊥ ⊥
3	2	lan 77	. . . . 5 (a⊥ ∩ b) = (a⊥ ∩ b⊥ ⊥ )
4	3	lor 70	. . . 4 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ ))
5	4	ax-r5 38	. . 3 (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)) ∪ (a ∩ (a⊥ ∪ b⊥ ))) = (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ (a ∩ (a⊥ ∪ b⊥ )))
6		oran 87	. . . . . . . 8 (a ∪ b) = (a⊥ ∩ b⊥ )⊥
7	6	lan 77	. . . . . . 7 ((a⊥ ∩ b⊥ ) ∩ (a ∪ b)) = ((a⊥ ∩ b⊥ ) ∩ (a⊥ ∩ b⊥ )⊥ )
8		anass 76	. . . . . . . 8 ((a⊥ ∩ b⊥ ) ∩ (a ∪ b)) = (a⊥ ∩ (b⊥ ∩ (a ∪ b)))
9	8	ax-r1 35	. . . . . . 7 (a⊥ ∩ (b⊥ ∩ (a ∪ b))) = ((a⊥ ∩ b⊥ ) ∩ (a ∪ b))
10		dff 101	. . . . . . 7 0 = ((a⊥ ∩ b⊥ ) ∩ (a⊥ ∩ b⊥ )⊥ )
11	7, 9, 10	3tr1 63	. . . . . 6 (a⊥ ∩ (b⊥ ∩ (a ∪ b))) = 0
12		anor3 90	. . . . . . . . . . . 12 (a⊥ ∩ b⊥ ) = (a ∪ b)⊥
13	12	ax-r5 38	. . . . . . . . . . 11 ((a⊥ ∩ b⊥ ) ∪ b) = ((a ∪ b)⊥ ∪ b)
14		ax-a2 31	. . . . . . . . . . 11 ((a ∪ b)⊥ ∪ b) = (b ∪ (a ∪ b)⊥ )
15	13, 14	ax-r2 36	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∪ b) = (b ∪ (a ∪ b)⊥ )
16		oran1 91	. . . . . . . . . 10 (b ∪ (a ∪ b)⊥ ) = (b⊥ ∩ (a ∪ b))⊥
17	15, 16	ax-r2 36	. . . . . . . . 9 ((a⊥ ∩ b⊥ ) ∪ b) = (b⊥ ∩ (a ∪ b))⊥
18	17	ax-r1 35	. . . . . . . 8 (b⊥ ∩ (a ∪ b))⊥ = ((a⊥ ∩ b⊥ ) ∪ b)
19	18	lan 77	. . . . . . 7 (a⊥ ∩ (b⊥ ∩ (a ∪ b))⊥ ) = (a⊥ ∩ ((a⊥ ∩ b⊥ ) ∪ b))
20		coman1 185	. . . . . . . . 9 (a⊥ ∩ b⊥ ) C a⊥
21		coman2 186	. . . . . . . . . 10 (a⊥ ∩ b⊥ ) C b⊥
22	21	comcom7 460	. . . . . . . . 9 (a⊥ ∩ b⊥ ) C b
23	20, 22	fh2 470	. . . . . . . 8 (a⊥ ∩ ((a⊥ ∩ b⊥ ) ∪ b)) = ((a⊥ ∩ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∩ b))
24		anass 76	. . . . . . . . . . 11 ((a⊥ ∩ a⊥ ) ∩ b⊥ ) = (a⊥ ∩ (a⊥ ∩ b⊥ ))
25	24	ax-r1 35	. . . . . . . . . 10 (a⊥ ∩ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ a⊥ ) ∩ b⊥ )
26		anidm 111	. . . . . . . . . . 11 (a⊥ ∩ a⊥ ) = a⊥
27	26	ran 78	. . . . . . . . . 10 ((a⊥ ∩ a⊥ ) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
28	25, 27	ax-r2 36	. . . . . . . . 9 (a⊥ ∩ (a⊥ ∩ b⊥ )) = (a⊥ ∩ b⊥ )
29	28	ax-r5 38	. . . . . . . 8 ((a⊥ ∩ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∩ b)) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))
30	23, 29	ax-r2 36	. . . . . . 7 (a⊥ ∩ ((a⊥ ∩ b⊥ ) ∪ b)) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))
31	19, 30	ax-r2 36	. . . . . 6 (a⊥ ∩ (b⊥ ∩ (a ∪ b))⊥ ) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))
32	11, 31	2or 72	. . . . 5 ((a⊥ ∩ (b⊥ ∩ (a ∪ b))) ∪ (a⊥ ∩ (b⊥ ∩ (a ∪ b))⊥ )) = (0 ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)))
33		ax-a2 31	. . . . . 6 (0 ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) = (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)) ∪ 0)
34		or0 102	. . . . . 6 (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)) ∪ 0) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))
35	33, 34	ax-r2 36	. . . . 5 (0 ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))
36	32, 35	ax-r2 36	. . . 4 ((a⊥ ∩ (b⊥ ∩ (a ∪ b))) ∪ (a⊥ ∩ (b⊥ ∩ (a ∪ b))⊥ )) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))
37		ax-a2 31	. . . . . . . . . . 11 (a⊥ ∪ a) = (a ∪ a⊥ )
38		df-t 41	. . . . . . . . . . . 12 1 = (a ∪ a⊥ )
39	38	ax-r1 35	. . . . . . . . . . 11 (a ∪ a⊥ ) = 1
40	37, 39	ax-r2 36	. . . . . . . . . 10 (a⊥ ∪ a) = 1
41	40	ax-r5 38	. . . . . . . . 9 ((a⊥ ∪ a) ∪ b) = (1 ∪ b)
42		ax-a3 32	. . . . . . . . 9 ((a⊥ ∪ a) ∪ b) = (a⊥ ∪ (a ∪ b))
43		ax-a2 31	. . . . . . . . . 10 (1 ∪ b) = (b ∪ 1)
44		or1 104	. . . . . . . . . 10 (b ∪ 1) = 1
45	43, 44	ax-r2 36	. . . . . . . . 9 (1 ∪ b) = 1
46	41, 42, 45	3tr2 64	. . . . . . . 8 (a⊥ ∪ (a ∪ b)) = 1
47	46	ran 78	. . . . . . 7 ((a⊥ ∪ (a ∪ b)) ∩ (a⊥ ∪ b⊥ )) = (1 ∩ (a⊥ ∪ b⊥ ))
48		ancom 74	. . . . . . . 8 (1 ∩ (a⊥ ∪ b⊥ )) = ((a⊥ ∪ b⊥ ) ∩ 1)
49		an1 106	. . . . . . . 8 ((a⊥ ∪ b⊥ ) ∩ 1) = (a⊥ ∪ b⊥ )
50	48, 49	ax-r2 36	. . . . . . 7 (1 ∩ (a⊥ ∪ b⊥ )) = (a⊥ ∪ b⊥ )
51	47, 50	ax-r2 36	. . . . . 6 ((a⊥ ∪ (a ∪ b)) ∩ (a⊥ ∪ b⊥ )) = (a⊥ ∪ b⊥ )
52	51	lan 77	. . . . 5 (a ∩ ((a⊥ ∪ (a ∪ b)) ∩ (a⊥ ∪ b⊥ ))) = (a ∩ (a⊥ ∪ b⊥ ))
53		ancom 74	. . . . . . . 8 (b⊥ ∩ (a ∪ b)) = ((a ∪ b) ∩ b⊥ )
54	53	lor 70	. . . . . . 7 (a⊥ ∪ (b⊥ ∩ (a ∪ b))) = (a⊥ ∪ ((a ∪ b) ∩ b⊥ ))
55		comor1 461	. . . . . . . . 9 (a ∪ b) C a
56	55	comcom2 183	. . . . . . . 8 (a ∪ b) C a⊥
57		comor2 462	. . . . . . . . 9 (a ∪ b) C b
58	57	comcom2 183	. . . . . . . 8 (a ∪ b) C b⊥
59	56, 58	fh4 472	. . . . . . 7 (a⊥ ∪ ((a ∪ b) ∩ b⊥ )) = ((a⊥ ∪ (a ∪ b)) ∩ (a⊥ ∪ b⊥ ))
60	54, 59	ax-r2 36	. . . . . 6 (a⊥ ∪ (b⊥ ∩ (a ∪ b))) = ((a⊥ ∪ (a ∪ b)) ∩ (a⊥ ∪ b⊥ ))
61	60	lan 77	. . . . 5 (a ∩ (a⊥ ∪ (b⊥ ∩ (a ∪ b)))) = (a ∩ ((a⊥ ∪ (a ∪ b)) ∩ (a⊥ ∪ b⊥ )))
62		id 59	. . . . 5 (a ∩ (a⊥ ∪ b⊥ )) = (a ∩ (a⊥ ∪ b⊥ ))
63	52, 61, 62	3tr1 63	. . . 4 (a ∩ (a⊥ ∪ (b⊥ ∩ (a ∪ b)))) = (a ∩ (a⊥ ∪ b⊥ ))
64	36, 63	2or 72	. . 3 (((a⊥ ∩ (b⊥ ∩ (a ∪ b))) ∪ (a⊥ ∩ (b⊥ ∩ (a ∪ b))⊥ )) ∪ (a ∩ (a⊥ ∪ (b⊥ ∩ (a ∪ b))))) = (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)) ∪ (a ∩ (a⊥ ∪ b⊥ )))
65		df-i3 46	. . 3 (a →3 b⊥ ) = (((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ ⊥ )) ∪ (a ∩ (a⊥ ∪ b⊥ )))
66	5, 64, 65	3tr1 63	. 2 (((a⊥ ∩ (b⊥ ∩ (a ∪ b))) ∪ (a⊥ ∩ (b⊥ ∩ (a ∪ b))⊥ )) ∪ (a ∩ (a⊥ ∪ (b⊥ ∩ (a ∪ b))))) = (a →3 b⊥ )
67	1, 66	ax-r2 36	1 (a →3 (b⊥ ∩ (a ∪ b))) = (a →3 b⊥ )

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8  0wf 9   →₃ wi3 14

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

This theorem is used by:  u3lem11a  787