Theorem ud5lem1a 586

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

Assertion

Ref	Expression
ud5lem1a	((a →5 b) ∩ (b →5 a)) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))

Proof of Theorem ud5lem1a

Step	Hyp	Ref	Expression
1		df-i5 48	. . 3 (a →5 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))
2		df-i5 48	. . 3 (b →5 a) = (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ (b⊥ ∩ a⊥ ))
3	1, 2	2an 79	. 2 ((a →5 b) ∩ (b →5 a)) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ (b⊥ ∩ a⊥ )))
4		ax-a2 31	. . . 4 (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ (b⊥ ∩ a⊥ )) = ((b⊥ ∩ a⊥ ) ∪ ((b ∩ a) ∪ (b⊥ ∩ a)))
5	4	lan 77	. . 3 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ (b⊥ ∩ a⊥ ))) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ ((b⊥ ∩ a⊥ ) ∪ ((b ∩ a) ∪ (b⊥ ∩ a))))
6		coman2 186	. . . . . . . . . 10 (a ∩ b) C b
7	6	comcom2 183	. . . . . . . . 9 (a ∩ b) C b⊥
8		coman1 185	. . . . . . . . . 10 (a ∩ b) C a
9	8	comcom2 183	. . . . . . . . 9 (a ∩ b) C a⊥
10	7, 9	com2an 484	. . . . . . . 8 (a ∩ b) C (b⊥ ∩ a⊥ )
11	10	comcom 453	. . . . . . 7 (b⊥ ∩ a⊥ ) C (a ∩ b)
12		coman2 186	. . . . . . . . . 10 (a⊥ ∩ b) C b
13	12	comcom2 183	. . . . . . . . 9 (a⊥ ∩ b) C b⊥
14		coman1 185	. . . . . . . . 9 (a⊥ ∩ b) C a⊥
15	13, 14	com2an 484	. . . . . . . 8 (a⊥ ∩ b) C (b⊥ ∩ a⊥ )
16	15	comcom 453	. . . . . . 7 (b⊥ ∩ a⊥ ) C (a⊥ ∩ b)
17	11, 16	com2or 483	. . . . . 6 (b⊥ ∩ a⊥ ) C ((a ∩ b) ∪ (a⊥ ∩ b))
18		coman2 186	. . . . . . 7 (b⊥ ∩ a⊥ ) C a⊥
19		coman1 185	. . . . . . 7 (b⊥ ∩ a⊥ ) C b⊥
20	18, 19	com2an 484	. . . . . 6 (b⊥ ∩ a⊥ ) C (a⊥ ∩ b⊥ )
21	17, 20	com2or 483	. . . . 5 (b⊥ ∩ a⊥ ) C (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))
22		coman1 185	. . . . . . . . 9 (b ∩ a) C b
23	22	comcom2 183	. . . . . . . 8 (b ∩ a) C b⊥
24		coman2 186	. . . . . . . . 9 (b ∩ a) C a
25	24	comcom2 183	. . . . . . . 8 (b ∩ a) C a⊥
26	23, 25	com2an 484	. . . . . . 7 (b ∩ a) C (b⊥ ∩ a⊥ )
27	26	comcom 453	. . . . . 6 (b⊥ ∩ a⊥ ) C (b ∩ a)
28		coman1 185	. . . . . . . 8 (b⊥ ∩ a) C b⊥
29		coman2 186	. . . . . . . . 9 (b⊥ ∩ a) C a
30	29	comcom2 183	. . . . . . . 8 (b⊥ ∩ a) C a⊥
31	28, 30	com2an 484	. . . . . . 7 (b⊥ ∩ a) C (b⊥ ∩ a⊥ )
32	31	comcom 453	. . . . . 6 (b⊥ ∩ a⊥ ) C (b⊥ ∩ a)
33	27, 32	com2or 483	. . . . 5 (b⊥ ∩ a⊥ ) C ((b ∩ a) ∪ (b⊥ ∩ a))
34	21, 33	fh2 470	. . . 4 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ ((b⊥ ∩ a⊥ ) ∪ ((b ∩ a) ∪ (b⊥ ∩ a)))) = (((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ a⊥ )) ∪ ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ ((b ∩ a) ∪ (b⊥ ∩ a))))
35	18	comcom3 454	. . . . . . . . . . 11 (b⊥ ∩ a⊥ )⊥ C a⊥
36	35	comcom5 458	. . . . . . . . . 10 (b⊥ ∩ a⊥ ) C a
37	19	comcom3 454	. . . . . . . . . . 11 (b⊥ ∩ a⊥ )⊥ C b⊥
38	37	comcom5 458	. . . . . . . . . 10 (b⊥ ∩ a⊥ ) C b
39	36, 38	com2an 484	. . . . . . . . 9 (b⊥ ∩ a⊥ ) C (a ∩ b)
40	18, 38	com2an 484	. . . . . . . . 9 (b⊥ ∩ a⊥ ) C (a⊥ ∩ b)
41	39, 40	com2or 483	. . . . . . . 8 (b⊥ ∩ a⊥ ) C ((a ∩ b) ∪ (a⊥ ∩ b))
42	41, 20	fh1r 473	. . . . . . 7 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ a⊥ )) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∩ (b⊥ ∩ a⊥ )))
43	11, 16	fh1r 473	. . . . . . . . . 10 (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a⊥ )) = (((a ∩ b) ∩ (b⊥ ∩ a⊥ )) ∪ ((a⊥ ∩ b) ∩ (b⊥ ∩ a⊥ )))
44		anass 76	. . . . . . . . . . . . 13 ((a ∩ b) ∩ (b⊥ ∩ a⊥ )) = (a ∩ (b ∩ (b⊥ ∩ a⊥ )))
45		anass 76	. . . . . . . . . . . . . . . 16 ((b ∩ b⊥ ) ∩ a⊥ ) = (b ∩ (b⊥ ∩ a⊥ ))
46	45	ax-r1 35	. . . . . . . . . . . . . . 15 (b ∩ (b⊥ ∩ a⊥ )) = ((b ∩ b⊥ ) ∩ a⊥ )
47	46	lan 77	. . . . . . . . . . . . . 14 (a ∩ (b ∩ (b⊥ ∩ a⊥ ))) = (a ∩ ((b ∩ b⊥ ) ∩ a⊥ ))
48		ancom 74	. . . . . . . . . . . . . . . . 17 ((b ∩ b⊥ ) ∩ a⊥ ) = (a⊥ ∩ (b ∩ b⊥ ))
49		dff 101	. . . . . . . . . . . . . . . . . . . 20 0 = (b ∩ b⊥ )
50	49	ax-r1 35	. . . . . . . . . . . . . . . . . . 19 (b ∩ b⊥ ) = 0
51	50	lan 77	. . . . . . . . . . . . . . . . . 18 (a⊥ ∩ (b ∩ b⊥ )) = (a⊥ ∩ 0)
52		an0 108	. . . . . . . . . . . . . . . . . 18 (a⊥ ∩ 0) = 0
53	51, 52	ax-r2 36	. . . . . . . . . . . . . . . . 17 (a⊥ ∩ (b ∩ b⊥ )) = 0
54	48, 53	ax-r2 36	. . . . . . . . . . . . . . . 16 ((b ∩ b⊥ ) ∩ a⊥ ) = 0
55	54	lan 77	. . . . . . . . . . . . . . 15 (a ∩ ((b ∩ b⊥ ) ∩ a⊥ )) = (a ∩ 0)
56		an0 108	. . . . . . . . . . . . . . 15 (a ∩ 0) = 0
57	55, 56	ax-r2 36	. . . . . . . . . . . . . 14 (a ∩ ((b ∩ b⊥ ) ∩ a⊥ )) = 0
58	47, 57	ax-r2 36	. . . . . . . . . . . . 13 (a ∩ (b ∩ (b⊥ ∩ a⊥ ))) = 0
59	44, 58	ax-r2 36	. . . . . . . . . . . 12 ((a ∩ b) ∩ (b⊥ ∩ a⊥ )) = 0
60		anass 76	. . . . . . . . . . . . 13 ((a⊥ ∩ b) ∩ (b⊥ ∩ a⊥ )) = (a⊥ ∩ (b ∩ (b⊥ ∩ a⊥ )))
61	46	lan 77	. . . . . . . . . . . . . 14 (a⊥ ∩ (b ∩ (b⊥ ∩ a⊥ ))) = (a⊥ ∩ ((b ∩ b⊥ ) ∩ a⊥ ))
62	54	lan 77	. . . . . . . . . . . . . . 15 (a⊥ ∩ ((b ∩ b⊥ ) ∩ a⊥ )) = (a⊥ ∩ 0)
63	62, 52	ax-r2 36	. . . . . . . . . . . . . 14 (a⊥ ∩ ((b ∩ b⊥ ) ∩ a⊥ )) = 0
64	61, 63	ax-r2 36	. . . . . . . . . . . . 13 (a⊥ ∩ (b ∩ (b⊥ ∩ a⊥ ))) = 0
65	60, 64	ax-r2 36	. . . . . . . . . . . 12 ((a⊥ ∩ b) ∩ (b⊥ ∩ a⊥ )) = 0
66	59, 65	2or 72	. . . . . . . . . . 11 (((a ∩ b) ∩ (b⊥ ∩ a⊥ )) ∪ ((a⊥ ∩ b) ∩ (b⊥ ∩ a⊥ ))) = (0 ∪ 0)
67		or0 102	. . . . . . . . . . 11 (0 ∪ 0) = 0
68	66, 67	ax-r2 36	. . . . . . . . . 10 (((a ∩ b) ∩ (b⊥ ∩ a⊥ )) ∪ ((a⊥ ∩ b) ∩ (b⊥ ∩ a⊥ ))) = 0
69	43, 68	ax-r2 36	. . . . . . . . 9 (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a⊥ )) = 0
70		ancom 74	. . . . . . . . . . 11 (b⊥ ∩ a⊥ ) = (a⊥ ∩ b⊥ )
71	70	lan 77	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∩ (b⊥ ∩ a⊥ )) = ((a⊥ ∩ b⊥ ) ∩ (a⊥ ∩ b⊥ ))
72		anidm 111	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∩ (a⊥ ∩ b⊥ )) = (a⊥ ∩ b⊥ )
73	71, 72	ax-r2 36	. . . . . . . . 9 ((a⊥ ∩ b⊥ ) ∩ (b⊥ ∩ a⊥ )) = (a⊥ ∩ b⊥ )
74	69, 73	2or 72	. . . . . . . 8 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∩ (b⊥ ∩ a⊥ ))) = (0 ∪ (a⊥ ∩ b⊥ ))
75		ax-a2 31	. . . . . . . . 9 (0 ∪ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b⊥ ) ∪ 0)
76		or0 102	. . . . . . . . 9 ((a⊥ ∩ b⊥ ) ∪ 0) = (a⊥ ∩ b⊥ )
77	75, 76	ax-r2 36	. . . . . . . 8 (0 ∪ (a⊥ ∩ b⊥ )) = (a⊥ ∩ b⊥ )
78	74, 77	ax-r2 36	. . . . . . 7 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∩ (b⊥ ∩ a⊥ ))) = (a⊥ ∩ b⊥ )
79	42, 78	ax-r2 36	. . . . . 6 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ a⊥ )) = (a⊥ ∩ b⊥ )
80	24, 22	com2an 484	. . . . . . . . . 10 (b ∩ a) C (a ∩ b)
81	25, 22	com2an 484	. . . . . . . . . 10 (b ∩ a) C (a⊥ ∩ b)
82	80, 81	com2or 483	. . . . . . . . 9 (b ∩ a) C ((a ∩ b) ∪ (a⊥ ∩ b))
83	25, 23	com2an 484	. . . . . . . . 9 (b ∩ a) C (a⊥ ∩ b⊥ )
84	82, 83	com2or 483	. . . . . . . 8 (b ∩ a) C (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))
85	23, 24	com2an 484	. . . . . . . 8 (b ∩ a) C (b⊥ ∩ a)
86	84, 85	fh2 470	. . . . . . 7 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ ((b ∩ a) ∪ (b⊥ ∩ a))) = (((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (b ∩ a)) ∪ ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ a)))
87	82, 83	fh1r 473	. . . . . . . . . 10 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (b ∩ a)) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b ∩ a)) ∪ ((a⊥ ∩ b⊥ ) ∩ (b ∩ a)))
88		anass 76	. . . . . . . . . . . . 13 ((a⊥ ∩ b⊥ ) ∩ (b ∩ a)) = (a⊥ ∩ (b⊥ ∩ (b ∩ a)))
89		an12 81	. . . . . . . . . . . . . . . . 17 (b ∩ (b⊥ ∩ a)) = (b⊥ ∩ (b ∩ a))
90	89	ax-r1 35	. . . . . . . . . . . . . . . 16 (b⊥ ∩ (b ∩ a)) = (b ∩ (b⊥ ∩ a))
91		anass 76	. . . . . . . . . . . . . . . . . 18 ((b ∩ b⊥ ) ∩ a) = (b ∩ (b⊥ ∩ a))
92	91	ax-r1 35	. . . . . . . . . . . . . . . . 17 (b ∩ (b⊥ ∩ a)) = ((b ∩ b⊥ ) ∩ a)
93		ancom 74	. . . . . . . . . . . . . . . . . 18 ((b ∩ b⊥ ) ∩ a) = (a ∩ (b ∩ b⊥ ))
94	50	lan 77	. . . . . . . . . . . . . . . . . . 19 (a ∩ (b ∩ b⊥ )) = (a ∩ 0)
95	94, 56	ax-r2 36	. . . . . . . . . . . . . . . . . 18 (a ∩ (b ∩ b⊥ )) = 0
96	93, 95	ax-r2 36	. . . . . . . . . . . . . . . . 17 ((b ∩ b⊥ ) ∩ a) = 0
97	92, 96	ax-r2 36	. . . . . . . . . . . . . . . 16 (b ∩ (b⊥ ∩ a)) = 0
98	90, 97	ax-r2 36	. . . . . . . . . . . . . . 15 (b⊥ ∩ (b ∩ a)) = 0
99	98	lan 77	. . . . . . . . . . . . . 14 (a⊥ ∩ (b⊥ ∩ (b ∩ a))) = (a⊥ ∩ 0)
100	99, 52	ax-r2 36	. . . . . . . . . . . . 13 (a⊥ ∩ (b⊥ ∩ (b ∩ a))) = 0
101	88, 100	ax-r2 36	. . . . . . . . . . . 12 ((a⊥ ∩ b⊥ ) ∩ (b ∩ a)) = 0
102	101	lor 70	. . . . . . . . . . 11 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b ∩ a)) ∪ ((a⊥ ∩ b⊥ ) ∩ (b ∩ a))) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b ∩ a)) ∪ 0)
103		or0 102	. . . . . . . . . . 11 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b ∩ a)) ∪ 0) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b ∩ a))
104	102, 103	ax-r2 36	. . . . . . . . . 10 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b ∩ a)) ∪ ((a⊥ ∩ b⊥ ) ∩ (b ∩ a))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b ∩ a))
105	87, 104	ax-r2 36	. . . . . . . . 9 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (b ∩ a)) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b ∩ a))
106	28	comcom3 454	. . . . . . . . . . . . . 14 (b⊥ ∩ a)⊥ C b⊥
107	106	comcom5 458	. . . . . . . . . . . . 13 (b⊥ ∩ a) C b
108	29, 107	com2an 484	. . . . . . . . . . . 12 (b⊥ ∩ a) C (a ∩ b)
109	30, 107	com2an 484	. . . . . . . . . . . 12 (b⊥ ∩ a) C (a⊥ ∩ b)
110	108, 109	com2or 483	. . . . . . . . . . 11 (b⊥ ∩ a) C ((a ∩ b) ∪ (a⊥ ∩ b))
111	30, 28	com2an 484	. . . . . . . . . . 11 (b⊥ ∩ a) C (a⊥ ∩ b⊥ )
112	110, 111	fh1r 473	. . . . . . . . . 10 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ a)) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a)) ∪ ((a⊥ ∩ b⊥ ) ∩ (b⊥ ∩ a)))
113		ancom 74	. . . . . . . . . . . . 13 ((a⊥ ∩ b⊥ ) ∩ (b⊥ ∩ a)) = ((b⊥ ∩ a) ∩ (a⊥ ∩ b⊥ ))
114		anass 76	. . . . . . . . . . . . . 14 ((b⊥ ∩ a) ∩ (a⊥ ∩ b⊥ )) = (b⊥ ∩ (a ∩ (a⊥ ∩ b⊥ )))
115		anass 76	. . . . . . . . . . . . . . . . . 18 ((a ∩ a⊥ ) ∩ b⊥ ) = (a ∩ (a⊥ ∩ b⊥ ))
116	115	ax-r1 35	. . . . . . . . . . . . . . . . 17 (a ∩ (a⊥ ∩ b⊥ )) = ((a ∩ a⊥ ) ∩ b⊥ )
117		ancom 74	. . . . . . . . . . . . . . . . . 18 ((a ∩ a⊥ ) ∩ b⊥ ) = (b⊥ ∩ (a ∩ a⊥ ))
118		dff 101	. . . . . . . . . . . . . . . . . . . . 21 0 = (a ∩ a⊥ )
119	118	ax-r1 35	. . . . . . . . . . . . . . . . . . . 20 (a ∩ a⊥ ) = 0
120	119	lan 77	. . . . . . . . . . . . . . . . . . 19 (b⊥ ∩ (a ∩ a⊥ )) = (b⊥ ∩ 0)
121		an0 108	. . . . . . . . . . . . . . . . . . 19 (b⊥ ∩ 0) = 0
122	120, 121	ax-r2 36	. . . . . . . . . . . . . . . . . 18 (b⊥ ∩ (a ∩ a⊥ )) = 0
123	117, 122	ax-r2 36	. . . . . . . . . . . . . . . . 17 ((a ∩ a⊥ ) ∩ b⊥ ) = 0
124	116, 123	ax-r2 36	. . . . . . . . . . . . . . . 16 (a ∩ (a⊥ ∩ b⊥ )) = 0
125	124	lan 77	. . . . . . . . . . . . . . 15 (b⊥ ∩ (a ∩ (a⊥ ∩ b⊥ ))) = (b⊥ ∩ 0)
126	125, 121	ax-r2 36	. . . . . . . . . . . . . 14 (b⊥ ∩ (a ∩ (a⊥ ∩ b⊥ ))) = 0
127	114, 126	ax-r2 36	. . . . . . . . . . . . 13 ((b⊥ ∩ a) ∩ (a⊥ ∩ b⊥ )) = 0
128	113, 127	ax-r2 36	. . . . . . . . . . . 12 ((a⊥ ∩ b⊥ ) ∩ (b⊥ ∩ a)) = 0
129	128	lor 70	. . . . . . . . . . 11 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a)) ∪ ((a⊥ ∩ b⊥ ) ∩ (b⊥ ∩ a))) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a)) ∪ 0)
130		or0 102	. . . . . . . . . . 11 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a)) ∪ 0) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a))
131	129, 130	ax-r2 36	. . . . . . . . . 10 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a)) ∪ ((a⊥ ∩ b⊥ ) ∩ (b⊥ ∩ a))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a))
132	112, 131	ax-r2 36	. . . . . . . . 9 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ a)) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a))
133	105, 132	2or 72	. . . . . . . 8 (((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (b ∩ a)) ∪ ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ a))) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b ∩ a)) ∪ (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a)))
134	7, 8	com2an 484	. . . . . . . . . . . . 13 (a ∩ b) C (b⊥ ∩ a)
135	134	comcom 453	. . . . . . . . . . . 12 (b⊥ ∩ a) C (a ∩ b)
136	135, 109	fh1r 473	. . . . . . . . . . 11 (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a)) = (((a ∩ b) ∩ (b⊥ ∩ a)) ∪ ((a⊥ ∩ b) ∩ (b⊥ ∩ a)))
137		anass 76	. . . . . . . . . . . . . 14 ((a ∩ b) ∩ (b⊥ ∩ a)) = (a ∩ (b ∩ (b⊥ ∩ a)))
138	97	lan 77	. . . . . . . . . . . . . . 15 (a ∩ (b ∩ (b⊥ ∩ a))) = (a ∩ 0)
139	138, 56	ax-r2 36	. . . . . . . . . . . . . 14 (a ∩ (b ∩ (b⊥ ∩ a))) = 0
140	137, 139	ax-r2 36	. . . . . . . . . . . . 13 ((a ∩ b) ∩ (b⊥ ∩ a)) = 0
141		anass 76	. . . . . . . . . . . . . 14 ((a⊥ ∩ b) ∩ (b⊥ ∩ a)) = (a⊥ ∩ (b ∩ (b⊥ ∩ a)))
142	97	lan 77	. . . . . . . . . . . . . . 15 (a⊥ ∩ (b ∩ (b⊥ ∩ a))) = (a⊥ ∩ 0)
143	142, 52	ax-r2 36	. . . . . . . . . . . . . 14 (a⊥ ∩ (b ∩ (b⊥ ∩ a))) = 0
144	141, 143	ax-r2 36	. . . . . . . . . . . . 13 ((a⊥ ∩ b) ∩ (b⊥ ∩ a)) = 0
145	140, 144	2or 72	. . . . . . . . . . . 12 (((a ∩ b) ∩ (b⊥ ∩ a)) ∪ ((a⊥ ∩ b) ∩ (b⊥ ∩ a))) = (0 ∪ 0)
146	145, 67	ax-r2 36	. . . . . . . . . . 11 (((a ∩ b) ∩ (b⊥ ∩ a)) ∪ ((a⊥ ∩ b) ∩ (b⊥ ∩ a))) = 0
147	136, 146	ax-r2 36	. . . . . . . . . 10 (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a)) = 0
148	147	lor 70	. . . . . . . . 9 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b ∩ a)) ∪ (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a))) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b ∩ a)) ∪ 0)
149	80, 81	fh1r 473	. . . . . . . . . . 11 (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b ∩ a)) = (((a ∩ b) ∩ (b ∩ a)) ∪ ((a⊥ ∩ b) ∩ (b ∩ a)))
150		ancom 74	. . . . . . . . . . . . . . 15 (b ∩ a) = (a ∩ b)
151	150	lan 77	. . . . . . . . . . . . . 14 ((a ∩ b) ∩ (b ∩ a)) = ((a ∩ b) ∩ (a ∩ b))
152		anidm 111	. . . . . . . . . . . . . 14 ((a ∩ b) ∩ (a ∩ b)) = (a ∩ b)
153	151, 152	ax-r2 36	. . . . . . . . . . . . 13 ((a ∩ b) ∩ (b ∩ a)) = (a ∩ b)
154		ancom 74	. . . . . . . . . . . . . 14 ((a⊥ ∩ b) ∩ (b ∩ a)) = ((b ∩ a) ∩ (a⊥ ∩ b))
155		anass 76	. . . . . . . . . . . . . . 15 ((b ∩ a) ∩ (a⊥ ∩ b)) = (b ∩ (a ∩ (a⊥ ∩ b)))
156		anass 76	. . . . . . . . . . . . . . . . . . . 20 ((a ∩ a⊥ ) ∩ b) = (a ∩ (a⊥ ∩ b))
157	156	ax-r1 35	. . . . . . . . . . . . . . . . . . 19 (a ∩ (a⊥ ∩ b)) = ((a ∩ a⊥ ) ∩ b)
158	119	ran 78	. . . . . . . . . . . . . . . . . . . 20 ((a ∩ a⊥ ) ∩ b) = (0 ∩ b)
159		ancom 74	. . . . . . . . . . . . . . . . . . . 20 (0 ∩ b) = (b ∩ 0)
160	158, 159	ax-r2 36	. . . . . . . . . . . . . . . . . . 19 ((a ∩ a⊥ ) ∩ b) = (b ∩ 0)
161	157, 160	ax-r2 36	. . . . . . . . . . . . . . . . . 18 (a ∩ (a⊥ ∩ b)) = (b ∩ 0)
162		an0 108	. . . . . . . . . . . . . . . . . 18 (b ∩ 0) = 0
163	161, 162	ax-r2 36	. . . . . . . . . . . . . . . . 17 (a ∩ (a⊥ ∩ b)) = 0
164	163	lan 77	. . . . . . . . . . . . . . . 16 (b ∩ (a ∩ (a⊥ ∩ b))) = (b ∩ 0)
165	164, 162	ax-r2 36	. . . . . . . . . . . . . . 15 (b ∩ (a ∩ (a⊥ ∩ b))) = 0
166	155, 165	ax-r2 36	. . . . . . . . . . . . . 14 ((b ∩ a) ∩ (a⊥ ∩ b)) = 0
167	154, 166	ax-r2 36	. . . . . . . . . . . . 13 ((a⊥ ∩ b) ∩ (b ∩ a)) = 0
168	153, 167	2or 72	. . . . . . . . . . . 12 (((a ∩ b) ∩ (b ∩ a)) ∪ ((a⊥ ∩ b) ∩ (b ∩ a))) = ((a ∩ b) ∪ 0)
169		or0 102	. . . . . . . . . . . 12 ((a ∩ b) ∪ 0) = (a ∩ b)
170	168, 169	ax-r2 36	. . . . . . . . . . 11 (((a ∩ b) ∩ (b ∩ a)) ∪ ((a⊥ ∩ b) ∩ (b ∩ a))) = (a ∩ b)
171	149, 170	ax-r2 36	. . . . . . . . . 10 (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b ∩ a)) = (a ∩ b)
172	103, 171	ax-r2 36	. . . . . . . . 9 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b ∩ a)) ∪ 0) = (a ∩ b)
173	148, 172	ax-r2 36	. . . . . . . 8 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b ∩ a)) ∪ (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (b⊥ ∩ a))) = (a ∩ b)
174	133, 173	ax-r2 36	. . . . . . 7 (((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (b ∩ a)) ∪ ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ a))) = (a ∩ b)
175	86, 174	ax-r2 36	. . . . . 6 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ ((b ∩ a) ∪ (b⊥ ∩ a))) = (a ∩ b)
176	79, 175	2or 72	. . . . 5 (((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ a⊥ )) ∪ ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ ((b ∩ a) ∪ (b⊥ ∩ a)))) = ((a⊥ ∩ b⊥ ) ∪ (a ∩ b))
177		ax-a2 31	. . . . 5 ((a⊥ ∩ b⊥ ) ∪ (a ∩ b)) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
178	176, 177	ax-r2 36	. . . 4 (((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ a⊥ )) ∪ ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ ((b ∩ a) ∪ (b⊥ ∩ a)))) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
179	34, 178	ax-r2 36	. . 3 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ ((b⊥ ∩ a⊥ ) ∪ ((b ∩ a) ∪ (b⊥ ∩ a)))) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
180	5, 179	ax-r2 36	. 2 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) ∩ (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ (b⊥ ∩ a⊥ ))) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
181	3, 180	ax-r2 36	1 ((a →5 b) ∩ (b →5 a)) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  0wf 9   →₅ 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:  ud5lem1  589