Theorem ud5lem1b 569

Description: Lemma for unified disjunction.

Assertion

Ref	Expression
ud5lem1b	((a ->5 b)_|_ ^ (b ->5 a)) = (a ^ b_|_)

Proof of Theorem ud5lem1b

Step	Hyp	Ref	Expression
1		ud5lem0c 273	. . 3 (a ->5 b)_|_ = (((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b))
2		df-i5 47	. . . 4 (b ->5 a) = (((b ^ a) v (b_|_ ^ a)) v (b_|_ ^ a_|_))
3		ax-a2 30	. . . 4 (((b ^ a) v (b_|_ ^ a)) v (b_|_ ^ a_|_)) = ((b_|_ ^ a_|_) v ((b ^ a) v (b_|_ ^ a)))
4	2, 3	ax-r2 35	. . 3 (b ->5 a) = ((b_|_ ^ a_|_) v ((b ^ a) v (b_|_ ^ a)))
5	1, 4	2an 72	. 2 ((a ->5 b)_|_ ^ (b ->5 a)) = ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ ((b_|_ ^ a_|_) v ((b ^ a) v (b_|_ ^ a))))
6		coman2 178	. . . . . . 7 (b_|_ ^ a_|_) C a_|_
7		coman1 177	. . . . . . 7 (b_|_ ^ a_|_) C b_|_
8	6, 7	com2or 465	. . . . . 6 (b_|_ ^ a_|_) C (a_|_ v b_|_)
9	6	comcom7 442	. . . . . . 7 (b_|_ ^ a_|_) C a
10	9, 7	com2or 465	. . . . . 6 (b_|_ ^ a_|_) C (a v b_|_)
11	8, 10	com2an 466	. . . . 5 (b_|_ ^ a_|_) C ((a_|_ v b_|_) ^ (a v b_|_))
12	7	comcom7 442	. . . . . 6 (b_|_ ^ a_|_) C b
13	9, 12	com2or 465	. . . . 5 (b_|_ ^ a_|_) C (a v b)
14	11, 13	com2an 466	. . . 4 (b_|_ ^ a_|_) C (((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b))
15	12, 9	com2an 466	. . . . 5 (b_|_ ^ a_|_) C (b ^ a)
16	7, 9	com2an 466	. . . . 5 (b_|_ ^ a_|_) C (b_|_ ^ a)
17	15, 16	com2or 465	. . . 4 (b_|_ ^ a_|_) C ((b ^ a) v (b_|_ ^ a))
18	14, 17	fh2 452	. . 3 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ ((b_|_ ^ a_|_) v ((b ^ a) v (b_|_ ^ a)))) = (((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ (b_|_ ^ a_|_)) v ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ ((b ^ a) v (b_|_ ^ a))))
19		anass 69	. . . . . 6 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ (b_|_ ^ a_|_)) = (((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a v b) ^ (b_|_ ^ a_|_)))
20		ax-a2 30	. . . . . . . . . 10 (a v b) = (b v a)
21		oran 79	. . . . . . . . . . . 12 (b v a) = (b_|_ ^ a_|_)_|_
22	21	ax-r1 34	. . . . . . . . . . 11 (b_|_ ^ a_|_)_|_ = (b v a)
23	22	con3 65	. . . . . . . . . 10 (b_|_ ^ a_|_) = (b v a)_|_
24	20, 23	2an 72	. . . . . . . . 9 ((a v b) ^ (b_|_ ^ a_|_)) = ((b v a) ^ (b v a)_|_)
25		dff 93	. . . . . . . . . 10 0 = ((b v a) ^ (b v a)_|_)
26	25	ax-r1 34	. . . . . . . . 9 ((b v a) ^ (b v a)_|_) = 0
27	24, 26	ax-r2 35	. . . . . . . 8 ((a v b) ^ (b_|_ ^ a_|_)) = 0
28	27	lan 70	. . . . . . 7 (((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a v b) ^ (b_|_ ^ a_|_))) = (((a_|_ v b_|_) ^ (a v b_|_)) ^ 0)
29		an0 100	. . . . . . 7 (((a_|_ v b_|_) ^ (a v b_|_)) ^ 0) = 0
30	28, 29	ax-r2 35	. . . . . 6 (((a_|_ v b_|_) ^ (a v b_|_)) ^ ((a v b) ^ (b_|_ ^ a_|_))) = 0
31	19, 30	ax-r2 35	. . . . 5 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ (b_|_ ^ a_|_)) = 0
32		coman2 178	. . . . . . . . . . 11 (b ^ a) C a
33	32	comcom2 175	. . . . . . . . . 10 (b ^ a) C a_|_
34		coman1 177	. . . . . . . . . . 11 (b ^ a) C b
35	34	comcom2 175	. . . . . . . . . 10 (b ^ a) C b_|_
36	33, 35	com2or 465	. . . . . . . . 9 (b ^ a) C (a_|_ v b_|_)
37	32, 35	com2or 465	. . . . . . . . 9 (b ^ a) C (a v b_|_)
38	36, 37	com2an 466	. . . . . . . 8 (b ^ a) C ((a_|_ v b_|_) ^ (a v b_|_))
39	32, 34	com2or 465	. . . . . . . 8 (b ^ a) C (a v b)
40	38, 39	com2an 466	. . . . . . 7 (b ^ a) C (((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b))
41	35, 32	com2an 466	. . . . . . 7 (b ^ a) C (b_|_ ^ a)
42	40, 41	fh2 452	. . . . . 6 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ ((b ^ a) v (b_|_ ^ a))) = (((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ (b ^ a)) v ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ (b_|_ ^ a)))
43		an32 76	. . . . . . . . 9 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ (b ^ a)) = ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (b ^ a)) ^ (a v b))
44		an32 76	. . . . . . . . . . . 12 (((a_|_ v b_|_) ^ (a v b_|_)) ^ (b ^ a)) = (((a_|_ v b_|_) ^ (b ^ a)) ^ (a v b_|_))
45		ax-a2 30	. . . . . . . . . . . . . . . 16 (a_|_ v b_|_) = (b_|_ v a_|_)
46		df-a 39	. . . . . . . . . . . . . . . 16 (b ^ a) = (b_|_ v a_|_)_|_
47	45, 46	2an 72	. . . . . . . . . . . . . . 15 ((a_|_ v b_|_) ^ (b ^ a)) = ((b_|_ v a_|_) ^ (b_|_ v a_|_)_|_)
48		dff 93	. . . . . . . . . . . . . . . 16 0 = ((b_|_ v a_|_) ^ (b_|_ v a_|_)_|_)
49	48	ax-r1 34	. . . . . . . . . . . . . . 15 ((b_|_ v a_|_) ^ (b_|_ v a_|_)_|_) = 0
50	47, 49	ax-r2 35	. . . . . . . . . . . . . 14 ((a_|_ v b_|_) ^ (b ^ a)) = 0
51	50	ran 71	. . . . . . . . . . . . 13 (((a_|_ v b_|_) ^ (b ^ a)) ^ (a v b_|_)) = (0 ^ (a v b_|_))
52		an0r 101	. . . . . . . . . . . . 13 (0 ^ (a v b_|_)) = 0
53	51, 52	ax-r2 35	. . . . . . . . . . . 12 (((a_|_ v b_|_) ^ (b ^ a)) ^ (a v b_|_)) = 0
54	44, 53	ax-r2 35	. . . . . . . . . . 11 (((a_|_ v b_|_) ^ (a v b_|_)) ^ (b ^ a)) = 0
55	54	ran 71	. . . . . . . . . 10 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (b ^ a)) ^ (a v b)) = (0 ^ (a v b))
56		an0r 101	. . . . . . . . . 10 (0 ^ (a v b)) = 0
57	55, 56	ax-r2 35	. . . . . . . . 9 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (b ^ a)) ^ (a v b)) = 0
58	43, 57	ax-r2 35	. . . . . . . 8 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ (b ^ a)) = 0
59		lea 152	. . . . . . . . . . . 12 (b_|_ ^ a) =< b_|_
60		leor 151	. . . . . . . . . . . . 13 b_|_ =< (a_|_ v b_|_)
61		leor 151	. . . . . . . . . . . . 13 b_|_ =< (a v b_|_)
62	60, 61	ler2an 165	. . . . . . . . . . . 12 b_|_ =< ((a_|_ v b_|_) ^ (a v b_|_))
63	59, 62	letr 129	. . . . . . . . . . 11 (b_|_ ^ a) =< ((a_|_ v b_|_) ^ (a v b_|_))
64		lear 153	. . . . . . . . . . . 12 (b_|_ ^ a) =< a
65		leo 150	. . . . . . . . . . . 12 a =< (a v b)
66	64, 65	letr 129	. . . . . . . . . . 11 (b_|_ ^ a) =< (a v b)
67	63, 66	ler2an 165	. . . . . . . . . 10 (b_|_ ^ a) =< (((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b))
68	67	df2le2 128	. . . . . . . . 9 ((b_|_ ^ a) ^ (((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b))) = (b_|_ ^ a)
69		ancom 68	. . . . . . . . 9 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ (b_|_ ^ a)) = ((b_|_ ^ a) ^ (((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)))
70		ancom 68	. . . . . . . . 9 (a ^ b_|_) = (b_|_ ^ a)
71	68, 69, 70	3tr1 60	. . . . . . . 8 ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ (b_|_ ^ a)) = (a ^ b_|_)
72	58, 71	2or 67	. . . . . . 7 (((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ (b ^ a)) v ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ (b_|_ ^ a))) = (0 v (a ^ b_|_))
73		or0r 95	. . . . . . 7 (0 v (a ^ b_|_)) = (a ^ b_|_)
74	72, 73	ax-r2 35	. . . . . 6 (((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ (b ^ a)) v ((((a_|_ v b_|_) ^ (a v b_|_)) ^ (a v b)) ^ (b_|_ ^ a))) = (a ^ b_|_)
75	42, 74	ax-r2 35	. . . . 5 ((((