Theorem 2oalem1 825

Description: Lemma for OA-like stuff with →₂ instead of →₀ . (Contributed by NM, 15-Nov-1998.)

Assertion

Ref	Expression
2oalem1	((a →2 b)⊥ ∪ ((b ∪ c) ∪ ((a →2 b) ∩ (a →2 c)))) = 1

Proof of Theorem 2oalem1

Step	Hyp	Ref	Expression
1		or12 80	. 2 ((a →2 b)⊥ ∪ ((b ∪ c) ∪ ((a →2 b) ∩ (a →2 c)))) = ((b ∪ c) ∪ ((a →2 b)⊥ ∪ ((a →2 b) ∩ (a →2 c))))
2		ud2lem0c 278	. . . 4 (a →2 b)⊥ = (b⊥ ∩ (a ∪ b))
3		df-i2 45	. . . . 5 (a →2 b) = (b ∪ (a⊥ ∩ b⊥ ))
4		df-i2 45	. . . . 5 (a →2 c) = (c ∪ (a⊥ ∩ c⊥ ))
5	3, 4	2an 79	. . . 4 ((a →2 b) ∩ (a →2 c)) = ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))
6	2, 5	2or 72	. . 3 ((a →2 b)⊥ ∪ ((a →2 b) ∩ (a →2 c))) = ((b⊥ ∩ (a ∪ b)) ∪ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ ))))
7	6	lor 70	. 2 ((b ∪ c) ∪ ((a →2 b)⊥ ∪ ((a →2 b) ∩ (a →2 c)))) = ((b ∪ c) ∪ ((b⊥ ∩ (a ∪ b)) ∪ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))))
8		or32 82	. . . . 5 ((b ∪ c) ∪ (b⊥ ∩ (a ∪ b))) = ((b ∪ (b⊥ ∩ (a ∪ b))) ∪ c)
9		oml 445	. . . . . . 7 (b ∪ (b⊥ ∩ (b ∪ a))) = (b ∪ a)
10		ax-a2 31	. . . . . . . . 9 (a ∪ b) = (b ∪ a)
11	10	lan 77	. . . . . . . 8 (b⊥ ∩ (a ∪ b)) = (b⊥ ∩ (b ∪ a))
12	11	lor 70	. . . . . . 7 (b ∪ (b⊥ ∩ (a ∪ b))) = (b ∪ (b⊥ ∩ (b ∪ a)))
13	9, 12, 10	3tr1 63	. . . . . 6 (b ∪ (b⊥ ∩ (a ∪ b))) = (a ∪ b)
14	13	ax-r5 38	. . . . 5 ((b ∪ (b⊥ ∩ (a ∪ b))) ∪ c) = ((a ∪ b) ∪ c)
15	8, 14	ax-r2 36	. . . 4 ((b ∪ c) ∪ (b⊥ ∩ (a ∪ b))) = ((a ∪ b) ∪ c)
16	15	ax-r5 38	. . 3 (((b ∪ c) ∪ (b⊥ ∩ (a ∪ b))) ∪ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))) = (((a ∪ b) ∪ c) ∪ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ ))))
17		ax-a3 32	. . 3 (((b ∪ c) ∪ (b⊥ ∩ (a ∪ b))) ∪ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))) = ((b ∪ c) ∪ ((b⊥ ∩ (a ∪ b)) ∪ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))))
18		oran 87	. . . . . . . . . . . . 13 (a ∪ b) = (a⊥ ∩ b⊥ )⊥
19	18	lan 77	. . . . . . . . . . . 12 (b⊥ ∩ (a ∪ b)) = (b⊥ ∩ (a⊥ ∩ b⊥ )⊥ )
20		anor3 90	. . . . . . . . . . . 12 (b⊥ ∩ (a⊥ ∩ b⊥ )⊥ ) = (b ∪ (a⊥ ∩ b⊥ ))⊥
21	19, 20	ax-r2 36	. . . . . . . . . . 11 (b⊥ ∩ (a ∪ b)) = (b ∪ (a⊥ ∩ b⊥ ))⊥
22	21	ax-r1 35	. . . . . . . . . 10 (b ∪ (a⊥ ∩ b⊥ ))⊥ = (b⊥ ∩ (a ∪ b))
23		lear 161	. . . . . . . . . 10 (b⊥ ∩ (a ∪ b)) ≤ (a ∪ b)
24	22, 23	bltr 138	. . . . . . . . 9 (b ∪ (a⊥ ∩ b⊥ ))⊥ ≤ (a ∪ b)
25		leo 158	. . . . . . . . 9 (a ∪ b) ≤ ((a ∪ b) ∪ c)
26	24, 25	letr 137	. . . . . . . 8 (b ∪ (a⊥ ∩ b⊥ ))⊥ ≤ ((a ∪ b) ∪ c)
27	26	lecom 180	. . . . . . 7 (b ∪ (a⊥ ∩ b⊥ ))⊥ C ((a ∪ b) ∪ c)
28	27	comcom6 459	. . . . . 6 (b ∪ (a⊥ ∩ b⊥ )) C ((a ∪ b) ∪ c)
29	28	comcom 453	. . . . 5 ((a ∪ b) ∪ c) C (b ∪ (a⊥ ∩ b⊥ ))
30		lear 161	. . . . . . . . . 10 (c⊥ ∩ (a ∪ c)) ≤ (a ∪ c)
31		leo 158	. . . . . . . . . 10 (a ∪ c) ≤ ((a ∪ c) ∪ b)
32	30, 31	letr 137	. . . . . . . . 9 (c⊥ ∩ (a ∪ c)) ≤ ((a ∪ c) ∪ b)
33		oran 87	. . . . . . . . . . 11 (a ∪ c) = (a⊥ ∩ c⊥ )⊥
34	33	lan 77	. . . . . . . . . 10 (c⊥ ∩ (a ∪ c)) = (c⊥ ∩ (a⊥ ∩ c⊥ )⊥ )
35		anor3 90	. . . . . . . . . 10 (c⊥ ∩ (a⊥ ∩ c⊥ )⊥ ) = (c ∪ (a⊥ ∩ c⊥ ))⊥
36	34, 35	ax-r2 36	. . . . . . . . 9 (c⊥ ∩ (a ∪ c)) = (c ∪ (a⊥ ∩ c⊥ ))⊥
37		or32 82	. . . . . . . . 9 ((a ∪ c) ∪ b) = ((a ∪ b) ∪ c)
38	32, 36, 37	le3tr2 141	. . . . . . . 8 (c ∪ (a⊥ ∩ c⊥ ))⊥ ≤ ((a ∪ b) ∪ c)
39	38	lecom 180	. . . . . . 7 (c ∪ (a⊥ ∩ c⊥ ))⊥ C ((a ∪ b) ∪ c)
40	39	comcom6 459	. . . . . 6 (c ∪ (a⊥ ∩ c⊥ )) C ((a ∪ b) ∪ c)
41	40	comcom 453	. . . . 5 ((a ∪ b) ∪ c) C (c ∪ (a⊥ ∩ c⊥ ))
42	29, 41	fh3 471	. . . 4 (((a ∪ b) ∪ c) ∪ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))) = ((((a ∪ b) ∪ c) ∪ (b ∪ (a⊥ ∩ b⊥ ))) ∩ (((a ∪ b) ∪ c) ∪ (c ∪ (a⊥ ∩ c⊥ ))))
43		or12 80	. . . . . 6 (((a ∪ b) ∪ c) ∪ (b ∪ (a⊥ ∩ b⊥ ))) = (b ∪ (((a ∪ b) ∪ c) ∪ (a⊥ ∩ b⊥ )))
44		or32 82	. . . . . . . 8 (((a ∪ b) ∪ c) ∪ (a⊥ ∩ b⊥ )) = (((a ∪ b) ∪ (a⊥ ∩ b⊥ )) ∪ c)
45		ax-a2 31	. . . . . . . 8 (((a ∪ b) ∪ (a⊥ ∩ b⊥ )) ∪ c) = (c ∪ ((a ∪ b) ∪ (a⊥ ∩ b⊥ )))
46		anor3 90	. . . . . . . . . . . 12 (a⊥ ∩ b⊥ ) = (a ∪ b)⊥
47	46	lor 70	. . . . . . . . . . 11 ((a ∪ b) ∪ (a⊥ ∩ b⊥ )) = ((a ∪ b) ∪ (a ∪ b)⊥ )
48		df-t 41	. . . . . . . . . . . 12 1 = ((a ∪ b) ∪ (a ∪ b)⊥ )
49	48	ax-r1 35	. . . . . . . . . . 11 ((a ∪ b) ∪ (a ∪ b)⊥ ) = 1
50	47, 49	ax-r2 36	. . . . . . . . . 10 ((a ∪ b) ∪ (a⊥ ∩ b⊥ )) = 1
51	50	lor 70	. . . . . . . . 9 (c ∪ ((a ∪ b) ∪ (a⊥ ∩ b⊥ ))) = (c ∪ 1)
52		or1 104	. . . . . . . . 9 (c ∪ 1) = 1
53	51, 52	ax-r2 36	. . . . . . . 8 (c ∪ ((a ∪ b) ∪ (a⊥ ∩ b⊥ ))) = 1
54	44, 45, 53	3tr 65	. . . . . . 7 (((a ∪ b) ∪ c) ∪ (a⊥ ∩ b⊥ )) = 1
55	54	lor 70	. . . . . 6 (b ∪ (((a ∪ b) ∪ c) ∪ (a⊥ ∩ b⊥ ))) = (b ∪ 1)
56		or1 104	. . . . . 6 (b ∪ 1) = 1
57	43, 55, 56	3tr 65	. . . . 5 (((a ∪ b) ∪ c) ∪ (b ∪ (a⊥ ∩ b⊥ ))) = 1
58		or12 80	. . . . . 6 (((a ∪ b) ∪ c) ∪ (c ∪ (a⊥ ∩ c⊥ ))) = (c ∪ (((a ∪ b) ∪ c) ∪ (a⊥ ∩ c⊥ )))
59		or32 82	. . . . . . . . . 10 ((a ∪ b) ∪ c) = ((a ∪ c) ∪ b)
60		ax-a2 31	. . . . . . . . . 10 ((a ∪ c) ∪ b) = (b ∪ (a ∪ c))
61	59, 60	ax-r2 36	. . . . . . . . 9 ((a ∪ b) ∪ c) = (b ∪ (a ∪ c))
62	61	ax-r5 38	. . . . . . . 8 (((a ∪ b) ∪ c) ∪ (a⊥ ∩ c⊥ )) = ((b ∪ (a ∪ c)) ∪ (a⊥ ∩ c⊥ ))
63		ax-a3 32	. . . . . . . 8 ((b ∪ (a ∪ c)) ∪ (a⊥ ∩ c⊥ )) = (b ∪ ((a ∪ c) ∪ (a⊥ ∩ c⊥ )))
64		anor3 90	. . . . . . . . . . . 12 (a⊥ ∩ c⊥ ) = (a ∪ c)⊥
65	64	lor 70	. . . . . . . . . . 11 ((a ∪ c) ∪ (a⊥ ∩ c⊥ )) = ((a ∪ c) ∪ (a ∪ c)⊥ )
66		df-t 41	. . . . . . . . . . . 12 1 = ((a ∪ c) ∪ (a ∪ c)⊥ )
67	66	ax-r1 35	. . . . . . . . . . 11 ((a ∪ c) ∪ (a ∪ c)⊥ ) = 1
68	65, 67	ax-r2 36	. . . . . . . . . 10 ((a ∪ c) ∪ (a⊥ ∩ c⊥ )) = 1
69	68	lor 70	. . . . . . . . 9 (b ∪ ((a ∪ c) ∪ (a⊥ ∩ c⊥ ))) = (b ∪ 1)
70	69, 56	ax-r2 36	. . . . . . . 8 (b ∪ ((a ∪ c) ∪ (a⊥ ∩ c⊥ ))) = 1
71	62, 63, 70	3tr 65	. . . . . . 7 (((a ∪ b) ∪ c) ∪ (a⊥ ∩ c⊥ )) = 1
72	71	lor 70	. . . . . 6 (c ∪ (((a ∪ b) ∪ c) ∪ (a⊥ ∩ c⊥ ))) = (c ∪ 1)
73	58, 72, 52	3tr 65	. . . . 5 (((a ∪ b) ∪ c) ∪ (c ∪ (a⊥ ∩ c⊥ ))) = 1
74	57, 73	2an 79	. . . 4 ((((a ∪ b) ∪ c) ∪ (b ∪ (a⊥ ∩ b⊥ ))) ∩ (((a ∪ b) ∪ c) ∪ (c ∪ (a⊥ ∩ c⊥ )))) = (1 ∩ 1)
75		anidm 111	. . . 4 (1 ∩ 1) = 1
76	42, 74, 75	3tr 65	. . 3 (((a ∪ b) ∪ c) ∪ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))) = 1
77	16, 17, 76	3tr2 64	. 2 ((b ∪ c) ∪ ((b⊥ ∩ (a ∪ b)) ∪ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ ))))) = 1
78	1, 7, 77	3tr 65	1 ((a →2 b)⊥ ∪ ((b ∪ c) ∪ ((a →2 b) ∩ (a →2 c)))) = 1

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   →₂ wi2 13

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

This theorem is used by:  2oath1  826