Theorem ud5lem1 589

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

Assertion

Ref	Expression
ud5lem1	((a →5 b) →5 (b →5 a)) = (a ∪ b⊥ )

Proof of Theorem ud5lem1

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

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   →₅ wi5 16

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

This theorem is used by:  ud5  599