Theorem ud5lem1b 587

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

Assertion

Ref	Expression
ud5lem1b	((a →5 b)⊥ ∩ (b →5 a)) = (a ∩ b⊥ )

Proof of Theorem ud5lem1b

Step	Hyp	Ref	Expression
1		ud5lem0c 281	. . 3 (a →5 b)⊥ = (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b))
2		df-i5 48	. . . 4 (b →5 a) = (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ (b⊥ ∩ a⊥ ))
3		ax-a2 31	. . . 4 (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ (b⊥ ∩ a⊥ )) = ((b⊥ ∩ a⊥ ) ∪ ((b ∩ a) ∪ (b⊥ ∩ a)))
4	2, 3	ax-r2 36	. . 3 (b →5 a) = ((b⊥ ∩ a⊥ ) ∪ ((b ∩ a) ∪ (b⊥ ∩ a)))
5	1, 4	2an 79	. 2 ((a →5 b)⊥ ∩ (b →5 a)) = ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ ((b⊥ ∩ a⊥ ) ∪ ((b ∩ a) ∪ (b⊥ ∩ a))))
6		coman2 186	. . . . . . 7 (b⊥ ∩ a⊥ ) C a⊥
7		coman1 185	. . . . . . 7 (b⊥ ∩ a⊥ ) C b⊥
8	6, 7	com2or 483	. . . . . 6 (b⊥ ∩ a⊥ ) C (a⊥ ∪ b⊥ )
9	6	comcom7 460	. . . . . . 7 (b⊥ ∩ a⊥ ) C a
10	9, 7	com2or 483	. . . . . 6 (b⊥ ∩ a⊥ ) C (a ∪ b⊥ )
11	8, 10	com2an 484	. . . . 5 (b⊥ ∩ a⊥ ) C ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ ))
12	7	comcom7 460	. . . . . 6 (b⊥ ∩ a⊥ ) C b
13	9, 12	com2or 483	. . . . 5 (b⊥ ∩ a⊥ ) C (a ∪ b)
14	11, 13	com2an 484	. . . 4 (b⊥ ∩ a⊥ ) C (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b))
15	12, 9	com2an 484	. . . . 5 (b⊥ ∩ a⊥ ) C (b ∩ a)
16	7, 9	com2an 484	. . . . 5 (b⊥ ∩ a⊥ ) C (b⊥ ∩ a)
17	15, 16	com2or 483	. . . 4 (b⊥ ∩ a⊥ ) C ((b ∩ a) ∪ (b⊥ ∩ a))
18	14, 17	fh2 470	. . 3 ((((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))))
19		anass 76	. . . . . 6 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ (b⊥ ∩ a⊥ )) = (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∪ b) ∩ (b⊥ ∩ a⊥ )))
20		ax-a2 31	. . . . . . . . . 10 (a ∪ b) = (b ∪ a)
21		oran 87	. . . . . . . . . . . 12 (b ∪ a) = (b⊥ ∩ a⊥ )⊥
22	21	ax-r1 35	. . . . . . . . . . 11 (b⊥ ∩ a⊥ )⊥ = (b ∪ a)
23	22	con3 68	. . . . . . . . . 10 (b⊥ ∩ a⊥ ) = (b ∪ a)⊥
24	20, 23	2an 79	. . . . . . . . 9 ((a ∪ b) ∩ (b⊥ ∩ a⊥ )) = ((b ∪ a) ∩ (b ∪ a)⊥ )
25		dff 101	. . . . . . . . . 10 0 = ((b ∪ a) ∩ (b ∪ a)⊥ )
26	25	ax-r1 35	. . . . . . . . 9 ((b ∪ a) ∩ (b ∪ a)⊥ ) = 0
27	24, 26	ax-r2 36	. . . . . . . 8 ((a ∪ b) ∩ (b⊥ ∩ a⊥ )) = 0
28	27	lan 77	. . . . . . 7 (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∪ b) ∩ (b⊥ ∩ a⊥ ))) = (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ 0)
29		an0 108	. . . . . . 7 (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ 0) = 0
30	28, 29	ax-r2 36	. . . . . 6 (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ ((a ∪ b) ∩ (b⊥ ∩ a⊥ ))) = 0
31	19, 30	ax-r2 36	. . . . 5 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ (b⊥ ∩ a⊥ )) = 0
32		coman2 186	. . . . . . . . . . 11 (b ∩ a) C a
33	32	comcom2 183	. . . . . . . . . 10 (b ∩ a) C a⊥
34		coman1 185	. . . . . . . . . . 11 (b ∩ a) C b
35	34	comcom2 183	. . . . . . . . . 10 (b ∩ a) C b⊥
36	33, 35	com2or 483	. . . . . . . . 9 (b ∩ a) C (a⊥ ∪ b⊥ )
37	32, 35	com2or 483	. . . . . . . . 9 (b ∩ a) C (a ∪ b⊥ )
38	36, 37	com2an 484	. . . . . . . 8 (b ∩ a) C ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ ))
39	32, 34	com2or 483	. . . . . . . 8 (b ∩ a) C (a ∪ b)
40	38, 39	com2an 484	. . . . . . 7 (b ∩ a) C (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b))
41	35, 32	com2an 484	. . . . . . 7 (b ∩ a) C (b⊥ ∩ a)
42	40, 41	fh2 470	. . . . . 6 ((((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)))
43		an32 83	. . . . . . . . 9 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ (b ∩ a)) = ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (b ∩ a)) ∩ (a ∪ b))
44		an32 83	. . . . . . . . . . . 12 (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (b ∩ a)) = (((a⊥ ∪ b⊥ ) ∩ (b ∩ a)) ∩ (a ∪ b⊥ ))
45		ax-a2 31	. . . . . . . . . . . . . . . 16 (a⊥ ∪ b⊥ ) = (b⊥ ∪ a⊥ )
46		df-a 40	. . . . . . . . . . . . . . . 16 (b ∩ a) = (b⊥ ∪ a⊥ )⊥
47	45, 46	2an 79	. . . . . . . . . . . . . . 15 ((a⊥ ∪ b⊥ ) ∩ (b ∩ a)) = ((b⊥ ∪ a⊥ ) ∩ (b⊥ ∪ a⊥ )⊥ )
48		dff 101	. . . . . . . . . . . . . . . 16 0 = ((b⊥ ∪ a⊥ ) ∩ (b⊥ ∪ a⊥ )⊥ )
49	48	ax-r1 35	. . . . . . . . . . . . . . 15 ((b⊥ ∪ a⊥ ) ∩ (b⊥ ∪ a⊥ )⊥ ) = 0
50	47, 49	ax-r2 36	. . . . . . . . . . . . . 14 ((a⊥ ∪ b⊥ ) ∩ (b ∩ a)) = 0
51	50	ran 78	. . . . . . . . . . . . 13 (((a⊥ ∪ b⊥ ) ∩ (b ∩ a)) ∩ (a ∪ b⊥ )) = (0 ∩ (a ∪ b⊥ ))
52		an0r 109	. . . . . . . . . . . . 13 (0 ∩ (a ∪ b⊥ )) = 0
53	51, 52	ax-r2 36	. . . . . . . . . . . 12 (((a⊥ ∪ b⊥ ) ∩ (b ∩ a)) ∩ (a ∪ b⊥ )) = 0
54	44, 53	ax-r2 36	. . . . . . . . . . 11 (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (b ∩ a)) = 0
55	54	ran 78	. . . . . . . . . 10 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (b ∩ a)) ∩ (a ∪ b)) = (0 ∩ (a ∪ b))
56		an0r 109	. . . . . . . . . 10 (0 ∩ (a ∪ b)) = 0
57	55, 56	ax-r2 36	. . . . . . . . 9 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (b ∩ a)) ∩ (a ∪ b)) = 0
58	43, 57	ax-r2 36	. . . . . . . 8 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ (b ∩ a)) = 0
59		lea 160	. . . . . . . . . . . 12 (b⊥ ∩ a) ≤ b⊥
60		leor 159	. . . . . . . . . . . . 13 b⊥ ≤ (a⊥ ∪ b⊥ )
61		leor 159	. . . . . . . . . . . . 13 b⊥ ≤ (a ∪ b⊥ )
62	60, 61	ler2an 173	. . . . . . . . . . . 12 b⊥ ≤ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ ))
63	59, 62	letr 137	. . . . . . . . . . 11 (b⊥ ∩ a) ≤ ((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ ))
64		lear 161	. . . . . . . . . . . 12 (b⊥ ∩ a) ≤ a
65		leo 158	. . . . . . . . . . . 12 a ≤ (a ∪ b)
66	64, 65	letr 137	. . . . . . . . . . 11 (b⊥ ∩ a) ≤ (a ∪ b)
67	63, 66	ler2an 173	. . . . . . . . . 10 (b⊥ ∩ a) ≤ (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b))
68	67	df2le2 136	. . . . . . . . 9 ((b⊥ ∩ a) ∩ (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b))) = (b⊥ ∩ a)
69		ancom 74	. . . . . . . . 9 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ (b⊥ ∩ a)) = ((b⊥ ∩ a) ∩ (((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)))
70		ancom 74	. . . . . . . . 9 (a ∩ b⊥ ) = (b⊥ ∩ a)
71	68, 69, 70	3tr1 63	. . . . . . . 8 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ (b⊥ ∩ a)) = (a ∩ b⊥ )
72	58, 71	2or 72	. . . . . . 7 (((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ (b ∩ a)) ∪ ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ (b⊥ ∩ a))) = (0 ∪ (a ∩ b⊥ ))
73		or0r 103	. . . . . . 7 (0 ∪ (a ∩ b⊥ )) = (a ∩ b⊥ )
74	72, 73	ax-r2 36	. . . . . 6 (((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ (b ∩ a)) ∪ ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ (b⊥ ∩ a))) = (a ∩ b⊥ )
75	42, 74	ax-r2 36	. . . . 5 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ ((b ∩ a) ∪ (b⊥ ∩ a))) = (a ∩ b⊥ )
76	31, 75	2or 72	. . . 4 (((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ (b⊥ ∩ a⊥ )) ∪ ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ ((b ∩ a) ∪ (b⊥ ∩ a)))) = (0 ∪ (a ∩ b⊥ ))
77	76, 73	ax-r2 36	. . 3 (((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ (b⊥ ∩ a⊥ )) ∪ ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ ((b ∩ a) ∪ (b⊥ ∩ a)))) = (a ∩ b⊥ )
78	18, 77	ax-r2 36	. 2 ((((a⊥ ∪ b⊥ ) ∩ (a ∪ b⊥ )) ∩ (a ∪ b)) ∩ ((b⊥ ∩ a⊥ ) ∪ ((b ∩ a) ∪ (b⊥ ∩ a)))) = (a ∩ b⊥ )
79	5, 78	ax-r2 36	1 ((a →5 b)⊥ ∩ (b →5 a)) = (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