Theorem u24lem 770

Description: Lemma for unified implication study. (Contributed by NM, 20-Dec-1997.)

Assertion

Ref	Expression
u24lem	((a →2 b) ∩ (a →4 b)) = (a →5 b)

Proof of Theorem u24lem

Step	Hyp	Ref	Expression
1		df-i2 45	. . 3 (a →2 b) = (b ∪ (a⊥ ∩ b⊥ ))
2	1	ran 78	. 2 ((a →2 b) ∩ (a →4 b)) = ((b ∪ (a⊥ ∩ b⊥ )) ∩ (a →4 b))
3		u4lemc1 683	. . . 4 b C (a →4 b)
4		comanr2 465	. . . . 5 b⊥ C (a⊥ ∩ b⊥ )
5	4	comcom6 459	. . . 4 b C (a⊥ ∩ b⊥ )
6	3, 5	fh2r 474	. . 3 ((b ∪ (a⊥ ∩ b⊥ )) ∩ (a →4 b)) = ((b ∩ (a →4 b)) ∪ ((a⊥ ∩ b⊥ ) ∩ (a →4 b)))
7		ancom 74	. . . . . 6 (b ∩ (a →4 b)) = ((a →4 b) ∩ b)
8		ancom 74	. . . . . 6 ((a →4 b) ∩ b) = (b ∩ (a →4 b))
9	7, 8	ax-r2 36	. . . . 5 (b ∩ (a →4 b)) = (b ∩ (a →4 b))
10		anass 76	. . . . . 6 ((a⊥ ∩ b⊥ ) ∩ (a →4 b)) = (a⊥ ∩ (b⊥ ∩ (a →4 b)))
11		ancom 74	. . . . . . . . 9 (b⊥ ∩ (a →4 b)) = ((a →4 b) ∩ b⊥ )
12		u4lemanb 618	. . . . . . . . 9 ((a →4 b) ∩ b⊥ ) = ((a⊥ ∪ b) ∩ b⊥ )
13	11, 12	ax-r2 36	. . . . . . . 8 (b⊥ ∩ (a →4 b)) = ((a⊥ ∪ b) ∩ b⊥ )
14	13	lan 77	. . . . . . 7 (a⊥ ∩ (b⊥ ∩ (a →4 b))) = (a⊥ ∩ ((a⊥ ∪ b) ∩ b⊥ ))
15		anass 76	. . . . . . . . 9 ((a⊥ ∩ (a⊥ ∪ b)) ∩ b⊥ ) = (a⊥ ∩ ((a⊥ ∪ b) ∩ b⊥ ))
16	15	ax-r1 35	. . . . . . . 8 (a⊥ ∩ ((a⊥ ∪ b) ∩ b⊥ )) = ((a⊥ ∩ (a⊥ ∪ b)) ∩ b⊥ )
17		anabs 121	. . . . . . . . . 10 (a⊥ ∩ (a⊥ ∪ b)) = a⊥
18	17	ran 78	. . . . . . . . 9 ((a⊥ ∩ (a⊥ ∪ b)) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
19		ancom 74	. . . . . . . . 9 (a⊥ ∩ b⊥ ) = (b⊥ ∩ a⊥ )
20	18, 19	ax-r2 36	. . . . . . . 8 ((a⊥ ∩ (a⊥ ∪ b)) ∩ b⊥ ) = (b⊥ ∩ a⊥ )
21	16, 20	ax-r2 36	. . . . . . 7 (a⊥ ∩ ((a⊥ ∪ b) ∩ b⊥ )) = (b⊥ ∩ a⊥ )
22	14, 21	ax-r2 36	. . . . . 6 (a⊥ ∩ (b⊥ ∩ (a →4 b))) = (b⊥ ∩ a⊥ )
23	10, 22	ax-r2 36	. . . . 5 ((a⊥ ∩ b⊥ ) ∩ (a →4 b)) = (b⊥ ∩ a⊥ )
24	9, 23	2or 72	. . . 4 ((b ∩ (a →4 b)) ∪ ((a⊥ ∩ b⊥ ) ∩ (a →4 b))) = ((b ∩ (a →4 b)) ∪ (b⊥ ∩ a⊥ ))
25		comanr1 464	. . . . . . 7 b⊥ C (b⊥ ∩ a⊥ )
26	25	comcom6 459	. . . . . 6 b C (b⊥ ∩ a⊥ )
27	26, 3	fh4r 476	. . . . 5 ((b ∩ (a →4 b)) ∪ (b⊥ ∩ a⊥ )) = ((b ∪ (b⊥ ∩ a⊥ )) ∩ ((a →4 b) ∪ (b⊥ ∩ a⊥ )))
28	3, 26	com2or 483	. . . . . . 7 b C ((a →4 b) ∪ (b⊥ ∩ a⊥ ))
29	28, 26	fh2r 474	. . . . . 6 ((b ∪ (b⊥ ∩ a⊥ )) ∩ ((a →4 b) ∪ (b⊥ ∩ a⊥ ))) = ((b ∩ ((a →4 b) ∪ (b⊥ ∩ a⊥ ))) ∪ ((b⊥ ∩ a⊥ ) ∩ ((a →4 b) ∪ (b⊥ ∩ a⊥ ))))
30	3, 26	fh1 469	. . . . . . . . 9 (b ∩ ((a →4 b) ∪ (b⊥ ∩ a⊥ ))) = ((b ∩ (a →4 b)) ∪ (b ∩ (b⊥ ∩ a⊥ )))
31		u4lemab 613	. . . . . . . . . . . 12 ((a →4 b) ∩ b) = ((a ∩ b) ∪ (a⊥ ∩ b))
32	7, 31	ax-r2 36	. . . . . . . . . . 11 (b ∩ (a →4 b)) = ((a ∩ b) ∪ (a⊥ ∩ b))
33	32	ax-r5 38	. . . . . . . . . 10 ((b ∩ (a →4 b)) ∪ (b ∩ (b⊥ ∩ a⊥ ))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (b ∩ (b⊥ ∩ a⊥ )))
34		id 59	. . . . . . . . . 10 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (b ∩ (b⊥ ∩ a⊥ ))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (b ∩ (b⊥ ∩ a⊥ )))
35	33, 34	ax-r2 36	. . . . . . . . 9 ((b ∩ (a →4 b)) ∪ (b ∩ (b⊥ ∩ a⊥ ))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (b ∩ (b⊥ ∩ a⊥ )))
36	30, 35	ax-r2 36	. . . . . . . 8 (b ∩ ((a →4 b) ∪ (b⊥ ∩ a⊥ ))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (b ∩ (b⊥ ∩ a⊥ )))
37		leor 159	. . . . . . . . 9 (b⊥ ∩ a⊥ ) ≤ ((a →4 b) ∪ (b⊥ ∩ a⊥ ))
38	37	df2le2 136	. . . . . . . 8 ((b⊥ ∩ a⊥ ) ∩ ((a →4 b) ∪ (b⊥ ∩ a⊥ ))) = (b⊥ ∩ a⊥ )
39	36, 38	2or 72	. . . . . . 7 ((b ∩ ((a →4 b) ∪ (b⊥ ∩ a⊥ ))) ∪ ((b⊥ ∩ a⊥ ) ∩ ((a →4 b) ∪ (b⊥ ∩ a⊥ )))) = ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (b ∩ (b⊥ ∩ a⊥ ))) ∪ (b⊥ ∩ a⊥ ))
40		ax-a3 32	. . . . . . . 8 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (b ∩ (b⊥ ∩ a⊥ ))) ∪ (b⊥ ∩ a⊥ )) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((b ∩ (b⊥ ∩ a⊥ )) ∪ (b⊥ ∩ a⊥ )))
41		lear 161	. . . . . . . . . . . 12 (b ∩ (b⊥ ∩ a⊥ )) ≤ (b⊥ ∩ a⊥ )
42	41	df-le2 131	. . . . . . . . . . 11 ((b ∩ (b⊥ ∩ a⊥ )) ∪ (b⊥ ∩ a⊥ )) = (b⊥ ∩ a⊥ )
43		ancom 74	. . . . . . . . . . 11 (b⊥ ∩ a⊥ ) = (a⊥ ∩ b⊥ )
44	42, 43	ax-r2 36	. . . . . . . . . 10 ((b ∩ (b⊥ ∩ a⊥ )) ∪ (b⊥ ∩ a⊥ )) = (a⊥ ∩ b⊥ )
45	44	lor 70	. . . . . . . . 9 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((b ∩ (b⊥ ∩ a⊥ )) ∪ (b⊥ ∩ a⊥ ))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))
46		df-i5 48	. . . . . . . . . . 11 (a →5 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))
47	46	ax-r1 35	. . . . . . . . . 10 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) = (a →5 b)
48		id 59	. . . . . . . . . 10 (a →5 b) = (a →5 b)
49	47, 48	ax-r2 36	. . . . . . . . 9 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ )) = (a →5 b)
50	45, 49	ax-r2 36	. . . . . . . 8 (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((b ∩ (b⊥ ∩ a⊥ )) ∪ (b⊥ ∩ a⊥ ))) = (a →5 b)
51	40, 50	ax-r2 36	. . . . . . 7 ((((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (b ∩ (b⊥ ∩ a⊥ ))) ∪ (b⊥ ∩ a⊥ )) = (a →5 b)
52	39, 51	ax-r2 36	. . . . . 6 ((b ∩ ((a →4 b) ∪ (b⊥ ∩ a⊥ ))) ∪ ((b⊥ ∩ a⊥ ) ∩ ((a →4 b) ∪ (b⊥ ∩ a⊥ )))) = (a →5 b)
53	29, 52	ax-r2 36	. . . . 5 ((b ∪ (b⊥ ∩ a⊥ )) ∩ ((a →4 b) ∪ (b⊥ ∩ a⊥ ))) = (a →5 b)
54	27, 53	ax-r2 36	. . . 4 ((b ∩ (a →4 b)) ∪ (b⊥ ∩ a⊥ )) = (a →5 b)
55	24, 54	ax-r2 36	. . 3 ((b ∩ (a →4 b)) ∪ ((a⊥ ∩ b⊥ ) ∩ (a →4 b))) = (a →5 b)
56	6, 55	ax-r2 36	. 2 ((b ∪ (a⊥ ∩ b⊥ )) ∩ (a →4 b)) = (a →5 b)
57	2, 56	ax-r2 36	1 ((a →2 b) ∩ (a →4 b)) = (a →5 b)

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   →₂ wi2 13   →₄ wi4 15   →₅ wi5 16

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-i2 45  df-i4 47  df-i5 48  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  negant5  863