Theorem ud3lem1b 567

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

Assertion

Ref	Expression
ud3lem1b	((a →3 b)⊥ ∩ (b →3 a)⊥ ) = 0

Proof of Theorem ud3lem1b

Step	Hyp	Ref	Expression
1		ud3lem0c 279	. . 3 (a →3 b)⊥ = (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ )))
2		ud3lem0c 279	. . 3 (b →3 a)⊥ = (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ (b⊥ ∪ (b ∩ a⊥ )))
3	1, 2	2an 79	. 2 ((a →3 b)⊥ ∩ (b →3 a)⊥ ) = ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ (b⊥ ∪ (b ∩ a⊥ ))))
4		an32 83	. . 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⊥ )))
5		an32 83	. . . . . 6 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ (b⊥ ∪ (b ∩ a⊥ )))) = (((a ∪ b⊥ ) ∩ (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ (b⊥ ∪ (b ∩ a⊥ )))) ∩ (a ∪ b))
6		an12 81	. . . . . . . . 9 ((a ∪ b⊥ ) ∩ (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ (b⊥ ∪ (b ∩ a⊥ )))) = (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ ((a ∪ b⊥ ) ∩ (b⊥ ∪ (b ∩ a⊥ ))))
7		comor2 462	. . . . . . . . . . . . 13 (a ∪ b⊥ ) C b⊥
8	7	comcom7 460	. . . . . . . . . . . . . 14 (a ∪ b⊥ ) C b
9		comor1 461	. . . . . . . . . . . . . . 15 (a ∪ b⊥ ) C a
10	9	comcom2 183	. . . . . . . . . . . . . 14 (a ∪ b⊥ ) C a⊥
11	8, 10	com2an 484	. . . . . . . . . . . . 13 (a ∪ b⊥ ) C (b ∩ a⊥ )
12	7, 11	fh1 469	. . . . . . . . . . . 12 ((a ∪ b⊥ ) ∩ (b⊥ ∪ (b ∩ a⊥ ))) = (((a ∪ b⊥ ) ∩ b⊥ ) ∪ ((a ∪ b⊥ ) ∩ (b ∩ a⊥ )))
13		ancom 74	. . . . . . . . . . . . . . . 16 ((a ∪ b⊥ ) ∩ b⊥ ) = (b⊥ ∩ (a ∪ b⊥ ))
14		ax-a2 31	. . . . . . . . . . . . . . . . 17 (a ∪ b⊥ ) = (b⊥ ∪ a)
15	14	lan 77	. . . . . . . . . . . . . . . 16 (b⊥ ∩ (a ∪ b⊥ )) = (b⊥ ∩ (b⊥ ∪ a))
16	13, 15	ax-r2 36	. . . . . . . . . . . . . . 15 ((a ∪ b⊥ ) ∩ b⊥ ) = (b⊥ ∩ (b⊥ ∪ a))
17		anabs 121	. . . . . . . . . . . . . . 15 (b⊥ ∩ (b⊥ ∪ a)) = b⊥
18	16, 17	ax-r2 36	. . . . . . . . . . . . . 14 ((a ∪ b⊥ ) ∩ b⊥ ) = b⊥
19		anor1 88	. . . . . . . . . . . . . . . 16 (b ∩ a⊥ ) = (b⊥ ∪ a)⊥
20	14, 19	2an 79	. . . . . . . . . . . . . . 15 ((a ∪ b⊥ ) ∩ (b ∩ a⊥ )) = ((b⊥ ∪ a) ∩ (b⊥ ∪ a)⊥ )
21		dff 101	. . . . . . . . . . . . . . . 16 0 = ((b⊥ ∪ a) ∩ (b⊥ ∪ a)⊥ )
22	21	ax-r1 35	. . . . . . . . . . . . . . 15 ((b⊥ ∪ a) ∩ (b⊥ ∪ a)⊥ ) = 0
23	20, 22	ax-r2 36	. . . . . . . . . . . . . 14 ((a ∪ b⊥ ) ∩ (b ∩ a⊥ )) = 0
24	18, 23	2or 72	. . . . . . . . . . . . 13 (((a ∪ b⊥ ) ∩ b⊥ ) ∪ ((a ∪ b⊥ ) ∩ (b ∩ a⊥ ))) = (b⊥ ∪ 0)
25		or0 102	. . . . . . . . . . . . 13 (b⊥ ∪ 0) = b⊥
26	24, 25	ax-r2 36	. . . . . . . . . . . 12 (((a ∪ b⊥ ) ∩ b⊥ ) ∪ ((a ∪ b⊥ ) ∩ (b ∩ a⊥ ))) = b⊥
27	12, 26	ax-r2 36	. . . . . . . . . . 11 ((a ∪ b⊥ ) ∩ (b⊥ ∪ (b ∩ a⊥ ))) = b⊥
28	27	lan 77	. . . . . . . . . 10 (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ ((a ∪ b⊥ ) ∩ (b⊥ ∪ (b ∩ a⊥ )))) = (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ b⊥ )
29		ancom 74	. . . . . . . . . . 11 (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ b⊥ ) = (b⊥ ∩ ((b ∪ a⊥ ) ∩ (b ∪ a)))
30		anass 76	. . . . . . . . . . . 12 ((b⊥ ∩ (b ∪ a⊥ )) ∩ (b ∪ a)) = (b⊥ ∩ ((b ∪ a⊥ ) ∩ (b ∪ a)))
31	30	ax-r1 35	. . . . . . . . . . 11 (b⊥ ∩ ((b ∪ a⊥ ) ∩ (b ∪ a))) = ((b⊥ ∩ (b ∪ a⊥ )) ∩ (b ∪ a))
32	29, 31	ax-r2 36	. . . . . . . . . 10 (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ b⊥ ) = ((b⊥ ∩ (b ∪ a⊥ )) ∩ (b ∪ a))
33	28, 32	ax-r2 36	. . . . . . . . 9 (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ ((a ∪ b⊥ ) ∩ (b⊥ ∪ (b ∩ a⊥ )))) = ((b⊥ ∩ (b ∪ a⊥ )) ∩ (b ∪ a))
34	6, 33	ax-r2 36	. . . . . . . 8 ((a ∪ b⊥ ) ∩ (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ (b⊥ ∪ (b ∩ a⊥ )))) = ((b⊥ ∩ (b ∪ a⊥ )) ∩ (b ∪ a))
35	34	ran 78	. . . . . . 7 (((a ∪ b⊥ ) ∩ (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ (b⊥ ∪ (b ∩ a⊥ )))) ∩ (a ∪ b)) = (((b⊥ ∩ (b ∪ a⊥ )) ∩ (b ∪ a)) ∩ (a ∪ b))
36		ax-a2 31	. . . . . . . . 9 (a ∪ b) = (b ∪ a)
37	36	lan 77	. . . . . . . 8 (((b⊥ ∩ (b ∪ a⊥ )) ∩ (b ∪ a)) ∩ (a ∪ b)) = (((b⊥ ∩ (b ∪ a⊥ )) ∩ (b ∪ a)) ∩ (b ∪ a))
38		anass 76	. . . . . . . . 9 (((b⊥ ∩ (b ∪ a⊥ )) ∩ (b ∪ a)) ∩ (b ∪ a)) = ((b⊥ ∩ (b ∪ a⊥ )) ∩ ((b ∪ a) ∩ (b ∪ a)))
39		anidm 111	. . . . . . . . . . 11 ((b ∪ a) ∩ (b ∪ a)) = (b ∪ a)
40	39	lan 77	. . . . . . . . . 10 ((b⊥ ∩ (b ∪ a⊥ )) ∩ ((b ∪ a) ∩ (b ∪ a))) = ((b⊥ ∩ (b ∪ a⊥ )) ∩ (b ∪ a))
41		an32 83	. . . . . . . . . 10 ((b⊥ ∩ (b ∪ a⊥ )) ∩ (b ∪ a)) = ((b⊥ ∩ (b ∪ a)) ∩ (b ∪ a⊥ ))
42	40, 41	ax-r2 36	. . . . . . . . 9 ((b⊥ ∩ (b ∪ a⊥ )) ∩ ((b ∪ a) ∩ (b ∪ a))) = ((b⊥ ∩ (b ∪ a)) ∩ (b ∪ a⊥ ))
43	38, 42	ax-r2 36	. . . . . . . 8 (((b⊥ ∩ (b ∪ a⊥ )) ∩ (b ∪ a)) ∩ (b ∪ a)) = ((b⊥ ∩ (b ∪ a)) ∩ (b ∪ a⊥ ))
44	37, 43	ax-r2 36	. . . . . . 7 (((b⊥ ∩ (b ∪ a⊥ )) ∩ (b ∪ a)) ∩ (a ∪ b)) = ((b⊥ ∩ (b ∪ a)) ∩ (b ∪ a⊥ ))
45	35, 44	ax-r2 36	. . . . . 6 (((a ∪ b⊥ ) ∩ (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ (b⊥ ∪ (b ∩ a⊥ )))) ∩ (a ∪ b)) = ((b⊥ ∩ (b ∪ a)) ∩ (b ∪ a⊥ ))
46	5, 45	ax-r2 36	. . . . 5 (((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ (b⊥ ∪ (b ∩ a⊥ )))) = ((b⊥ ∩ (b ∪ a)) ∩ (b ∪ a⊥ ))
47	46	ran 78	. . . 4 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ (b⊥ ∪ (b ∩ a⊥ )))) ∩ (a⊥ ∪ (a ∩ b⊥ ))) = (((b⊥ ∩ (b ∪ a)) ∩ (b ∪ a⊥ )) ∩ (a⊥ ∪ (a ∩ b⊥ )))
48		anass 76	. . . . 5 (((b⊥ ∩ (b ∪ a)) ∩ (b ∪ a⊥ )) ∩ (a⊥ ∪ (a ∩ b⊥ ))) = ((b⊥ ∩ (b ∪ a)) ∩ ((b ∪ a⊥ ) ∩ (a⊥ ∪ (a ∩ b⊥ ))))
49		ax-a2 31	. . . . . . . . 9 (b ∪ a⊥ ) = (a⊥ ∪ b)
50	49	ran 78	. . . . . . . 8 ((b ∪ a⊥ ) ∩ (a⊥ ∪ (a ∩ b⊥ ))) = ((a⊥ ∪ b) ∩ (a⊥ ∪ (a ∩ b⊥ )))
51		ancom 74	. . . . . . . . 9 ((a⊥ ∪ b) ∩ (a⊥ ∪ (a ∩ b⊥ ))) = ((a⊥ ∪ (a ∩ b⊥ )) ∩ (a⊥ ∪ b))
52		comor1 461	. . . . . . . . . . 11 (a⊥ ∪ b) C a⊥
53	52	comcom7 460	. . . . . . . . . . . 12 (a⊥ ∪ b) C a
54		comor2 462	. . . . . . . . . . . . 13 (a⊥ ∪ b) C b
55	54	comcom2 183	. . . . . . . . . . . 12 (a⊥ ∪ b) C b⊥
56	53, 55	com2an 484	. . . . . . . . . . 11 (a⊥ ∪ b) C (a ∩ b⊥ )
57	52, 56	fh1r 473	. . . . . . . . . 10 ((a⊥ ∪ (a ∩ b⊥ )) ∩ (a⊥ ∪ b)) = ((a⊥ ∩ (a⊥ ∪ b)) ∪ ((a ∩ b⊥ ) ∩ (a⊥ ∪ b)))
58		anabs 121	. . . . . . . . . . . 12 (a⊥ ∩ (a⊥ ∪ b)) = a⊥
59		ancom 74	. . . . . . . . . . . . 13 ((a ∩ b⊥ ) ∩ (a⊥ ∪ b)) = ((a⊥ ∪ b) ∩ (a ∩ b⊥ ))
60		anor1 88	. . . . . . . . . . . . . . 15 (a ∩ b⊥ ) = (a⊥ ∪ b)⊥
61	60	lan 77	. . . . . . . . . . . . . 14 ((a⊥ ∪ b) ∩ (a ∩ b⊥ )) = ((a⊥ ∪ b) ∩ (a⊥ ∪ b)⊥ )
62		dff 101	. . . . . . . . . . . . . . 15 0 = ((a⊥ ∪ b) ∩ (a⊥ ∪ b)⊥ )
63	62	ax-r1 35	. . . . . . . . . . . . . 14 ((a⊥ ∪ b) ∩ (a⊥ ∪ b)⊥ ) = 0
64	61, 63	ax-r2 36	. . . . . . . . . . . . 13 ((a⊥ ∪ b) ∩ (a ∩ b⊥ )) = 0
65	59, 64	ax-r2 36	. . . . . . . . . . . 12 ((a ∩ b⊥ ) ∩ (a⊥ ∪ b)) = 0
66	58, 65	2or 72	. . . . . . . . . . 11 ((a⊥ ∩ (a⊥ ∪ b)) ∪ ((a ∩ b⊥ ) ∩ (a⊥ ∪ b))) = (a⊥ ∪ 0)
67		or0 102	. . . . . . . . . . 11 (a⊥ ∪ 0) = a⊥
68	66, 67	ax-r2 36	. . . . . . . . . 10 ((a⊥ ∩ (a⊥ ∪ b)) ∪ ((a ∩ b⊥ ) ∩ (a⊥ ∪ b))) = a⊥
69	57, 68	ax-r2 36	. . . . . . . . 9 ((a⊥ ∪ (a ∩ b⊥ )) ∩ (a⊥ ∪ b)) = a⊥
70	51, 69	ax-r2 36	. . . . . . . 8 ((a⊥ ∪ b) ∩ (a⊥ ∪ (a ∩ b⊥ ))) = a⊥
71	50, 70	ax-r2 36	. . . . . . 7 ((b ∪ a⊥ ) ∩ (a⊥ ∪ (a ∩ b⊥ ))) = a⊥
72	71	lan 77	. . . . . 6 ((b⊥ ∩ (b ∪ a)) ∩ ((b ∪ a⊥ ) ∩ (a⊥ ∪ (a ∩ b⊥ )))) = ((b⊥ ∩ (b ∪ a)) ∩ a⊥ )
73		an32 83	. . . . . . 7 ((b⊥ ∩ (b ∪ a)) ∩ a⊥ ) = ((b⊥ ∩ a⊥ ) ∩ (b ∪ a))
74		oran 87	. . . . . . . . 9 (b ∪ a) = (b⊥ ∩ a⊥ )⊥
75	74	lan 77	. . . . . . . 8 ((b⊥ ∩ a⊥ ) ∩ (b ∪ a)) = ((b⊥ ∩ a⊥ ) ∩ (b⊥ ∩ a⊥ )⊥ )
76		dff 101	. . . . . . . . 9 0 = ((b⊥ ∩ a⊥ ) ∩ (b⊥ ∩ a⊥ )⊥ )
77	76	ax-r1 35	. . . . . . . 8 ((b⊥ ∩ a⊥ ) ∩ (b⊥ ∩ a⊥ )⊥ ) = 0
78	75, 77	ax-r2 36	. . . . . . 7 ((b⊥ ∩ a⊥ ) ∩ (b ∪ a)) = 0
79	73, 78	ax-r2 36	. . . . . 6 ((b⊥ ∩ (b ∪ a)) ∩ a⊥ ) = 0
80	72, 79	ax-r2 36	. . . . 5 ((b⊥ ∩ (b ∪ a)) ∩ ((b ∪ a⊥ ) ∩ (a⊥ ∪ (a ∩ b⊥ )))) = 0
81	48, 80	ax-r2 36	. . . 4 (((b⊥ ∩ (b ∪ a)) ∩ (b ∪ a⊥ )) ∩ (a⊥ ∪ (a ∩ b⊥ ))) = 0
82	47, 81	ax-r2 36	. . 3 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ (b⊥ ∪ (b ∩ a⊥ )))) ∩ (a⊥ ∪ (a ∩ b⊥ ))) = 0
83	4, 82	ax-r2 36	. 2 ((((a ∪ b⊥ ) ∩ (a ∪ b)) ∩ (a⊥ ∪ (a ∩ b⊥ ))) ∩ (((b ∪ a⊥ ) ∩ (b ∪ a)) ∩ (b⊥ ∪ (b ∩ a⊥ )))) = 0
84	3, 83	ax-r2 36	1 ((a →3 b)⊥ ∩ (b →3 a)⊥ ) = 0

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