Theorem ud3lem1a 566

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

Assertion

Ref	Expression
ud3lem1a	((a →3 b)⊥ ∩ (b →3 a)) = (a ∩ b⊥ )

Proof of Theorem ud3lem1a

Step	Hyp	Ref	Expression
1		ud3lem0c 279	. . 3 (a →3 b)⊥ = (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ )))
2		df-i3 46	. . 3 (b →3 a) = (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))
3	1, 2	2an 79	. 2 ((a →3 b)⊥ ∩ (b →3 a)) = ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a))))
4		comor2 462	. . . . . . . . 9 (a ∪ b⊥ ) C b⊥
5		comor1 461	. . . . . . . . 9 (a ∪ b⊥ ) C a
6	4, 5	com2an 484	. . . . . . . 8 (a ∪ b⊥ ) C (b⊥ ∩ a)
7	5	comcom2 183	. . . . . . . . 9 (a ∪ b⊥ ) C a⊥
8	4, 7	com2an 484	. . . . . . . 8 (a ∪ b⊥ ) C (b⊥ ∩ a⊥ )
9	6, 8	com2or 483	. . . . . . 7 (a ∪ b⊥ ) C ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ ))
10	9	comcom 453	. . . . . 6 ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) C (a ∪ b⊥ )
11		comor2 462	. . . . . . . . . 10 (a ∪ b) C b
12	11	comcom2 183	. . . . . . . . 9 (a ∪ b) C b⊥
13		comor1 461	. . . . . . . . 9 (a ∪ b) C a
14	12, 13	com2an 484	. . . . . . . 8 (a ∪ b) C (b⊥ ∩ a)
15	13	comcom2 183	. . . . . . . . 9 (a ∪ b) C a⊥
16	12, 15	com2an 484	. . . . . . . 8 (a ∪ b) C (b⊥ ∩ a⊥ )
17	14, 16	com2or 483	. . . . . . 7 (a ∪ b) C ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ ))
18	17	comcom 453	. . . . . 6 ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) C (a ∪ b)
19	10, 18	com2an 484	. . . . 5 ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) C ((a ∪ b⊥ ) ∩ (a ∪ b))
20		comanr2 465	. . . . . . . . 9 a C (b⊥ ∩ a)
21	20	comcom3 454	. . . . . . . 8 a⊥ C (b⊥ ∩ a)
22		comanr2 465	. . . . . . . 8 a⊥ C (b⊥ ∩ a⊥ )
23	21, 22	com2or 483	. . . . . . 7 a⊥ C ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ ))
24	23	comcom 453	. . . . . 6 ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) C a⊥
25		coman2 186	. . . . . . . . 9 (a ∩ b⊥ ) C b⊥
26		coman1 185	. . . . . . . . 9 (a ∩ b⊥ ) C a
27	25, 26	com2an 484	. . . . . . . 8 (a ∩ b⊥ ) C (b⊥ ∩ a)
28	26	comcom2 183	. . . . . . . . 9 (a ∩ b⊥ ) C a⊥
29	25, 28	com2an 484	. . . . . . . 8 (a ∩ b⊥ ) C (b⊥ ∩ a⊥ )
30	27, 29	com2or 483	. . . . . . 7 (a ∩ b⊥ ) C ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ ))
31	30	comcom 453	. . . . . 6 ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) C (a ∩ b⊥ )
32	24, 31	com2or 483	. . . . 5 ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) C (a⊥ ∪ (a ∩ b⊥ ))
33	19, 32	com2an 484	. . . 4 ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) C (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ )))
34		comanr1 464	. . . . . . . 8 b⊥ C (b⊥ ∩ a)
35	34	comcom6 459	. . . . . . 7 b C (b⊥ ∩ a)
36		comanr1 464	. . . . . . . 8 b⊥ C (b⊥ ∩ a⊥ )
37	36	comcom6 459	. . . . . . 7 b C (b⊥ ∩ a⊥ )
38	35, 37	com2or 483	. . . . . 6 b C ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ ))
39	38	comcom 453	. . . . 5 ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) C b
40		comor1 461	. . . . . . . 8 (b⊥ ∪ a) C b⊥
41		comor2 462	. . . . . . . 8 (b⊥ ∪ a) C a
42	40, 41	com2an 484	. . . . . . 7 (b⊥ ∪ a) C (b⊥ ∩ a)
43	41	comcom2 183	. . . . . . . 8 (b⊥ ∪ a) C a⊥
44	40, 43	com2an 484	. . . . . . 7 (b⊥ ∪ a) C (b⊥ ∩ a⊥ )
45	42, 44	com2or 483	. . . . . 6 (b⊥ ∪ a) C ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ ))
46	45	comcom 453	. . . . 5 ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) C (b⊥ ∪ a)
47	39, 46	com2an 484	. . . 4 ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) C (b ∩ (b⊥ ∪ a))
48	33, 47	fh2 470	. . 3 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) = (((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ ))) ∪ ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (b ∩ (b⊥ ∪ a))))
49		coman2 186	. . . . . . . . . 10 (b⊥ ∩ a) C a
50		coman1 185	. . . . . . . . . 10 (b⊥ ∩ a) C b⊥
51	49, 50	com2or 483	. . . . . . . . 9 (b⊥ ∩ a) C (a ∪ b⊥ )
52	50	comcom7 460	. . . . . . . . . 10 (b⊥ ∩ a) C b
53	49, 52	com2or 483	. . . . . . . . 9 (b⊥ ∩ a) C (a ∪ b)
54	51, 53	com2an 484	. . . . . . . 8 (b⊥ ∩ a) C ((a ∪ b⊥ ) ∩ (a ∪ b))
55	49	comcom2 183	. . . . . . . . 9 (b⊥ ∩ a) C a⊥
56	49, 50	com2an 484	. . . . . . . . 9 (b⊥ ∩ a) C (a ∩ b⊥ )
57	55, 56	com2or 483	. . . . . . . 8 (b⊥ ∩ a) C (a⊥ ∪ (a ∩ b⊥ ))
58	54, 57	com2an 484	. . . . . . 7 (b⊥ ∩ a) C (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ )))
59	50, 55	com2an 484	. . . . . . 7 (b⊥ ∩ a) C (b⊥ ∩ a⊥ )
60	58, 59	fh2 470	. . . . . 6 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ ))) = (((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (b⊥ ∩ a)) ∪ ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (b⊥ ∩ a⊥ )))
61		anass 76	. . . . . . . . 9 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (b⊥ ∩ a)) = (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ ((a⊥ ∪ (a ∩ b⊥ )) ∩ (b⊥ ∩ a)))
62		ancom 74	. . . . . . . . . . . 12 ((a⊥ ∪ (a ∩ b⊥ )) ∩ (b⊥ ∩ a)) = ((b⊥ ∩ a) ∩ (a⊥ ∪ (a ∩ b⊥ )))
63		ancom 74	. . . . . . . . . . . . . 14 (b⊥ ∩ a) = (a ∩ b⊥ )
64		ax-a2 31	. . . . . . . . . . . . . 14 (a⊥ ∪ (a ∩ b⊥ )) = ((a ∩ b⊥ ) ∪ a⊥ )
65	63, 64	2an 79	. . . . . . . . . . . . 13 ((b⊥ ∩ a) ∩ (a⊥ ∪ (a ∩ b⊥ ))) = ((a ∩ b⊥ ) ∩ ((a ∩ b⊥ ) ∪ a⊥ ))
66		anabs 121	. . . . . . . . . . . . 13 ((a ∩ b⊥ ) ∩ ((a ∩ b⊥ ) ∪ a⊥ )) = (a ∩ b⊥ )
67	65, 66	ax-r2 36	. . . . . . . . . . . 12 ((b⊥ ∩ a) ∩ (a⊥ ∪ (a ∩ b⊥ ))) = (a ∩ b⊥ )
68	62, 67	ax-r2 36	. . . . . . . . . . 11 ((a⊥ ∪ (a ∩ b⊥ )) ∩ (b⊥ ∩ a)) = (a ∩ b⊥ )
69	68	lan 77	. . . . . . . . . 10 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ ((a⊥ ∪ (a ∩ b⊥ )) ∩ (b⊥ ∩ a))) = (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a ∩ b⊥ ))
70		ancom 74	. . . . . . . . . . 11 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a ∩ b⊥ )) = ((a ∩ b⊥ ) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b)))
71		lea 160	. . . . . . . . . . . . 13 (a ∩ b⊥ ) ≤ a
72		leo 158	. . . . . . . . . . . . . 14 a ≤ (a ∪ b⊥ )
73		leo 158	. . . . . . . . . . . . . 14 a ≤ (a ∪ b)
74	72, 73	ler2an 173	. . . . . . . . . . . . 13 a ≤ ((a ∪ b⊥ ) ∩ (a ∪ b))
75	71, 74	letr 137	. . . . . . . . . . . 12 (a ∩ b⊥ ) ≤ ((a ∪ b⊥ ) ∩ (a ∪ b))
76	75	df2le2 136	. . . . . . . . . . 11 ((a ∩ b⊥ ) ∩ ((a ∪ b⊥ ) ∩ (a ∪ b))) = (a ∩ b⊥ )
77	70, 76	ax-r2 36	. . . . . . . . . 10 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a ∩ b⊥ )) = (a ∩ b⊥ )
78	69, 77	ax-r2 36	. . . . . . . . 9 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ ((a⊥ ∪ (a ∩ b⊥ )) ∩ (b⊥ ∩ a))) = (a ∩ b⊥ )
79	61, 78	ax-r2 36	. . . . . . . 8 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (b⊥ ∩ a)) = (a ∩ b⊥ )
80		an32 83	. . . . . . . . 9 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (b⊥ ∩ a⊥ )) = ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (b⊥ ∩ a⊥ )) ∩ (a⊥ ∪ (a ∩ b⊥ )))
81		anass 76	. . . . . . . . . . . 12 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (b⊥ ∩ a⊥ )) = ((a ∪ b⊥ ) ∩ ((a ∪ b) ∩ (b⊥ ∩ a⊥ )))
82		ax-a2 31	. . . . . . . . . . . . . . . 16 (a ∪ b) = (b ∪ a)
83		oran 87	. . . . . . . . . . . . . . . . . 18 (b ∪ a) = (b⊥ ∩ a⊥ )⊥
84	83	ax-r1 35	. . . . . . . . . . . . . . . . 17 (b⊥ ∩ a⊥ )⊥ = (b ∪ a)
85	84	con3 68	. . . . . . . . . . . . . . . 16 (b⊥ ∩ a⊥ ) = (b ∪ a)⊥
86	82, 85	2an 79	. . . . . . . . . . . . . . 15 ((a ∪ b) ∩ (b⊥ ∩ a⊥ )) = ((b ∪ a) ∩ (b ∪ a)⊥ )
87		dff 101	. . . . . . . . . . . . . . . 16 0 = ((b ∪ a) ∩ (b ∪ a)⊥ )
88	87	ax-r1 35	. . . . . . . . . . . . . . 15 ((b ∪ a) ∩ (b ∪ a)⊥ ) = 0
89	86, 88	ax-r2 36	. . . . . . . . . . . . . 14 ((a ∪ b) ∩ (b⊥ ∩ a⊥ )) = 0
90	89	lan 77	. . . . . . . . . . . . 13 ((a ∪ b⊥ ) ∩ ((a ∪ b) ∩ (b⊥ ∩ a⊥ ))) = ((a ∪ b⊥ ) ∩ 0)
91		an0 108	. . . . . . . . . . . . 13 ((a ∪ b⊥ ) ∩ 0) = 0
92	90, 91	ax-r2 36	. . . . . . . . . . . 12 ((a ∪ b⊥ ) ∩ ((a ∪ b) ∩ (b⊥ ∩ a⊥ ))) = 0
93	81, 92	ax-r2 36	. . . . . . . . . . 11 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (b⊥ ∩ a⊥ )) = 0
94	93	ran 78	. . . . . . . . . 10 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (b⊥ ∩ a⊥ )) ∩ (a⊥ ∪ (a ∩ b⊥ ))) = (0 ∩ (a⊥ ∪ (a ∩ b⊥ )))
95		an0r 109	. . . . . . . . . 10 (0 ∩ (a⊥ ∪ (a ∩ b⊥ ))) = 0
96	94, 95	ax-r2 36	. . . . . . . . 9 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (b⊥ ∩ a⊥ )) ∩ (a⊥ ∪ (a ∩ b⊥ ))) = 0
97	80, 96	ax-r2 36	. . . . . . . 8 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (b⊥ ∩ a⊥ )) = 0
98	79, 97	2or 72	. . . . . . 7 (((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (b⊥ ∩ a)) ∪ ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (b⊥ ∩ a⊥ ))) = ((a ∩ b⊥ ) ∪ 0)
99		or0 102	. . . . . . 7 ((a ∩ b⊥ ) ∪ 0) = (a ∩ b⊥ )
100	98, 99	ax-r2 36	. . . . . 6 (((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (b⊥ ∩ a)) ∪ ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (b⊥ ∩ a⊥ ))) = (a ∩ b⊥ )
101	60, 100	ax-r2 36	. . . . 5 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ ))) = (a ∩ b⊥ )
102		anass 76	. . . . . 6 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (b ∩ (b⊥ ∪ a))) = (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ ((a⊥ ∪ (a ∩ b⊥ )) ∩ (b ∩ (b⊥ ∪ a))))
103		anass 76	. . . . . . . . . 10 (((a⊥ ∪ (a ∩ b⊥ )) ∩ b) ∩ (b⊥ ∪ a)) = ((a⊥ ∪ (a ∩ b⊥ )) ∩ (b ∩ (b⊥ ∪ a)))
104	103	ax-r1 35	. . . . . . . . 9 ((a⊥ ∪ (a ∩ b⊥ )) ∩ (b ∩ (b⊥ ∪ a))) = (((a⊥ ∪ (a ∩ b⊥ )) ∩ b) ∩ (b⊥ ∪ a))
105	64	ran 78	. . . . . . . . . . . 12 ((a⊥ ∪ (a ∩ b⊥ )) ∩ b) = (((a ∩ b⊥ ) ∪ a⊥ ) ∩ b)
106	25	comcom7 460	. . . . . . . . . . . . . 14 (a ∩ b⊥ ) C b
107	106, 28	fh2r 474	. . . . . . . . . . . . 13 (((a ∩ b⊥ ) ∪ a⊥ ) ∩ b) = (((a ∩ b⊥ ) ∩ b) ∪ (a⊥ ∩ b))
108		anass 76	. . . . . . . . . . . . . . . 16 ((a ∩ b⊥ ) ∩ b) = (a ∩ (b⊥ ∩ b))
109		ancom 74	. . . . . . . . . . . . . . . . . . 19 (b⊥ ∩ b) = (b ∩ b⊥ )
110		dff 101	. . . . . . . . . . . . . . . . . . . 20 0 = (b ∩ b⊥ )
111	110	ax-r1 35	. . . . . . . . . . . . . . . . . . 19 (b ∩ b⊥ ) = 0
112	109, 111	ax-r2 36	. . . . . . . . . . . . . . . . . 18 (b⊥ ∩ b) = 0
113	112	lan 77	. . . . . . . . . . . . . . . . 17 (a ∩ (b⊥ ∩ b)) = (a ∩ 0)
114		an0 108	. . . . . . . . . . . . . . . . 17 (a ∩ 0) = 0
115	113, 114	ax-r2 36	. . . . . . . . . . . . . . . 16 (a ∩ (b⊥ ∩ b)) = 0
116	108, 115	ax-r2 36	. . . . . . . . . . . . . . 15 ((a ∩ b⊥ ) ∩ b) = 0
117		ancom 74	. . . . . . . . . . . . . . 15 (a⊥ ∩ b) = (b ∩ a⊥ )
118	116, 117	2or 72	. . . . . . . . . . . . . 14 (((a ∩ b⊥ ) ∩ b) ∪ (a⊥ ∩ b)) = (0 ∪ (b ∩ a⊥ ))
119		or0r 103	. . . . . . . . . . . . . 14 (0 ∪ (b ∩ a⊥ )) = (b ∩ a⊥ )
120	118, 119	ax-r2 36	. . . . . . . . . . . . 13 (((a ∩ b⊥ ) ∩ b) ∪ (a⊥ ∩ b)) = (b ∩ a⊥ )
121	107, 120	ax-r2 36	. . . . . . . . . . . 12 (((a ∩ b⊥ ) ∪ a⊥ ) ∩ b) = (b ∩ a⊥ )
122	105, 121	ax-r2 36	. . . . . . . . . . 11 ((a⊥ ∪ (a ∩ b⊥ )) ∩ b) = (b ∩ a⊥ )
123	122	ran 78	. . . . . . . . . 10 (((a⊥ ∪ (a ∩ b⊥ )) ∩ b) ∩ (b⊥ ∪ a)) = ((b ∩ a⊥ ) ∩ (b⊥ ∪ a))
124		anor1 88	. . . . . . . . . . . . . 14 (b ∩ a⊥ ) = (b⊥ ∪ a)⊥
125	124	ax-r1 35	. . . . . . . . . . . . 13 (b⊥ ∪ a)⊥ = (b ∩ a⊥ )
126	125	con3 68	. . . . . . . . . . . 12 (b⊥ ∪ a) = (b ∩ a⊥ )⊥
127	126	lan 77	. . . . . . . . . . 11 ((b ∩ a⊥ ) ∩ (b⊥ ∪ a)) = ((b ∩ a⊥ ) ∩ (b ∩ a⊥ )⊥ )
128		dff 101	. . . . . . . . . . . 12 0 = ((b ∩ a⊥ ) ∩ (b ∩ a⊥ )⊥ )
129	128	ax-r1 35	. . . . . . . . . . 11 ((b ∩ a⊥ ) ∩ (b ∩ a⊥ )⊥ ) = 0
130	127, 129	ax-r2 36	. . . . . . . . . 10 ((b ∩ a⊥ ) ∩ (b⊥ ∪ a)) = 0
131	123, 130	ax-r2 36	. . . . . . . . 9 (((a⊥ ∪ (a ∩ b⊥ )) ∩ b) ∩ (b⊥ ∪ a)) = 0
132	104, 131	ax-r2 36	. . . . . . . 8 ((a⊥ ∪ (a ∩ b⊥ )) ∩ (b ∩ (b⊥ ∪ a))) = 0
133	132	lan 77	. . . . . . 7 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ ((a⊥ ∪ (a ∩ b⊥ )) ∩ (b ∩ (b⊥ ∪ a)))) = (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ 0)
134		an0 108	. . . . . . 7 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ 0) = 0
135	133, 134	ax-r2 36	. . . . . 6 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ ((a⊥ ∪ (a ∩ b⊥ )) ∩ (b ∩ (b⊥ ∪ a)))) = 0
136	102, 135	ax-r2 36	. . . . 5 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (b ∩ (b⊥ ∪ a))) = 0
137	101, 136	2or 72	. . . 4 (((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ ))) ∪ ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (b ∩ (b⊥ ∪ a)))) = ((a ∩ b⊥ ) ∪ 0)
138	137, 99	ax-r2 36	. . 3 (((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ ))) ∪ ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (b ∩ (b⊥ ∪ a)))) = (a ∩ b⊥ )
139	48, 138	ax-r2 36	. 2 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) = (a ∩ b⊥ )
140	3, 139	ax-r2 36	1 ((a →3 b)⊥ ∩ (b →3 a)) = (a ∩ b⊥ )

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  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:  ud3lem1  570