Theorem ud3lem1c 568

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

Assertion

Ref	Expression
ud3lem1c	((a →3 b)⊥ ∪ (b →3 a)) = (a ∪ b⊥ )

Proof of Theorem ud3lem1c

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	2or 72	. 2 ((a →3 b)⊥ ∪ (b →3 a)) = ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a))))
4		coman2 186	. . . . . . . . 9 (b⊥ ∩ a) C a
5		coman1 185	. . . . . . . . 9 (b⊥ ∩ a) C b⊥
6	4, 5	com2or 483	. . . . . . . 8 (b⊥ ∩ a) C (a ∪ b⊥ )
7	5	comcom7 460	. . . . . . . . 9 (b⊥ ∩ a) C b
8	4, 7	com2or 483	. . . . . . . 8 (b⊥ ∩ a) C (a ∪ b)
9	6, 8	com2an 484	. . . . . . 7 (b⊥ ∩ a) C ((a ∪ b⊥ ) ∩ (a ∪ b))
10	9	comcom 453	. . . . . 6 ((a ∪ b⊥ ) ∩ (a ∪ b)) C (b⊥ ∩ a)
11		coman2 186	. . . . . . . . . 10 (b⊥ ∩ a⊥ ) C a⊥
12	11	comcom7 460	. . . . . . . . 9 (b⊥ ∩ a⊥ ) C a
13		coman1 185	. . . . . . . . 9 (b⊥ ∩ a⊥ ) C b⊥
14	12, 13	com2or 483	. . . . . . . 8 (b⊥ ∩ a⊥ ) C (a ∪ b⊥ )
15	13	comcom7 460	. . . . . . . . 9 (b⊥ ∩ a⊥ ) C b
16	12, 15	com2or 483	. . . . . . . 8 (b⊥ ∩ a⊥ ) C (a ∪ b)
17	14, 16	com2an 484	. . . . . . 7 (b⊥ ∩ a⊥ ) C ((a ∪ b⊥ ) ∩ (a ∪ b))
18	17	comcom 453	. . . . . 6 ((a ∪ b⊥ ) ∩ (a ∪ b)) C (b⊥ ∩ a⊥ )
19	10, 18	com2or 483	. . . . 5 ((a ∪ b⊥ ) ∩ (a ∪ b)) C ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ ))
20		comorr2 463	. . . . . . . . 9 b⊥ C (a ∪ b⊥ )
21	20	comcom6 459	. . . . . . . 8 b C (a ∪ b⊥ )
22		comorr2 463	. . . . . . . 8 b C (a ∪ b)
23	21, 22	com2an 484	. . . . . . 7 b C ((a ∪ b⊥ ) ∩ (a ∪ b))
24	23	comcom 453	. . . . . 6 ((a ∪ b⊥ ) ∩ (a ∪ b)) C b
25		comor2 462	. . . . . . . . 9 (b⊥ ∪ a) C a
26		comor1 461	. . . . . . . . 9 (b⊥ ∪ a) C b⊥
27	25, 26	com2or 483	. . . . . . . 8 (b⊥ ∪ a) C (a ∪ b⊥ )
28	26	comcom7 460	. . . . . . . . 9 (b⊥ ∪ a) C b
29	25, 28	com2or 483	. . . . . . . 8 (b⊥ ∪ a) C (a ∪ b)
30	27, 29	com2an 484	. . . . . . 7 (b⊥ ∪ a) C ((a ∪ b⊥ ) ∩ (a ∪ b))
31	30	comcom 453	. . . . . 6 ((a ∪ b⊥ ) ∩ (a ∪ b)) C (b⊥ ∪ a)
32	24, 31	com2an 484	. . . . 5 ((a ∪ b⊥ ) ∩ (a ∪ b)) C (b ∩ (b⊥ ∪ a))
33	19, 32	com2or 483	. . . 4 ((a ∪ b⊥ ) ∩ (a ∪ b)) C (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))
34		comorr 184	. . . . . . . 8 a C (a ∪ b⊥ )
35	34	comcom3 454	. . . . . . 7 a⊥ C (a ∪ b⊥ )
36		comorr 184	. . . . . . . 8 a C (a ∪ b)
37	36	comcom3 454	. . . . . . 7 a⊥ C (a ∪ b)
38	35, 37	com2an 484	. . . . . 6 a⊥ C ((a ∪ b⊥ ) ∩ (a ∪ b))
39	38	comcom 453	. . . . 5 ((a ∪ b⊥ ) ∩ (a ∪ b)) C a⊥
40		coman1 185	. . . . . . . 8 (a ∩ b⊥ ) C a
41		coman2 186	. . . . . . . 8 (a ∩ b⊥ ) C b⊥
42	40, 41	com2or 483	. . . . . . 7 (a ∩ b⊥ ) C (a ∪ b⊥ )
43	41	comcom7 460	. . . . . . . 8 (a ∩ b⊥ ) C b
44	40, 43	com2or 483	. . . . . . 7 (a ∩ b⊥ ) C (a ∪ b)
45	42, 44	com2an 484	. . . . . 6 (a ∩ b⊥ ) C ((a ∪ b⊥ ) ∩ (a ∪ b))
46	45	comcom 453	. . . . 5 ((a ∪ b⊥ ) ∩ (a ∪ b)) C (a ∩ b⊥ )
47	39, 46	com2or 483	. . . 4 ((a ∪ b⊥ ) ∩ (a ∪ b)) C (a⊥ ∪ (a ∩ b⊥ ))
48	33, 47	fh4r 476	. . 3 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) = ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) ∩ ((a⊥ ∪ (a ∩ b⊥ )) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))))
49		comor2 462	. . . . . . . . . 10 (a ∪ b⊥ ) C b⊥
50		comor1 461	. . . . . . . . . 10 (a ∪ b⊥ ) C a
51	49, 50	com2an 484	. . . . . . . . 9 (a ∪ b⊥ ) C (b⊥ ∩ a)
52	50	comcom2 183	. . . . . . . . . 10 (a ∪ b⊥ ) C a⊥
53	49, 52	com2an 484	. . . . . . . . 9 (a ∪ b⊥ ) C (b⊥ ∩ a⊥ )
54	51, 53	com2or 483	. . . . . . . 8 (a ∪ b⊥ ) C ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ ))
55	49	comcom7 460	. . . . . . . . 9 (a ∪ b⊥ ) C b
56	49, 50	com2or 483	. . . . . . . . 9 (a ∪ b⊥ ) C (b⊥ ∪ a)
57	55, 56	com2an 484	. . . . . . . 8 (a ∪ b⊥ ) C (b ∩ (b⊥ ∪ a))
58	54, 57	com2or 483	. . . . . . 7 (a ∪ b⊥ ) C (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))
59	50, 55	com2or 483	. . . . . . 7 (a ∪ b⊥ ) C (a ∪ b)
60	58, 59	fh4r 476	. . . . . 6 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) = (((a ∪ b⊥ ) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) ∩ ((a ∪ b) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))))
61		ax-a2 31	. . . . . . . . 9 ((a ∪ b⊥ ) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) = ((((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a))) ∪ (a ∪ b⊥ ))
62		lea 160	. . . . . . . . . . . . 13 (b⊥ ∩ a) ≤ b⊥
63		lea 160	. . . . . . . . . . . . 13 (b⊥ ∩ a⊥ ) ≤ b⊥
64	62, 63	lel2or 170	. . . . . . . . . . . 12 ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ≤ b⊥
65		leor 159	. . . . . . . . . . . 12 b⊥ ≤ (a ∪ b⊥ )
66	64, 65	letr 137	. . . . . . . . . . 11 ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ≤ (a ∪ b⊥ )
67		lear 161	. . . . . . . . . . . 12 (b ∩ (b⊥ ∪ a)) ≤ (b⊥ ∪ a)
68		ax-a2 31	. . . . . . . . . . . 12 (b⊥ ∪ a) = (a ∪ b⊥ )
69	67, 68	lbtr 139	. . . . . . . . . . 11 (b ∩ (b⊥ ∪ a)) ≤ (a ∪ b⊥ )
70	66, 69	lel2or 170	. . . . . . . . . 10 (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a))) ≤ (a ∪ b⊥ )
71	70	df-le2 131	. . . . . . . . 9 ((((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a))) ∪ (a ∪ b⊥ )) = (a ∪ b⊥ )
72	61, 71	ax-r2 36	. . . . . . . 8 ((a ∪ b⊥ ) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) = (a ∪ b⊥ )
73		or12 80	. . . . . . . . 9 ((a ∪ b) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) = (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ ((a ∪ b) ∪ (b ∩ (b⊥ ∪ a))))
74		ax-a3 32	. . . . . . . . . . 11 ((((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (a ∪ b)) ∪ (b ∩ (b⊥ ∪ a))) = (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ ((a ∪ b) ∪ (b ∩ (b⊥ ∪ a))))
75	74	ax-r1 35	. . . . . . . . . 10 (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ ((a ∪ b) ∪ (b ∩ (b⊥ ∪ a)))) = ((((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (a ∪ b)) ∪ (b ∩ (b⊥ ∪ a)))
76		ax-a3 32	. . . . . . . . . . . . 13 (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (a ∪ b)) = ((b⊥ ∩ a) ∪ ((b⊥ ∩ a⊥ ) ∪ (a ∪ b)))
77		ancom 74	. . . . . . . . . . . . . . . . 17 (b⊥ ∩ a⊥ ) = (a⊥ ∩ b⊥ )
78		oran 87	. . . . . . . . . . . . . . . . 17 (a ∪ b) = (a⊥ ∩ b⊥ )⊥
79	77, 78	2or 72	. . . . . . . . . . . . . . . 16 ((b⊥ ∩ a⊥ ) ∪ (a ∪ b)) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ )⊥ )
80		df-t 41	. . . . . . . . . . . . . . . . 17 1 = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ )⊥ )
81	80	ax-r1 35	. . . . . . . . . . . . . . . 16 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ )⊥ ) = 1
82	79, 81	ax-r2 36	. . . . . . . . . . . . . . 15 ((b⊥ ∩ a⊥ ) ∪ (a ∪ b)) = 1
83	82	lor 70	. . . . . . . . . . . . . 14 ((b⊥ ∩ a) ∪ ((b⊥ ∩ a⊥ ) ∪ (a ∪ b))) = ((b⊥ ∩ a) ∪ 1)
84		or1 104	. . . . . . . . . . . . . 14 ((b⊥ ∩ a) ∪ 1) = 1
85	83, 84	ax-r2 36	. . . . . . . . . . . . 13 ((b⊥ ∩ a) ∪ ((b⊥ ∩ a⊥ ) ∪ (a ∪ b))) = 1
86	76, 85	ax-r2 36	. . . . . . . . . . . 12 (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (a ∪ b)) = 1
87	86	ax-r5 38	. . . . . . . . . . 11 ((((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (a ∪ b)) ∪ (b ∩ (b⊥ ∪ a))) = (1 ∪ (b ∩ (b⊥ ∪ a)))
88		or1r 105	. . . . . . . . . . 11 (1 ∪ (b ∩ (b⊥ ∪ a))) = 1
89	87, 88	ax-r2 36	. . . . . . . . . 10 ((((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (a ∪ b)) ∪ (b ∩ (b⊥ ∪ a))) = 1
90	75, 89	ax-r2 36	. . . . . . . . 9 (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ ((a ∪ b) ∪ (b ∩ (b⊥ ∪ a)))) = 1
91	73, 90	ax-r2 36	. . . . . . . 8 ((a ∪ b) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) = 1
92	72, 91	2an 79	. . . . . . 7 (((a ∪ b⊥ ) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) ∩ ((a ∪ b) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a))))) = ((a ∪ b⊥ ) ∩ 1)
93		an1 106	. . . . . . 7 ((a ∪ b⊥ ) ∩ 1) = (a ∪ b⊥ )
94	92, 93	ax-r2 36	. . . . . 6 (((a ∪ b⊥ ) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) ∩ ((a ∪ b) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a))))) = (a ∪ b⊥ )
95	60, 94	ax-r2 36	. . . . 5 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) = (a ∪ b⊥ )
96		or12 80	. . . . . 6 ((a⊥ ∪ (a ∩ b⊥ )) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) = (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ ((a⊥ ∪ (a ∩ b⊥ )) ∪ (b ∩ (b⊥ ∪ a))))
97		ax-a2 31	. . . . . . . . . 10 (a⊥ ∪ (a ∩ b⊥ )) = ((a ∩ b⊥ ) ∪ a⊥ )
98		ancom 74	. . . . . . . . . 10 (b ∩ (b⊥ ∪ a)) = ((b⊥ ∪ a) ∩ b)
99	97, 98	2or 72	. . . . . . . . 9 ((a⊥ ∪ (a ∩ b⊥ )) ∪ (b ∩ (b⊥ ∪ a))) = (((a ∩ b⊥ ) ∪ a⊥ ) ∪ ((b⊥ ∪ a) ∩ b))
100		ax-a3 32	. . . . . . . . . 10 (((a ∩ b⊥ ) ∪ a⊥ ) ∪ ((b⊥ ∪ a) ∩ b)) = ((a ∩ b⊥ ) ∪ (a⊥ ∪ ((b⊥ ∪ a) ∩ b)))
101	25	comcom2 183	. . . . . . . . . . . . . 14 (b⊥ ∪ a) C a⊥
102	101, 28	fh4 472	. . . . . . . . . . . . 13 (a⊥ ∪ ((b⊥ ∪ a) ∩ b)) = ((a⊥ ∪ (b⊥ ∪ a)) ∩ (a⊥ ∪ b))
103		ax-a2 31	. . . . . . . . . . . . . . . 16 (a⊥ ∪ (b⊥ ∪ a)) = ((b⊥ ∪ a) ∪ a⊥ )
104		ax-a3 32	. . . . . . . . . . . . . . . . 17 ((b⊥ ∪ a) ∪ a⊥ ) = (b⊥ ∪ (a ∪ a⊥ ))
105		df-t 41	. . . . . . . . . . . . . . . . . . . 20 1 = (a ∪ a⊥ )
106	105	ax-r1 35	. . . . . . . . . . . . . . . . . . 19 (a ∪ a⊥ ) = 1
107	106	lor 70	. . . . . . . . . . . . . . . . . 18 (b⊥ ∪ (a ∪ a⊥ )) = (b⊥ ∪ 1)
108		or1 104	. . . . . . . . . . . . . . . . . 18 (b⊥ ∪ 1) = 1
109	107, 108	ax-r2 36	. . . . . . . . . . . . . . . . 17 (b⊥ ∪ (a ∪ a⊥ )) = 1
110	104, 109	ax-r2 36	. . . . . . . . . . . . . . . 16 ((b⊥ ∪ a) ∪ a⊥ ) = 1
111	103, 110	ax-r2 36	. . . . . . . . . . . . . . 15 (a⊥ ∪ (b⊥ ∪ a)) = 1
112	111	ran 78	. . . . . . . . . . . . . 14 ((a⊥ ∪ (b⊥ ∪ a)) ∩ (a⊥ ∪ b)) = (1 ∩ (a⊥ ∪ b))
113		an1r 107	. . . . . . . . . . . . . 14 (1 ∩ (a⊥ ∪ b)) = (a⊥ ∪ b)
114	112, 113	ax-r2 36	. . . . . . . . . . . . 13 ((a⊥ ∪ (b⊥ ∪ a)) ∩ (a⊥ ∪ b)) = (a⊥ ∪ b)
115	102, 114	ax-r2 36	. . . . . . . . . . . 12 (a⊥ ∪ ((b⊥ ∪ a) ∩ b)) = (a⊥ ∪ b)
116	115	lor 70	. . . . . . . . . . 11 ((a ∩ b⊥ ) ∪ (a⊥ ∪ ((b⊥ ∪ a) ∩ b))) = ((a ∩ b⊥ ) ∪ (a⊥ ∪ b))
117		ax-a2 31	. . . . . . . . . . . 12 ((a ∩ b⊥ ) ∪ (a⊥ ∪ b)) = ((a⊥ ∪ b) ∪ (a ∩ b⊥ ))
118		anor1 88	. . . . . . . . . . . . . 14 (a ∩ b⊥ ) = (a⊥ ∪ b)⊥
119	118	lor 70	. . . . . . . . . . . . 13 ((a⊥ ∪ b) ∪ (a ∩ b⊥ )) = ((a⊥ ∪ b) ∪ (a⊥ ∪ b)⊥ )
120		df-t 41	. . . . . . . . . . . . . 14 1 = ((a⊥ ∪ b) ∪ (a⊥ ∪ b)⊥ )
121	120	ax-r1 35	. . . . . . . . . . . . 13 ((a⊥ ∪ b) ∪ (a⊥ ∪ b)⊥ ) = 1
122	119, 121	ax-r2 36	. . . . . . . . . . . 12 ((a⊥ ∪ b) ∪ (a ∩ b⊥ )) = 1
123	117, 122	ax-r2 36	. . . . . . . . . . 11 ((a ∩ b⊥ ) ∪ (a⊥ ∪ b)) = 1
124	116, 123	ax-r2 36	. . . . . . . . . 10 ((a ∩ b⊥ ) ∪ (a⊥ ∪ ((b⊥ ∪ a) ∩ b))) = 1
125	100, 124	ax-r2 36	. . . . . . . . 9 (((a ∩ b⊥ ) ∪ a⊥ ) ∪ ((b⊥ ∪ a) ∩ b)) = 1
126	99, 125	ax-r2 36	. . . . . . . 8 ((a⊥ ∪ (a ∩ b⊥ )) ∪ (b ∩ (b⊥ ∪ a))) = 1
127	126	lor 70	. . . . . . 7 (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ ((a⊥ ∪ (a ∩ b⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) = (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ 1)
128		or1 104	. . . . . . 7 (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ 1) = 1
129	127, 128	ax-r2 36	. . . . . 6 (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ ((a⊥ ∪ (a ∩ b⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) = 1
130	96, 129	ax-r2 36	. . . . 5 ((a⊥ ∪ (a ∩ b⊥ )) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) = 1
131	95, 130	2an 79	. . . 4 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) ∩ ((a⊥ ∪ (a ∩ b⊥ )) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a))))) = ((a ∪ b⊥ ) ∩ 1)
132	131, 93	ax-r2 36	. . 3 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) ∩ ((a⊥ ∪ (a ∩ b⊥ )) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a))))) = (a ∪ b⊥ )
133	48, 132	ax-r2 36	. 2 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∪ (((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )) ∪ (b ∩ (b⊥ ∪ a)))) = (a ∪ b⊥ )
134	3, 133	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  1wt 8   →₃ 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:  ud3lem1d  569