Theorem ud4lem1a 577

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

Assertion

Ref	Expression
ud4lem1a	((a →4 b) ∩ (b →4 a)) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))

Proof of Theorem ud4lem1a

Step	Hyp	Ref	Expression
1		df-i4 47	. . 3 (a →4 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ ))
2		df-i4 47	. . 3 (b →4 a) = (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ ))
3	1, 2	2an 79	. 2 ((a →4 b) ∩ (b →4 a)) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ )) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ )))
4		coman2 186	. . . . . . . . . 10 (a ∩ b) C b
5	4	comcom 453	. . . . . . . . 9 b C (a ∩ b)
6		coman2 186	. . . . . . . . . 10 (a⊥ ∩ b) C b
7	6	comcom 453	. . . . . . . . 9 b C (a⊥ ∩ b)
8	5, 7	com2or 483	. . . . . . . 8 b C ((a ∩ b) ∪ (a⊥ ∩ b))
9	8	comcom 453	. . . . . . 7 ((a ∩ b) ∪ (a⊥ ∩ b)) C b
10		coman1 185	. . . . . . . . . 10 (a ∩ b) C a
11	10	comcom 453	. . . . . . . . 9 a C (a ∩ b)
12		coman1 185	. . . . . . . . . . . 12 (a⊥ ∩ b) C a⊥
13	12	comcom 453	. . . . . . . . . . 11 a⊥ C (a⊥ ∩ b)
14	13	comcom2 183	. . . . . . . . . 10 a⊥ C (a⊥ ∩ b)⊥
15	14	comcom5 458	. . . . . . . . 9 a C (a⊥ ∩ b)
16	11, 15	com2or 483	. . . . . . . 8 a C ((a ∩ b) ∪ (a⊥ ∩ b))
17	16	comcom 453	. . . . . . 7 ((a ∩ b) ∪ (a⊥ ∩ b)) C a
18	9, 17	com2an 484	. . . . . 6 ((a ∩ b) ∪ (a⊥ ∩ b)) C (b ∩ a)
19	5	comcom3 454	. . . . . . . . 9 b⊥ C (a ∩ b)
20	7	comcom3 454	. . . . . . . . 9 b⊥ C (a⊥ ∩ b)
21	19, 20	com2or 483	. . . . . . . 8 b⊥ C ((a ∩ b) ∪ (a⊥ ∩ b))
22	21	comcom 453	. . . . . . 7 ((a ∩ b) ∪ (a⊥ ∩ b)) C b⊥
23	22, 17	com2an 484	. . . . . 6 ((a ∩ b) ∪ (a⊥ ∩ b)) C (b⊥ ∩ a)
24	18, 23	com2or 483	. . . . 5 ((a ∩ b) ∪ (a⊥ ∩ b)) C ((b ∩ a) ∪ (b⊥ ∩ a))
25	22, 17	com2or 483	. . . . . 6 ((a ∩ b) ∪ (a⊥ ∩ b)) C (b⊥ ∪ a)
26	11	comcom3 454	. . . . . . . 8 a⊥ C (a ∩ b)
27	26, 13	com2or 483	. . . . . . 7 a⊥ C ((a ∩ b) ∪ (a⊥ ∩ b))
28	27	comcom 453	. . . . . 6 ((a ∩ b) ∪ (a⊥ ∩ b)) C a⊥
29	25, 28	com2an 484	. . . . 5 ((a ∩ b) ∪ (a⊥ ∩ b)) C ((b⊥ ∪ a) ∩ a⊥ )
30	24, 29	com2or 483	. . . 4 ((a ∩ b) ∪ (a⊥ ∩ b)) C (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ ))
31	28, 9	com2or 483	. . . . 5 ((a ∩ b) ∪ (a⊥ ∩ b)) C (a⊥ ∪ b)
32	9	comcom2 183	. . . . 5 ((a ∩ b) ∪ (a⊥ ∩ b)) C b⊥
33	31, 32	com2an 484	. . . 4 ((a ∩ b) ∪ (a⊥ ∩ b)) C ((a⊥ ∪ b) ∩ b⊥ )
34	30, 33	fh2r 474	. . 3 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ )) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ ))) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ ))) ∪ (((a⊥ ∪ b) ∩ b⊥ ) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ ))))
35		ancom 74	. . . . . . . . 9 (b ∩ a) = (a ∩ b)
36		ancom 74	. . . . . . . . 9 (b⊥ ∩ a) = (a ∩ b⊥ )
37	35, 36	2or 72	. . . . . . . 8 ((b ∩ a) ∪ (b⊥ ∩ a)) = ((a ∩ b) ∪ (a ∩ b⊥ ))
38		ax-a2 31	. . . . . . . . 9 (b⊥ ∪ a) = (a ∪ b⊥ )
39	38	ran 78	. . . . . . . 8 ((b⊥ ∪ a) ∩ a⊥ ) = ((a ∪ b⊥ ) ∩ a⊥ )
40	37, 39	2or 72	. . . . . . 7 (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ )) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a ∪ b⊥ ) ∩ a⊥ ))
41	40	lan 77	. . . . . 6 (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ ))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a ∪ b⊥ ) ∩ a⊥ )))
42	17, 9	com2an 484	. . . . . . . . 9 ((a ∩ b) ∪ (a⊥ ∩ b)) C (a ∩ b)
43	17, 22	com2an 484	. . . . . . . . 9 ((a ∩ b) ∪ (a⊥ ∩ b)) C (a ∩ b⊥ )
44	42, 43	com2or 483	. . . . . . . 8 ((a ∩ b) ∪ (a⊥ ∩ b)) C ((a ∩ b) ∪ (a ∩ b⊥ ))
45	17, 32	com2or 483	. . . . . . . . 9 ((a ∩ b) ∪ (a⊥ ∩ b)) C (a ∪ b⊥ )
46	45, 28	com2an 484	. . . . . . . 8 ((a ∩ b) ∪ (a⊥ ∩ b)) C ((a ∪ b⊥ ) ∩ a⊥ )
47	44, 46	fh1 469	. . . . . . 7 (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a ∪ b⊥ ) ∩ a⊥ ))) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ ((a ∩ b) ∪ (a ∩ b⊥ ))) ∪ (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ ((a ∪ b⊥ ) ∩ a⊥ )))
48		an4 86	. . . . . . . . . . 11 ((a⊥ ∩ b) ∩ (a ∩ b⊥ )) = ((a⊥ ∩ a) ∩ (b ∩ b⊥ ))
49		dff 101	. . . . . . . . . . . . . 14 0 = (b ∩ b⊥ )
50	49	ax-r1 35	. . . . . . . . . . . . 13 (b ∩ b⊥ ) = 0
51	50	lan 77	. . . . . . . . . . . 12 ((a⊥ ∩ a) ∩ (b ∩ b⊥ )) = ((a⊥ ∩ a) ∩ 0)
52		an0 108	. . . . . . . . . . . 12 ((a⊥ ∩ a) ∩ 0) = 0
53	51, 52	ax-r2 36	. . . . . . . . . . 11 ((a⊥ ∩ a) ∩ (b ∩ b⊥ )) = 0
54	48, 53	ax-r2 36	. . . . . . . . . 10 ((a⊥ ∩ b) ∩ (a ∩ b⊥ )) = 0
55	54	lor 70	. . . . . . . . 9 ((a ∩ b) ∪ ((a⊥ ∩ b) ∩ (a ∩ b⊥ ))) = ((a ∩ b) ∪ 0)
56	10	comcom2 183	. . . . . . . . . . 11 (a ∩ b) C a⊥
57	56, 4	com2an 484	. . . . . . . . . 10 (a ∩ b) C (a⊥ ∩ b)
58	4	comcom2 183	. . . . . . . . . . 11 (a ∩ b) C b⊥
59	10, 58	com2an 484	. . . . . . . . . 10 (a ∩ b) C (a ∩ b⊥ )
60	57, 59	fh3 471	. . . . . . . . 9 ((a ∩ b) ∪ ((a⊥ ∩ b) ∩ (a ∩ b⊥ ))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ ((a ∩ b) ∪ (a ∩ b⊥ )))
61		or0 102	. . . . . . . . 9 ((a ∩ b) ∪ 0) = (a ∩ b)
62	55, 60, 61	3tr2 64	. . . . . . . 8 (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ ((a ∩ b) ∪ (a ∩ b⊥ ))) = (a ∩ b)
63	10, 58	com2or 483	. . . . . . . . . . 11 (a ∩ b) C (a ∪ b⊥ )
64	63, 56	com2an 484	. . . . . . . . . 10 (a ∩ b) C ((a ∪ b⊥ ) ∩ a⊥ )
65	64, 57	fh2r 474	. . . . . . . . 9 (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ ((a ∪ b⊥ ) ∩ a⊥ )) = (((a ∩ b) ∩ ((a ∪ b⊥ ) ∩ a⊥ )) ∪ ((a⊥ ∩ b) ∩ ((a ∪ b⊥ ) ∩ a⊥ )))
66		an12 81	. . . . . . . . . . . 12 ((a ∩ b) ∩ ((a ∪ b⊥ ) ∩ a⊥ )) = ((a ∪ b⊥ ) ∩ ((a ∩ b) ∩ a⊥ ))
67		an32 83	. . . . . . . . . . . . . . 15 ((a ∩ b) ∩ a⊥ ) = ((a ∩ a⊥ ) ∩ b)
68		ancom 74	. . . . . . . . . . . . . . . 16 ((a ∩ a⊥ ) ∩ b) = (b ∩ (a ∩ a⊥ ))
69		dff 101	. . . . . . . . . . . . . . . . . . 19 0 = (a ∩ a⊥ )
70	69	ax-r1 35	. . . . . . . . . . . . . . . . . 18 (a ∩ a⊥ ) = 0
71	70	lan 77	. . . . . . . . . . . . . . . . 17 (b ∩ (a ∩ a⊥ )) = (b ∩ 0)
72		an0 108	. . . . . . . . . . . . . . . . 17 (b ∩ 0) = 0
73	71, 72	ax-r2 36	. . . . . . . . . . . . . . . 16 (b ∩ (a ∩ a⊥ )) = 0
74	68, 73	ax-r2 36	. . . . . . . . . . . . . . 15 ((a ∩ a⊥ ) ∩ b) = 0
75	67, 74	ax-r2 36	. . . . . . . . . . . . . 14 ((a ∩ b) ∩ a⊥ ) = 0
76	75	lan 77	. . . . . . . . . . . . 13 ((a ∪ b⊥ ) ∩ ((a ∩ b) ∩ a⊥ )) = ((a ∪ b⊥ ) ∩ 0)
77		an0 108	. . . . . . . . . . . . 13 ((a ∪ b⊥ ) ∩ 0) = 0
78	76, 77	ax-r2 36	. . . . . . . . . . . 12 ((a ∪ b⊥ ) ∩ ((a ∩ b) ∩ a⊥ )) = 0
79	66, 78	ax-r2 36	. . . . . . . . . . 11 ((a ∩ b) ∩ ((a ∪ b⊥ ) ∩ a⊥ )) = 0
80		ancom 74	. . . . . . . . . . . 12 (((a⊥ ∩ b) ∩ (a ∪ b⊥ )) ∩ a⊥ ) = (a⊥ ∩ ((a⊥ ∩ b) ∩ (a ∪ b⊥ )))
81		anass 76	. . . . . . . . . . . 12 (((a⊥ ∩ b) ∩ (a ∪ b⊥ )) ∩ a⊥ ) = ((a⊥ ∩ b) ∩ ((a ∪ b⊥ ) ∩ a⊥ ))
82		anor2 89	. . . . . . . . . . . . . . . . . 18 (a⊥ ∩ b) = (a ∪ b⊥ )⊥
83	82	ax-r1 35	. . . . . . . . . . . . . . . . 17 (a ∪ b⊥ )⊥ = (a⊥ ∩ b)
84	83	con3 68	. . . . . . . . . . . . . . . 16 (a ∪ b⊥ ) = (a⊥ ∩ b)⊥
85	84	lan 77	. . . . . . . . . . . . . . 15 ((a⊥ ∩ b) ∩ (a ∪ b⊥ )) = ((a⊥ ∩ b) ∩ (a⊥ ∩ b)⊥ )
86		dff 101	. . . . . . . . . . . . . . . 16 0 = ((a⊥ ∩ b) ∩ (a⊥ ∩ b)⊥ )
87	86	ax-r1 35	. . . . . . . . . . . . . . 15 ((a⊥ ∩ b) ∩ (a⊥ ∩ b)⊥ ) = 0
88	85, 87	ax-r2 36	. . . . . . . . . . . . . 14 ((a⊥ ∩ b) ∩ (a ∪ b⊥ )) = 0
89	88	lan 77	. . . . . . . . . . . . 13 (a⊥ ∩ ((a⊥ ∩ b) ∩ (a ∪ b⊥ ))) = (a⊥ ∩ 0)
90		an0 108	. . . . . . . . . . . . 13 (a⊥ ∩ 0) = 0
91	89, 90	ax-r2 36	. . . . . . . . . . . 12 (a⊥ ∩ ((a⊥ ∩ b) ∩ (a ∪ b⊥ ))) = 0
92	80, 81, 91	3tr2 64	. . . . . . . . . . 11 ((a⊥ ∩ b) ∩ ((a ∪ b⊥ ) ∩ a⊥ )) = 0
93	79, 92	2or 72	. . . . . . . . . 10 (((a ∩ b) ∩ ((a ∪ b⊥ ) ∩ a⊥ )) ∪ ((a⊥ ∩ b) ∩ ((a ∪ b⊥ ) ∩ a⊥ ))) = (0 ∪ 0)
94		or0 102	. . . . . . . . . 10 (0 ∪ 0) = 0
95	93, 94	ax-r2 36	. . . . . . . . 9 (((a ∩ b) ∩ ((a ∪ b⊥ ) ∩ a⊥ )) ∪ ((a⊥ ∩ b) ∩ ((a ∪ b⊥ ) ∩ a⊥ ))) = 0
96	65, 95	ax-r2 36	. . . . . . . 8 (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ ((a ∪ b⊥ ) ∩ a⊥ )) = 0
97	62, 96	2or 72	. . . . . . 7 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ ((a ∩ b) ∪ (a ∩ b⊥ ))) ∪ (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ ((a ∪ b⊥ ) ∩ a⊥ ))) = ((a ∩ b) ∪ 0)
98	47, 97	ax-r2 36	. . . . . 6 (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a ∪ b⊥ ) ∩ a⊥ ))) = ((a ∩ b) ∪ 0)
99	41, 98	ax-r2 36	. . . . 5 (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ ))) = ((a ∩ b) ∪ 0)
100	99, 61	ax-r2 36	. . . 4 (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ ))) = (a ∩ b)
101		coman2 186	. . . . . . . . . . . 12 (b ∩ a) C a
102	101	comcom 453	. . . . . . . . . . 11 a C (b ∩ a)
103		coman2 186	. . . . . . . . . . . 12 (b⊥ ∩ a) C a
104	103	comcom 453	. . . . . . . . . . 11 a C (b⊥ ∩ a)
105	102, 104	com2or 483	. . . . . . . . . 10 a C ((b ∩ a) ∪ (b⊥ ∩ a))
106	105	comcom3 454	. . . . . . . . 9 a⊥ C ((b ∩ a) ∪ (b⊥ ∩ a))
107	106	comcom 453	. . . . . . . 8 ((b ∩ a) ∪ (b⊥ ∩ a)) C a⊥
108		coman1 185	. . . . . . . . . . 11 (b ∩ a) C b
109	108	comcom 453	. . . . . . . . . 10 b C (b ∩ a)
110		coman1 185	. . . . . . . . . . . . 13 (b⊥ ∩ a) C b⊥
111	110	comcom 453	. . . . . . . . . . . 12 b⊥ C (b⊥ ∩ a)
112	111	comcom2 183	. . . . . . . . . . 11 b⊥ C (b⊥ ∩ a)⊥
113	112	comcom5 458	. . . . . . . . . 10 b C (b⊥ ∩ a)
114	109, 113	com2or 483	. . . . . . . . 9 b C ((b ∩ a) ∪ (b⊥ ∩ a))
115	114	comcom 453	. . . . . . . 8 ((b ∩ a) ∪ (b⊥ ∩ a)) C b
116	107, 115	com2or 483	. . . . . . 7 ((b ∩ a) ∪ (b⊥ ∩ a)) C (a⊥ ∪ b)
117	109	comcom3 454	. . . . . . . . 9 b⊥ C (b ∩ a)
118	117, 111	com2or 483	. . . . . . . 8 b⊥ C ((b ∩ a) ∪ (b⊥ ∩ a))
119	118	comcom 453	. . . . . . 7 ((b ∩ a) ∪ (b⊥ ∩ a)) C b⊥
120	116, 119	com2an 484	. . . . . 6 ((b ∩ a) ∪ (b⊥ ∩ a)) C ((a⊥ ∪ b) ∩ b⊥ )
121	105	comcom 453	. . . . . . . 8 ((b ∩ a) ∪ (b⊥ ∩ a)) C a
122	119, 121	com2or 483	. . . . . . 7 ((b ∩ a) ∪ (b⊥ ∩ a)) C (b⊥ ∪ a)
123	102	comcom3 454	. . . . . . . . 9 a⊥ C (b ∩ a)
124	104	comcom3 454	. . . . . . . . 9 a⊥ C (b⊥ ∩ a)
125	123, 124	com2or 483	. . . . . . . 8 a⊥ C ((b ∩ a) ∪ (b⊥ ∩ a))
126	125	comcom 453	. . . . . . 7 ((b ∩ a) ∪ (b⊥ ∩ a)) C a⊥
127	122, 126	com2an 484	. . . . . 6 ((b ∩ a) ∪ (b⊥ ∩ a)) C ((b⊥ ∪ a) ∩ a⊥ )
128	120, 127	fh2 470	. . . . 5 (((a⊥ ∪ b) ∩ b⊥ ) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ ))) = ((((a⊥ ∪ b) ∩ b⊥ ) ∩ ((b ∩ a) ∪ (b⊥ ∩ a))) ∪ (((a⊥ ∪ b) ∩ b⊥ ) ∩ ((b⊥ ∪ a) ∩ a⊥ )))
129		lea 160	. . . . . . . . . . . . 13 (b ∩ a) ≤ b
130	129	lecon 154	. . . . . . . . . . . 12 b⊥ ≤ (b ∩ a)⊥
131	130	lelan 167	. . . . . . . . . . 11 ((a⊥ ∪ b) ∩ b⊥ ) ≤ ((a⊥ ∪ b) ∩ (b ∩ a)⊥ )
132	131	lecon 154	. . . . . . . . . 10 ((a⊥ ∪ b) ∩ (b ∩ a)⊥ )⊥ ≤ ((a⊥ ∪ b) ∩ b⊥ )⊥
133	132	lelan 167	. . . . . . . . 9 (((a⊥ ∪ b) ∩ b⊥ ) ∩ ((a⊥ ∪ b) ∩ (b ∩ a)⊥ )⊥ ) ≤ (((a⊥ ∪ b) ∩ b⊥ ) ∩ ((a⊥ ∪ b) ∩ b⊥ )⊥ )
134		ax-a2 31	. . . . . . . . . . 11 ((b ∩ a) ∪ (b⊥ ∩ a)) = ((b⊥ ∩ a) ∪ (b ∩ a))
135		oran 87	. . . . . . . . . . . 12 ((b⊥ ∩ a) ∪ (b ∩ a)) = ((b⊥ ∩ a)⊥ ∩ (b ∩ a)⊥ )⊥
136		anor1 88	. . . . . . . . . . . . . . . 16 (a ∩ b⊥ ) = (a⊥ ∪ b)⊥
137	36, 136	ax-r2 36	. . . . . . . . . . . . . . 15 (b⊥ ∩ a) = (a⊥ ∪ b)⊥
138	137	con2 67	. . . . . . . . . . . . . 14 (b⊥ ∩ a)⊥ = (a⊥ ∪ b)
139	138	ran 78	. . . . . . . . . . . . 13 ((b⊥ ∩ a)⊥ ∩ (b ∩ a)⊥ ) = ((a⊥ ∪ b) ∩ (b ∩ a)⊥ )
140	139	ax-r4 37	. . . . . . . . . . . 12 ((b⊥ ∩ a)⊥ ∩ (b ∩ a)⊥ )⊥ = ((a⊥ ∪ b) ∩ (b ∩ a)⊥ )⊥
141	135, 140	ax-r2 36	. . . . . . . . . . 11 ((b⊥ ∩ a) ∪ (b ∩ a)) = ((a⊥ ∪ b) ∩ (b ∩ a)⊥ )⊥
142	134, 141	ax-r2 36	. . . . . . . . . 10 ((b ∩ a) ∪ (b⊥ ∩ a)) = ((a⊥ ∪ b) ∩ (b ∩ a)⊥ )⊥
143	142	lan 77	. . . . . . . . 9 (((a⊥ ∪ b) ∩ b⊥ ) ∩ ((b ∩ a) ∪ (b⊥ ∩ a))) = (((a⊥ ∪ b) ∩ b⊥ ) ∩ ((a⊥ ∪ b) ∩ (b ∩ a)⊥ )⊥ )
144		dff 101	. . . . . . . . 9 0 = (((a⊥ ∪ b) ∩ b⊥ ) ∩ ((a⊥ ∪ b) ∩ b⊥ )⊥ )
145	133, 143, 144	le3tr1 140	. . . . . . . 8 (((a⊥ ∪ b) ∩ b⊥ ) ∩ ((b ∩ a) ∪ (b⊥ ∩ a))) ≤ 0
146		le0 147	. . . . . . . 8 0 ≤ (((a⊥ ∪ b) ∩ b⊥ ) ∩ ((b ∩ a) ∪ (b⊥ ∩ a)))
147	145, 146	lebi 145	. . . . . . 7 (((a⊥ ∪ b) ∩ b⊥ ) ∩ ((b ∩ a) ∪ (b⊥ ∩ a))) = 0
148		an4 86	. . . . . . . 8 (((a⊥ ∪ b) ∩ b⊥ ) ∩ ((b⊥ ∪ a) ∩ a⊥ )) = (((a⊥ ∪ b) ∩ (b⊥ ∪ a)) ∩ (b⊥ ∩ a⊥ ))
149		ancom 74	. . . . . . . . . 10 (((a⊥ ∪ b) ∩ (b⊥ ∪ a)) ∩ (b⊥ ∩ a⊥ )) = ((b⊥ ∩ a⊥ ) ∩ ((a⊥ ∪ b) ∩ (b⊥ ∪ a)))
150		ancom 74	. . . . . . . . . . . 12 ((a⊥ ∪ b) ∩ (b⊥ ∪ a)) = ((b⊥ ∪ a) ∩ (a⊥ ∪ b))
151	150	lan 77	. . . . . . . . . . 11 ((b⊥ ∩ a⊥ ) ∩ ((a⊥ ∪ b) ∩ (b⊥ ∪ a))) = ((b⊥ ∩ a⊥ ) ∩ ((b⊥ ∪ a) ∩ (a⊥ ∪ b)))
152		leo 158	. . . . . . . . . . . . 13 b⊥ ≤ (b⊥ ∪ a)
153		leo 158	. . . . . . . . . . . . 13 a⊥ ≤ (a⊥ ∪ b)
154	152, 153	le2an 169	. . . . . . . . . . . 12 (b⊥ ∩ a⊥ ) ≤ ((b⊥ ∪ a) ∩ (a⊥ ∪ b))
155	154	df2le2 136	. . . . . . . . . . 11 ((b⊥ ∩ a⊥ ) ∩ ((b⊥ ∪ a) ∩ (a⊥ ∪ b))) = (b⊥ ∩ a⊥ )
156	151, 155	ax-r2 36	. . . . . . . . . 10 ((b⊥ ∩ a⊥ ) ∩ ((a⊥ ∪ b) ∩ (b⊥ ∪ a))) = (b⊥ ∩ a⊥ )
157	149, 156	ax-r2 36	. . . . . . . . 9 (((a⊥ ∪ b) ∩ (b⊥ ∪ a)) ∩ (b⊥ ∩ a⊥ )) = (b⊥ ∩ a⊥ )
158		ancom 74	. . . . . . . . 9 (b⊥ ∩ a⊥ ) = (a⊥ ∩ b⊥ )
159	157, 158	ax-r2 36	. . . . . . . 8 (((a⊥ ∪ b) ∩ (b⊥ ∪ a)) ∩ (b⊥ ∩ a⊥ )) = (a⊥ ∩ b⊥ )
160	148, 159	ax-r2 36	. . . . . . 7 (((a⊥ ∪ b) ∩ b⊥ ) ∩ ((b⊥ ∪ a) ∩ a⊥ )) = (a⊥ ∩ b⊥ )
161	147, 160	2or 72	. . . . . 6 ((((a⊥ ∪ b) ∩ b⊥ ) ∩ ((b ∩ a) ∪ (b⊥ ∩ a))) ∪ (((a⊥ ∪ b) ∩ b⊥ ) ∩ ((b⊥ ∪ a) ∩ a⊥ ))) = (0 ∪ (a⊥ ∩ b⊥ ))
162		ax-a2 31	. . . . . . 7 (0 ∪ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b⊥ ) ∪ 0)
163		or0 102	. . . . . . 7 ((a⊥ ∩ b⊥ ) ∪ 0) = (a⊥ ∩ b⊥ )
164	162, 163	ax-r2 36	. . . . . 6 (0 ∪ (a⊥ ∩ b⊥ )) = (a⊥ ∩ b⊥ )
165	161, 164	ax-r2 36	. . . . 5 ((((a⊥ ∪ b) ∩ b⊥ ) ∩ ((b ∩ a) ∪ (b⊥ ∩ a))) ∪ (((a⊥ ∪ b) ∩ b⊥ ) ∩ ((b⊥ ∪ a) ∩ a⊥ ))) = (a⊥ ∩ b⊥ )
166	128, 165	ax-r2 36	. . . 4 (((a⊥ ∪ b) ∩ b⊥ ) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ ))) = (a⊥ ∩ b⊥ )
167	100, 166	2or 72	. . 3 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ ))) ∪ (((a⊥ ∪ b) ∩ b⊥ ) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ )))) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
168	34, 167	ax-r2 36	. 2 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ )) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ ))) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
169	3, 168	ax-r2 36	1 ((a →4 b) ∩ (b →4 a)) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  0wf 9   →₄ wi4 15

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

This theorem is referenced by:  ud4lem1  581  u4lembi  724