Theorem ud4lem1c 579

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

Assertion

Ref	Expression
ud4lem1c	((a →4 b)⊥ ∪ (b →4 a)) = (a ∪ b⊥ )

Proof of Theorem ud4lem1c

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

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   →₄ wi4 15

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

This theorem is used by:  ud4lem1d  580