Theorem ud4lem1 581

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

Assertion

Ref	Expression
ud4lem1	((a →4 b) →4 (b →4 a)) = (a ∪ (a⊥ ∩ b⊥ ))

Proof of Theorem ud4lem1

Step	Hyp	Ref	Expression
1		df-i4 47	. 2 ((a →4 b) →4 (b →4 a)) = ((((a →4 b) ∩ (b →4 a)) ∪ ((a →4 b)⊥ ∩ (b →4 a))) ∪ (((a →4 b)⊥ ∪ (b →4 a)) ∩ (b →4 a)⊥ ))
2		ud4lem1a 577	. . . . 5 ((a →4 b) ∩ (b →4 a)) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
3		ud4lem1b 578	. . . . 5 ((a →4 b)⊥ ∩ (b →4 a)) = (a ∩ b⊥ )
4	2, 3	2or 72	. . . 4 (((a →4 b) ∩ (b →4 a)) ∪ ((a →4 b)⊥ ∩ (b →4 a))) = (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ ))
5		ud4lem1d 580	. . . 4 (((a →4 b)⊥ ∪ (b →4 a)) ∩ (b →4 a)⊥ ) = (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ a)
6	4, 5	2or 72	. . 3 ((((a →4 b) ∩ (b →4 a)) ∪ ((a →4 b)⊥ ∩ (b →4 a))) ∪ (((a →4 b)⊥ ∪ (b →4 a)) ∩ (b →4 a)⊥ )) = ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ a))
7		ancom 74	. . . . . 6 (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ a) = (a ∩ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)))
8	7	lor 70	. . . . 5 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ a)) = ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ (a ∩ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b))))
9		coman1 185	. . . . . . . . . . . 12 (a ∩ b) C a
10	9	comcom 453	. . . . . . . . . . 11 a C (a ∩ b)
11	10	comcom3 454	. . . . . . . . . 10 a⊥ C (a ∩ b)
12		coman1 185	. . . . . . . . . . 11 (a⊥ ∩ b⊥ ) C a⊥
13	12	comcom 453	. . . . . . . . . 10 a⊥ C (a⊥ ∩ b⊥ )
14	11, 13	com2or 483	. . . . . . . . 9 a⊥ C ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
15		coman1 185	. . . . . . . . . . 11 (a ∩ b⊥ ) C a
16	15	comcom 453	. . . . . . . . . 10 a C (a ∩ b⊥ )
17	16	comcom3 454	. . . . . . . . 9 a⊥ C (a ∩ b⊥ )
18	14, 17	com2or 483	. . . . . . . 8 a⊥ C (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ ))
19	18	comcom2 183	. . . . . . 7 a⊥ C (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ ))⊥
20	19	comcom5 458	. . . . . 6 a C (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ ))
21		comorr 184	. . . . . . . . 9 a⊥ C (a⊥ ∪ b⊥ )
22		comorr 184	. . . . . . . . 9 a⊥ C (a⊥ ∪ b)
23	21, 22	com2an 484	. . . . . . . 8 a⊥ C ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b))
24	23	comcom2 183	. . . . . . 7 a⊥ C ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b))⊥
25	24	comcom5 458	. . . . . 6 a C ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b))
26	20, 25	fh4 472	. . . . 5 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ (a ∩ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)))) = (((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ a) ∩ ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b))))
27	8, 26	ax-r2 36	. . . 4 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ a)) = (((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ a) ∩ ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b))))
28		ax-a3 32	. . . . . . . 8 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ a) = (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ ((a ∩ b⊥ ) ∪ a))
29		or4 84	. . . . . . . . 9 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ ((a ∩ b⊥ ) ∪ a)) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ a))
30		lea 160	. . . . . . . . . . . 12 (a ∩ b) ≤ a
31		lea 160	. . . . . . . . . . . 12 (a ∩ b⊥ ) ≤ a
32	30, 31	lel2or 170	. . . . . . . . . . 11 ((a ∩ b) ∪ (a ∩ b⊥ )) ≤ a
33		leor 159	. . . . . . . . . . 11 a ≤ ((a⊥ ∩ b⊥ ) ∪ a)
34	32, 33	letr 137	. . . . . . . . . 10 ((a ∩ b) ∪ (a ∩ b⊥ )) ≤ ((a⊥ ∩ b⊥ ) ∪ a)
35	34	df-le2 131	. . . . . . . . 9 (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b⊥ ) ∪ a)) = ((a⊥ ∩ b⊥ ) ∪ a)
36	29, 35	ax-r2 36	. . . . . . . 8 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ ((a ∩ b⊥ ) ∪ a)) = ((a⊥ ∩ b⊥ ) ∪ a)
37	28, 36	ax-r2 36	. . . . . . 7 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ a) = ((a⊥ ∩ b⊥ ) ∪ a)
38		ax-a2 31	. . . . . . 7 ((a⊥ ∩ b⊥ ) ∪ a) = (a ∪ (a⊥ ∩ b⊥ ))
39	37, 38	ax-r2 36	. . . . . 6 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ a) = (a ∪ (a⊥ ∩ b⊥ ))
40	9	comcom2 183	. . . . . . . . . . . . 13 (a ∩ b) C a⊥
41		coman2 186	. . . . . . . . . . . . . 14 (a ∩ b) C b
42	41	comcom2 183	. . . . . . . . . . . . 13 (a ∩ b) C b⊥
43	40, 42	com2or 483	. . . . . . . . . . . 12 (a ∩ b) C (a⊥ ∪ b⊥ )
44	43	comcom 453	. . . . . . . . . . 11 (a⊥ ∪ b⊥ ) C (a ∩ b)
45		comor1 461	. . . . . . . . . . . 12 (a⊥ ∪ b⊥ ) C a⊥
46		comor2 462	. . . . . . . . . . . 12 (a⊥ ∪ b⊥ ) C b⊥
47	45, 46	com2an 484	. . . . . . . . . . 11 (a⊥ ∪ b⊥ ) C (a⊥ ∩ b⊥ )
48	44, 47	com2or 483	. . . . . . . . . 10 (a⊥ ∪ b⊥ ) C ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
49	45	comcom3 454	. . . . . . . . . . . 12 (a⊥ ∪ b⊥ )⊥ C a⊥
50	49	comcom5 458	. . . . . . . . . . 11 (a⊥ ∪ b⊥ ) C a
51	50, 46	com2an 484	. . . . . . . . . 10 (a⊥ ∪ b⊥ ) C (a ∩ b⊥ )
52	48, 51	com2or 483	. . . . . . . . 9 (a⊥ ∪ b⊥ ) C (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ ))
53	46	comcom3 454	. . . . . . . . . . 11 (a⊥ ∪ b⊥ )⊥ C b⊥
54	53	comcom5 458	. . . . . . . . . 10 (a⊥ ∪ b⊥ ) C b
55	45, 54	com2or 483	. . . . . . . . 9 (a⊥ ∪ b⊥ ) C (a⊥ ∪ b)
56	52, 55	fh4 472	. . . . . . . 8 ((((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)))
57		or32 82	. . . . . . . . . 10 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ (a⊥ ∪ b⊥ )) = ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∪ b⊥ )) ∪ (a ∩ b⊥ ))
58		or32 82	. . . . . . . . . . . . 13 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∪ b⊥ )) = (((a ∩ b) ∪ (a⊥ ∪ b⊥ )) ∪ (a⊥ ∩ b⊥ ))
59		df-a 40	. . . . . . . . . . . . . . . . . . 19 (a ∩ b) = (a⊥ ∪ b⊥ )⊥
60	59	con2 67	. . . . . . . . . . . . . . . . . 18 (a ∩ b)⊥ = (a⊥ ∪ b⊥ )
61	60	ax-r1 35	. . . . . . . . . . . . . . . . 17 (a⊥ ∪ b⊥ ) = (a ∩ b)⊥
62	61	lor 70	. . . . . . . . . . . . . . . 16 ((a ∩ b) ∪ (a⊥ ∪ b⊥ )) = ((a ∩ b) ∪ (a ∩ b)⊥ )
63		df-t 41	. . . . . . . . . . . . . . . . 17 1 = ((a ∩ b) ∪ (a ∩ b)⊥ )
64	63	ax-r1 35	. . . . . . . . . . . . . . . 16 ((a ∩ b) ∪ (a ∩ b)⊥ ) = 1
65	62, 64	ax-r2 36	. . . . . . . . . . . . . . 15 ((a ∩ b) ∪ (a⊥ ∪ b⊥ )) = 1
66	65	ax-r5 38	. . . . . . . . . . . . . 14 (((a ∩ b) ∪ (a⊥ ∪ b⊥ )) ∪ (a⊥ ∩ b⊥ )) = (1 ∪ (a⊥ ∩ b⊥ ))
67		ax-a2 31	. . . . . . . . . . . . . . 15 (1 ∪ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b⊥ ) ∪ 1)
68		or1 104	. . . . . . . . . . . . . . 15 ((a⊥ ∩ b⊥ ) ∪ 1) = 1
69	67, 68	ax-r2 36	. . . . . . . . . . . . . 14 (1 ∪ (a⊥ ∩ b⊥ )) = 1
70	66, 69	ax-r2 36	. . . . . . . . . . . . 13 (((a ∩ b) ∪ (a⊥ ∪ b⊥ )) ∪ (a⊥ ∩ b⊥ )) = 1
71	58, 70	ax-r2 36	. . . . . . . . . . . 12 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∪ b⊥ )) = 1
72	71	ax-r5 38	. . . . . . . . . . 11 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∪ b⊥ )) ∪ (a ∩ b⊥ )) = (1 ∪ (a ∩ b⊥ ))
73		ax-a2 31	. . . . . . . . . . . 12 (1 ∪ (a ∩ b⊥ )) = ((a ∩ b⊥ ) ∪ 1)
74		or1 104	. . . . . . . . . . . 12 ((a ∩ b⊥ ) ∪ 1) = 1
75	73, 74	ax-r2 36	. . . . . . . . . . 11 (1 ∪ (a ∩ b⊥ )) = 1
76	72, 75	ax-r2 36	. . . . . . . . . 10 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∪ b⊥ )) ∪ (a ∩ b⊥ )) = 1
77	57, 76	ax-r2 36	. . . . . . . . 9 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ (a⊥ ∪ b⊥ )) = 1
78		ax-a3 32	. . . . . . . . . 10 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ (a⊥ ∪ b)) = (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∪ b)))
79		anor1 88	. . . . . . . . . . . . . 14 (a ∩ b⊥ ) = (a⊥ ∪ b)⊥
80	79	lor 70	. . . . . . . . . . . . 13 ((a⊥ ∪ b) ∪ (a ∩ b⊥ )) = ((a⊥ ∪ b) ∪ (a⊥ ∪ b)⊥ )
81		ax-a2 31	. . . . . . . . . . . . 13 ((a ∩ b⊥ ) ∪ (a⊥ ∪ b)) = ((a⊥ ∪ b) ∪ (a ∩ b⊥ ))
82		df-t 41	. . . . . . . . . . . . 13 1 = ((a⊥ ∪ b) ∪ (a⊥ ∪ b)⊥ )
83	80, 81, 82	3tr1 63	. . . . . . . . . . . 12 ((a ∩ b⊥ ) ∪ (a⊥ ∪ b)) = 1
84	83	lor 70	. . . . . . . . . . 11 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∪ b))) = (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ 1)
85		or1 104	. . . . . . . . . . 11 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ 1) = 1
86	84, 85	ax-r2 36	. . . . . . . . . 10 (((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∪ b))) = 1
87	78, 86	ax-r2 36	. . . . . . . . 9 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ (a⊥ ∪ b)) = 1
88	77, 87	2an 79	. . . . . . . 8 (((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ (a⊥ ∪ b⊥ )) ∩ ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ (a⊥ ∪ b))) = (1 ∩ 1)
89	56, 88	ax-r2 36	. . . . . . 7 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b))) = (1 ∩ 1)
90		an1 106	. . . . . . 7 (1 ∩ 1) = 1
91	89, 90	ax-r2 36	. . . . . 6 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b))) = 1
92	39, 91	2an 79	. . . . 5 (((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ a) ∩ ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)))) = ((a ∪ (a⊥ ∩ b⊥ )) ∩ 1)
93		an1 106	. . . . 5 ((a ∪ (a⊥ ∩ b⊥ )) ∩ 1) = (a ∪ (a⊥ ∩ b⊥ ))
94	92, 93	ax-r2 36	. . . 4 (((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ a) ∩ ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)))) = (a ∪ (a⊥ ∩ b⊥ ))
95	27, 94	ax-r2 36	. . 3 ((((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ b⊥ )) ∪ (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ a)) = (a ∪ (a⊥ ∩ b⊥ ))
96	6, 95	ax-r2 36	. 2 ((((a →4 b) ∩ (b →4 a)) ∪ ((a →4 b)⊥ ∩ (b →4 a))) ∪ (((a →4 b)⊥ ∪ (b →4 a)) ∩ (b →4 a)⊥ )) = (a ∪ (a⊥ ∩ b⊥ ))
97	1, 96	ax-r2 36	1 ((a →4 b) →4 (b →4 a)) = (a ∪ (a⊥ ∩ b⊥ ))

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   →₄ wi4 15

This theorem was proved from 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 theorem 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 referenced by:  ud4  598