Theorem ud4lem1b 560

Description: Lemma for unified disjunction.

Assertion

Ref	Expression
ud4lem1b	((a →4 b)⊥ ∩ (b →4 a)) = (a ∩ b⊥ )

Proof of Theorem ud4lem1b

Step	Hyp	Ref	Expression
1		ud4lem0c 272	. . 3 (a →4 b)⊥ = (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b))
2		df-i4 46	. . 3 (b →4 a) = (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ ))
3	1, 2	2an 72	. 2 ((a →4 b)⊥ ∩ (b →4 a)) = ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ )))
4		coman2 178	. . . . . . . . . . 11 (b ∩ a) C a
5	4	comcom2 175	. . . . . . . . . 10 (b ∩ a) C a⊥
6		coman1 177	. . . . . . . . . . 11 (b ∩ a) C b
7	6	comcom2 175	. . . . . . . . . 10 (b ∩ a) C b⊥
8	5, 7	com2or 465	. . . . . . . . 9 (b ∩ a) C (a⊥ ∪ b⊥ )
9	8	comcom 435	. . . . . . . 8 (a⊥ ∪ b⊥ ) C (b ∩ a)
10		coman2 178	. . . . . . . . . . 11 (b⊥ ∩ a) C a
11	10	comcom2 175	. . . . . . . . . 10 (b⊥ ∩ a) C a⊥
12		coman1 177	. . . . . . . . . 10 (b⊥ ∩ a) C b⊥
13	11, 12	com2or 465	. . . . . . . . 9 (b⊥ ∩ a) C (a⊥ ∪ b⊥ )
14	13	comcom 435	. . . . . . . 8 (a⊥ ∪ b⊥ ) C (b⊥ ∩ a)
15	9, 14	com2or 465	. . . . . . 7 (a⊥ ∪ b⊥ ) C ((b ∩ a) ∪ (b⊥ ∩ a))
16	15	comcom 435	. . . . . 6 ((b ∩ a) ∪ (b⊥ ∩ a)) C (a⊥ ∪ b⊥ )
17	4, 7	com2or 465	. . . . . . . . 9 (b ∩ a) C (a ∪ b⊥ )
18	17	comcom 435	. . . . . . . 8 (a ∪ b⊥ ) C (b ∩ a)
19		comor2 444	. . . . . . . . 9 (a ∪ b⊥ ) C b⊥
20		comor1 443	. . . . . . . . 9 (a ∪ b⊥ ) C a
21	19, 20	com2an 466	. . . . . . . 8 (a ∪ b⊥ ) C (b⊥ ∩ a)
22	18, 21	com2or 465	. . . . . . 7 (a ∪ b⊥ ) C ((b ∩ a) ∪ (b⊥ ∩ a))
23	22	comcom 435	. . . . . 6 ((b ∩ a) ∪ (b⊥ ∩ a)) C (a ∪ b⊥ )
24	16, 23	com2an 466	. . . . 5 ((b ∩ a) ∪ (b⊥ ∩ a)) C ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ ))
25		coman2 178	. . . . . . . . . . 11 (a ∩ b⊥ ) C b⊥
26	25	comcom3 436	. . . . . . . . . 10 (a ∩ b⊥ )⊥ C b⊥
27	26	comcom5 440	. . . . . . . . 9 (a ∩ b⊥ ) C b
28		coman1 177	. . . . . . . . 9 (a ∩ b⊥ ) C a
29	27, 28	com2an 466	. . . . . . . 8 (a ∩ b⊥ ) C (b ∩ a)
30	25, 28	com2an 466	. . . . . . . 8 (a ∩ b⊥ ) C (b⊥ ∩ a)
31	29, 30	com2or 465	. . . . . . 7 (a ∩ b⊥ ) C ((b ∩ a) ∪ (b⊥ ∩ a))
32	31	comcom 435	. . . . . 6 ((b ∩ a) ∪ (b⊥ ∩ a)) C (a ∩ b⊥ )
33	6	comcom 435	. . . . . . . 8 b C (b ∩ a)
34	12	comcom 435	. . . . . . . . . 10 b⊥ C (b⊥ ∩ a)
35	34	comcom2 175	. . . . . . . . 9 b⊥ C (b⊥ ∩ a)⊥
36	35	comcom5 440	. . . . . . . 8 b C (b⊥ ∩ a)
37	33, 36	com2or 465	. . . . . . 7 b C ((b ∩ a) ∪ (b⊥ ∩ a))
38	37	comcom 435	. . . . . 6 ((b ∩ a) ∪ (b⊥ ∩ a)) C b
39	32, 38	com2or 465	. . . . 5 ((b ∩ a) ∪ (b⊥ ∩ a)) C ((a ∩ b⊥ ) ∪ b)
40	24, 39	com2an 466	. . . 4 ((b ∩ a) ∪ (b⊥ ∩ a)) C (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b))
41		comor1 443	. . . . . . . . . 10 (b⊥ ∪ a) C b⊥
42	41	comcom3 436	. . . . . . . . 9 (b⊥ ∪ a)⊥ C b⊥
43	42	comcom5 440	. . . . . . . 8 (b⊥ ∪ a) C b
44		comor2 444	. . . . . . . 8 (b⊥ ∪ a) C a
45	43, 44	com2an 466	. . . . . . 7 (b⊥ ∪ a) C (b ∩ a)
46	41, 44	com2an 466	. . . . . . 7 (b⊥ ∪ a) C (b⊥ ∩ a)
47	45, 46	com2or 465	. . . . . 6 (b⊥ ∪ a) C ((b ∩ a) ∪ (b⊥ ∩ a))
48	47	comcom 435	. . . . 5 ((b ∩ a) ∪ (b⊥ ∩ a)) C (b⊥ ∪ a)
49	4	comcom 435	. . . . . . . 8 a C (b ∩ a)
50	10	comcom 435	. . . . . . . 8 a C (b⊥ ∩ a)
51	49, 50	com2or 465	. . . . . . 7 a C ((b ∩ a) ∪ (b⊥ ∩ a))
52	51	comcom 435	. . . . . 6 ((b ∩ a) ∪ (b⊥ ∩ a)) C a
53	52	comcom2 175	. . . . 5 ((b ∩ a) ∪ (b⊥ ∩ a)) C a⊥
54	48, 53	com2an 466	. . . 4 ((b ∩ a) ∪ (b⊥ ∩ a)) C ((b⊥ ∪ a) ∩ a⊥ )
55	40, 54	fh2 452	. . 3 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ ))) = (((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ ((b ∩ a) ∪ (b⊥ ∩ a))) ∪ ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ ((b⊥ ∪ a) ∩ a⊥ )))
56	8, 17	com2an 466	. . . . . . . 8 (b ∩ a) C ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ ))
57	4, 7	com2an 466	. . . . . . . . 9 (b ∩ a) C (a ∩ b⊥ )
58	57, 6	com2or 465	. . . . . . . 8 (b ∩ a) C ((a ∩ b⊥ ) ∪ b)
59	56, 58	com2an 466	. . . . . . 7 (b ∩ a) C (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b))
60	7, 4	com2an 466	. . . . . . 7 (b ∩ a) C (b⊥ ∩ a)
61	59, 60	fh2 452	. . . . . 6 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ ((b ∩ a) ∪ (b⊥ ∩ a))) = (((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (b ∩ a)) ∪ ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (b⊥ ∩ a)))
62		an32 76	. . . . . . . . . 10 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (b ∩ a)) = ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (b ∩ a)) ∩ ((a ∩ b⊥ ) ∪ b))
63		an32 76	. . . . . . . . . . . . 13 (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (b ∩ a)) = (((a⊥ ∪ b⊥ ) ∩ (b ∩ a)) ∩ (a ∪ b⊥ ))
64		ax-a2 30	. . . . . . . . . . . . . . . . 17 (a⊥ ∪ b⊥ ) = (b⊥ ∪ a⊥ )
65		df-a 39	. . . . . . . . . . . . . . . . 17 (b ∩ a) = (b⊥ ∪ a⊥ )⊥
66	64, 65	2an 72	. . . . . . . . . . . . . . . 16 ((a⊥ ∪ b⊥ ) ∩ (b ∩ a)) = ((b⊥ ∪ a⊥ ) ∩ (b⊥ ∪ a⊥ )⊥ )
67		dff 93	. . . . . . . . . . . . . . . . 17 0 = ((b⊥ ∪ a⊥ ) ∩ (b⊥ ∪ a⊥ )⊥ )
68	67	ax-r1 34	. . . . . . . . . . . . . . . 16 ((b⊥ ∪ a⊥ ) ∩ (b⊥ ∪ a⊥ )⊥ ) = 0
69	66, 68	ax-r2 35	. . . . . . . . . . . . . . 15 ((a⊥ ∪ b⊥ ) ∩ (b ∩ a)) = 0
70	69	ran 71	. . . . . . . . . . . . . 14 (((a⊥ ∪ b⊥ ) ∩ (b ∩ a)) ∩ (a ∪ b⊥ )) = (0 ∩ (a ∪ b⊥ ))
71		ancom 68	. . . . . . . . . . . . . . 15 (0 ∩ (a ∪ b⊥ )) = ((a ∪ b⊥ ) ∩ 0)
72		an0 100	. . . . . . . . . . . . . . 15 ((a ∪ b⊥ ) ∩ 0) = 0
73	71, 72	ax-r2 35	. . . . . . . . . . . . . 14 (0 ∩ (a ∪ b⊥ )) = 0
74	70, 73	ax-r2 35	. . . . . . . . . . . . 13 (((a⊥ ∪ b⊥ ) ∩ (b ∩ a)) ∩ (a ∪ b⊥ )) = 0
75	63, 74	ax-r2 35	. . . . . . . . . . . 12 (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (b ∩ a)) = 0
76	75	ran 71	. . . . . . . . . . 11 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (b ∩ a)) ∩ ((a ∩ b⊥ ) ∪ b)) = (0 ∩ ((a ∩ b⊥ ) ∪ b))
77		ancom 68	. . . . . . . . . . . 12 (0 ∩ ((a ∩ b⊥ ) ∪ b)) = (((a ∩ b⊥ ) ∪ b) ∩ 0)
78		an0 100	. . . . . . . . . . . 12 (((a ∩ b⊥ ) ∪ b) ∩ 0) = 0
79	77, 78	ax-r2 35	. . . . . . . . . . 11 (0 ∩ ((a ∩ b⊥ ) ∪ b)) = 0
80	76, 79	ax-r2 35	. . . . . . . . . 10 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (b ∩ a)) ∩ ((a ∩ b⊥ ) ∪ b)) = 0
81	62, 80	ax-r2 35	. . . . . . . . 9 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (b ∩ a)) = 0
82		lea 152	. . . . . . . . . . . . . 14 (b⊥ ∩ a) ≤ b⊥
83		leor 151	. . . . . . . . . . . . . 14 b⊥ ≤ (a⊥ ∪ b⊥ )
84	82, 83	letr 129	. . . . . . . . . . . . 13 (b⊥ ∩ a) ≤ (a⊥ ∪ b⊥ )
85		lear 153	. . . . . . . . . . . . . 14 (b⊥ ∩ a) ≤ a
86		leo 150	. . . . . . . . . . . . . 14 a ≤ (a ∪ b⊥ )
87	85, 86	letr 129	. . . . . . . . . . . . 13 (b⊥ ∩ a) ≤ (a ∪ b⊥ )
88	84, 87	ler2an 165	. . . . . . . . . . . 12 (b⊥ ∩ a) ≤ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ ))
89		ancom 68	. . . . . . . . . . . . 13 (b⊥ ∩ a) = (a ∩ b⊥ )
90		leo 150	. . . . . . . . . . . . 13 (a ∩ b⊥ ) ≤ ((a ∩ b⊥ ) ∪ b)
91	89, 90	bltr 130	. . . . . . . . . . . 12 (b⊥ ∩ a) ≤ ((a ∩ b⊥ ) ∪ b)
92	88, 91	ler2an 165	. . . . . . . . . . 11 (b⊥ ∩ a) ≤ (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b))
93	92	df2le2 128	. . . . . . . . . 10 ((b⊥ ∩ a) ∩ (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b))) = (b⊥ ∩ a)
94		ancom 68	. . . . . . . . . 10 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (b⊥ ∩ a)) = ((b⊥ ∩ a) ∩ (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)))
95		ancom 68	. . . . . . . . . 10 (a ∩ b⊥ ) = (b⊥ ∩ a)
96	93, 94, 95	3tr1 60	. . . . . . . . 9 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (b⊥ ∩ a)) = (a ∩ b⊥ )
97	81, 96	2or 67	. . . . . . . 8 (((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (b ∩ a)) ∪ ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (b⊥ ∩ a))) = (0 ∪ (a ∩ b⊥ ))
98		ax-a2 30	. . . . . . . 8 (0 ∪ (a ∩ b⊥ )) = ((a ∩ b⊥ ) ∪ 0)
99	97, 98	ax-r2 35	. . . . . . 7 (((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (b ∩ a)) ∪ ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (b⊥ ∩ a))) = ((a ∩ b⊥ ) ∪ 0)
100		or0 94	. . . . . . 7 ((a ∩ b⊥ ) ∪ 0) = (a ∩ b⊥ )
101	99, 100	ax-r2 35	. . . . . 6 (((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (b ∩ a)) ∪ ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (b⊥ ∩ a))) = (a ∩ b⊥ )
102	61, 101	ax-r2 35	. . . . 5 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ ((b ∩ a) ∪ (b⊥ ∩ a))) = (a ∩ b⊥ )
103		anass 69	. . . . . 6 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ ((b⊥ ∪ a) ∩ a⊥ )) = (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (((a ∩ b⊥ ) ∪ b) ∩ ((b⊥ ∪ a) ∩ a⊥ )))
104	25, 28	com2or 465	. . . . . . . . . . 11 (a ∩ b⊥ ) C (b⊥ ∪ a)
105	28	comcom2 175	. . . . . . . . . . 11 (a ∩ b⊥ ) C a⊥
106	104, 105	com2an 466	. . . . . . . . . 10 (a ∩ b⊥ ) C ((b⊥ ∪ a) ∩ a⊥ )
107	106, 27	fh2r 456	. . . . . . . . 9 (((a ∩ b⊥ ) ∪ b) ∩ ((b⊥ ∪ a) ∩ a⊥ )) = (((a ∩ b⊥ ) ∩ ((b⊥ ∪ a) ∩ a⊥ )) ∪ (b ∩ ((b⊥ ∪ a) ∩ a⊥ )))
108		an12 74	. . . . . . . . . . . 12 ((a ∩ b⊥ ) ∩ ((b⊥ ∪ a) ∩ a⊥ )) = ((b⊥ ∪ a) ∩ ((a ∩ b⊥ ) ∩ a⊥ ))
109		an32 76	. . . . . . . . . . . . . . 15 ((a ∩ b⊥ ) ∩ a⊥ ) = ((a ∩ a⊥ ) ∩ b⊥ )
110		ancom 68	. . . . . . . . . . . . . . . 16 ((a ∩ a⊥ ) ∩ b⊥ ) = (b⊥ ∩ (a ∩ a⊥ ))
111		dff 93	. . . . . . . . . . . . . . . . . . 19 0 = (a ∩ a⊥ )
112	111	ax-r1 34	. . . . . . . . . . . . . . . . . 18 (a ∩ a⊥ ) = 0
113	112	lan 70	. . . . . . . . . . . . . . . . 17 (b⊥ ∩ (a ∩ a⊥ )) = (b⊥ ∩ 0)
114		an0 100	. . . . . . . . . . . . . . . . 17 (b⊥ ∩ 0) = 0
115	113, 114	ax-r2 35	. . . . . . . . . . . . . . . 16 (b⊥ ∩ (a ∩ a⊥ )) = 0
116	110, 115	ax-r2 35	. . . . . . . . . . . . . . 15 ((a ∩ a⊥ ) ∩ b⊥ ) = 0
117	109, 116	ax-r2 35	. . . . . . . . . . . . . 14 ((a ∩ b⊥ ) ∩ a⊥ ) = 0
118	117	lan 70	. . . . . . . . . . . . 13 ((b⊥ ∪ a) ∩ ((a ∩ b⊥ ) ∩ a⊥ )) = ((b⊥ ∪ a) ∩ 0)
119		an0 100	. . . . . . . . . . . . 13 ((b⊥ ∪ a) ∩ 0) = 0
120	118, 119	ax-r2 35	. . . . . . . . . . . 12 ((b⊥ ∪ a) ∩ ((a ∩ b⊥ ) ∩ a⊥ )) = 0
121	108, 120	ax-r2 35	. . . . . . . . . . 11 ((a ∩ b⊥ ) ∩ ((b⊥ ∪ a) ∩ a⊥ )) = 0
122		anor1 80	. . . . . . . . . . . . 13 (b ∩ a⊥ ) = (b⊥ ∪ a)⊥
123	122	lan 70	. . . . . . . . . . . 12 ((b⊥ ∪ a) ∩ (b ∩ a⊥ )) = ((b⊥ ∪ a) ∩ (b⊥ ∪ a)⊥ )
124		an12 74	. . . . . . . . . . . 12 (b ∩ ((b⊥ ∪ a) ∩ a⊥ )) = ((b⊥ ∪ a) ∩ (b ∩ a⊥ ))
125		dff 93	. . . . . . . . . . . 12 0 = ((b⊥ ∪ a) ∩ (b⊥ ∪ a)⊥ )
126	123, 124, 125	3tr1 60	. . . . . . . . . . 11 (b ∩ ((b⊥ ∪ a) ∩ a⊥ )) = 0
127	121, 126	2or 67	. . . . . . . . . 10 (((a ∩ b⊥ ) ∩ ((b⊥ ∪ a) ∩ a⊥ )) ∪ (b ∩ ((b⊥ ∪ a) ∩ a⊥ ))) = (0 ∪ 0)
128		or0 94	. . . . . . . . . 10 (0 ∪ 0) = 0
129	127, 128	ax-r2 35	. . . . . . . . 9 (((a ∩ b⊥ ) ∩ ((b⊥ ∪ a) ∩ a⊥ )) ∪ (b ∩ ((b⊥ ∪ a) ∩ a⊥ ))) = 0
130	107, 129	ax-r2 35	. . . . . . . 8 (((a ∩ b⊥ ) ∪ b) ∩ ((b⊥ ∪ a) ∩ a⊥ )) = 0
131	130	lan 70	. . . . . . 7 (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (((a ∩ b⊥ ) ∪ b) ∩ ((b⊥ ∪ a) ∩ a⊥ ))) = (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ 0)
132		an0 100	. . . . . . 7 (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ 0) = 0
133	131, 132	ax-r2 35	. . . . . 6 (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (((a ∩ b⊥ ) ∪ b) ∩ ((b⊥ ∪ a) ∩ a⊥ ))) = 0
134	103, 133	ax-r2 35	. . . . 5 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ ((b⊥ ∪ a) ∩ a⊥ )) = 0
135	102, 134	2or 67	. . . 4 (((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ ((b ∩ a) ∪ (b⊥ ∩ a))) ∪ ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ ((b⊥ ∪ a) ∩ a⊥ ))) = ((a ∩ b⊥ ) ∪ 0)
136	135, 100	ax-r2 35	. . 3 (((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ ((b ∩ a) ∪ (b⊥ ∩ a))) ∪ ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ ((b⊥ ∪ a) ∩ a⊥ ))) = (a ∩ b⊥ )
137	55, 136	ax-r2 35	. 2 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∩ b⊥ ) ∪ b)) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b⊥ ∪ a) ∩ a⊥ ))) = (a ∩ b⊥ )
138	3, 137	ax-r2 35	1 ((a →4 b)⊥ ∩ (b →4 a)) = (a ∩ b⊥ )

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

This theorem is referenced by:  ud4lem1 563

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i4 46  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org