Theorem 1oa 820

Description: Orthoarguesian-like law with →₁ instead of →₀ but true in all OMLs. (Contributed by NM, 1-Nov-1998.)

Assertion

Ref	Expression
1oa	((a →2 b) ∩ ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))) ≤ (a →2 c)

Proof of Theorem 1oa

Step	Hyp	Ref	Expression
1		lear 161	. . 3 ((((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ c)) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ )))) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (c ∪ (a⊥ ∩ c⊥ )))) ≤ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (c ∪ (a⊥ ∩ c⊥ )))
2		an12 81	. . . . 5 (a⊥ ∩ (b⊥ ∩ c⊥ )) = (b⊥ ∩ (a⊥ ∩ c⊥ ))
3		lear 161	. . . . . 6 (b⊥ ∩ (a⊥ ∩ c⊥ )) ≤ (a⊥ ∩ c⊥ )
4	3	lerr 150	. . . . 5 (b⊥ ∩ (a⊥ ∩ c⊥ )) ≤ (c ∪ (a⊥ ∩ c⊥ ))
5	2, 4	bltr 138	. . . 4 (a⊥ ∩ (b⊥ ∩ c⊥ )) ≤ (c ∪ (a⊥ ∩ c⊥ ))
6		leid 148	. . . 4 (c ∪ (a⊥ ∩ c⊥ )) ≤ (c ∪ (a⊥ ∩ c⊥ ))
7	5, 6	lel2or 170	. . 3 ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (c ∪ (a⊥ ∩ c⊥ ))) ≤ (c ∪ (a⊥ ∩ c⊥ ))
8	1, 7	letr 137	. 2 ((((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ c)) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ )))) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (c ∪ (a⊥ ∩ c⊥ )))) ≤ (c ∪ (a⊥ ∩ c⊥ ))
9		df-i1 44	. . . 4 ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c))) = ((b ∪ c)⊥ ∪ ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c))))
10	9	lan 77	. . 3 ((a →2 b) ∩ ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))) = ((a →2 b) ∩ ((b ∪ c)⊥ ∪ ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c)))))
11		an12 81	. . . . . 6 ((a →2 b) ∩ ((b ∪ c) ∩ (a →2 c))) = ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c)))
12	11	ax-r1 35	. . . . 5 ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c))) = ((a →2 b) ∩ ((b ∪ c) ∩ (a →2 c)))
13		coman1 185	. . . . 5 ((a →2 b) ∩ ((b ∪ c) ∩ (a →2 c))) C (a →2 b)
14	12, 13	bctr 181	. . . 4 ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c))) C (a →2 b)
15		coman1 185	. . . . 5 ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c))) C (b ∪ c)
16	15	comcom2 183	. . . 4 ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c))) C (b ∪ c)⊥
17	14, 16	fh2c 477	. . 3 ((a →2 b) ∩ ((b ∪ c)⊥ ∪ ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c))))) = (((a →2 b) ∩ (b ∪ c)⊥ ) ∪ ((a →2 b) ∩ ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c)))))
18		df-i2 45	. . . . . . 7 (a →2 b) = (b ∪ (a⊥ ∩ b⊥ ))
19		anor3 90	. . . . . . . 8 (b⊥ ∩ c⊥ ) = (b ∪ c)⊥
20	19	ax-r1 35	. . . . . . 7 (b ∪ c)⊥ = (b⊥ ∩ c⊥ )
21	18, 20	2an 79	. . . . . 6 ((a →2 b) ∩ (b ∪ c)⊥ ) = ((b ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ c⊥ ))
22		comid 187	. . . . . . . . . . 11 b C b
23	22	comcom3 454	. . . . . . . . . 10 b⊥ C b
24		comanr2 465	. . . . . . . . . 10 b⊥ C (a⊥ ∩ b⊥ )
25	23, 24	fh1r 473	. . . . . . . . 9 ((b ∪ (a⊥ ∩ b⊥ )) ∩ b⊥ ) = ((b ∩ b⊥ ) ∪ ((a⊥ ∩ b⊥ ) ∩ b⊥ ))
26		dff 101	. . . . . . . . . . 11 0 = (b ∩ b⊥ )
27	26	ax-r1 35	. . . . . . . . . 10 (b ∩ b⊥ ) = 0
28		anass 76	. . . . . . . . . . 11 ((a⊥ ∩ b⊥ ) ∩ b⊥ ) = (a⊥ ∩ (b⊥ ∩ b⊥ ))
29		anidm 111	. . . . . . . . . . . 12 (b⊥ ∩ b⊥ ) = b⊥
30	29	lan 77	. . . . . . . . . . 11 (a⊥ ∩ (b⊥ ∩ b⊥ )) = (a⊥ ∩ b⊥ )
31	28, 30	ax-r2 36	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
32	27, 31	2or 72	. . . . . . . . 9 ((b ∩ b⊥ ) ∪ ((a⊥ ∩ b⊥ ) ∩ b⊥ )) = (0 ∪ (a⊥ ∩ b⊥ ))
33		ax-a2 31	. . . . . . . . . 10 (0 ∪ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b⊥ ) ∪ 0)
34		or0 102	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∪ 0) = (a⊥ ∩ b⊥ )
35	33, 34	ax-r2 36	. . . . . . . . 9 (0 ∪ (a⊥ ∩ b⊥ )) = (a⊥ ∩ b⊥ )
36	25, 32, 35	3tr 65	. . . . . . . 8 ((b ∪ (a⊥ ∩ b⊥ )) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
37	36	ran 78	. . . . . . 7 (((b ∪ (a⊥ ∩ b⊥ )) ∩ b⊥ ) ∩ c⊥ ) = ((a⊥ ∩ b⊥ ) ∩ c⊥ )
38		anass 76	. . . . . . 7 (((b ∪ (a⊥ ∩ b⊥ )) ∩ b⊥ ) ∩ c⊥ ) = ((b ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ c⊥ ))
39		anass 76	. . . . . . 7 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) = (a⊥ ∩ (b⊥ ∩ c⊥ ))
40	37, 38, 39	3tr2 64	. . . . . 6 ((b ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ c⊥ )) = (a⊥ ∩ (b⊥ ∩ c⊥ ))
41	21, 40	ax-r2 36	. . . . 5 ((a →2 b) ∩ (b ∪ c)⊥ ) = (a⊥ ∩ (b⊥ ∩ c⊥ ))
42		an12 81	. . . . . 6 ((a →2 b) ∩ ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c)))) = ((b ∪ c) ∩ ((a →2 b) ∩ ((a →2 b) ∩ (a →2 c))))
43		anass 76	. . . . . . . . 9 (((a →2 b) ∩ (a →2 b)) ∩ (a →2 c)) = ((a →2 b) ∩ ((a →2 b) ∩ (a →2 c)))
44	43	ax-r1 35	. . . . . . . 8 ((a →2 b) ∩ ((a →2 b) ∩ (a →2 c))) = (((a →2 b) ∩ (a →2 b)) ∩ (a →2 c))
45		anidm 111	. . . . . . . . . 10 ((a →2 b) ∩ (a →2 b)) = (a →2 b)
46	45, 18	ax-r2 36	. . . . . . . . 9 ((a →2 b) ∩ (a →2 b)) = (b ∪ (a⊥ ∩ b⊥ ))
47		df-i2 45	. . . . . . . . 9 (a →2 c) = (c ∪ (a⊥ ∩ c⊥ ))
48	46, 47	2an 79	. . . . . . . 8 (((a →2 b) ∩ (a →2 b)) ∩ (a →2 c)) = ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))
49	44, 48	ax-r2 36	. . . . . . 7 ((a →2 b) ∩ ((a →2 b) ∩ (a →2 c))) = ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))
50	49	lan 77	. . . . . 6 ((b ∪ c) ∩ ((a →2 b) ∩ ((a →2 b) ∩ (a →2 c)))) = ((b ∪ c) ∩ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ ))))
51	42, 50	ax-r2 36	. . . . 5 ((a →2 b) ∩ ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c)))) = ((b ∪ c) ∩ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ ))))
52	41, 51	2or 72	. . . 4 (((a →2 b) ∩ (b ∪ c)⊥ ) ∪ ((a →2 b) ∩ ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c))))) = ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ ((b ∪ c) ∩ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))))
53	39	ax-r1 35	. . . . . . . 8 (a⊥ ∩ (b⊥ ∩ c⊥ )) = ((a⊥ ∩ b⊥ ) ∩ c⊥ )
54		lea 160	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) ≤ (a⊥ ∩ b⊥ )
55	54	lerr 150	. . . . . . . . 9 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) ≤ (b ∪ (a⊥ ∩ b⊥ ))
56	55	lecom 180	. . . . . . . 8 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) C (b ∪ (a⊥ ∩ b⊥ ))
57	53, 56	bctr 181	. . . . . . 7 (a⊥ ∩ (b⊥ ∩ c⊥ )) C (b ∪ (a⊥ ∩ b⊥ ))
58	4	lecom 180	. . . . . . . 8 (b⊥ ∩ (a⊥ ∩ c⊥ )) C (c ∪ (a⊥ ∩ c⊥ ))
59	2, 58	bctr 181	. . . . . . 7 (a⊥ ∩ (b⊥ ∩ c⊥ )) C (c ∪ (a⊥ ∩ c⊥ ))
60	57, 59	fh3 471	. . . . . 6 ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))) = (((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ ))) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (c ∪ (a⊥ ∩ c⊥ ))))
61	60	lan 77	. . . . 5 (((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ c)) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ ))))) = (((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ c)) ∩ (((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ ))) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (c ∪ (a⊥ ∩ c⊥ )))))
62		coman2 186	. . . . . . . 8 (a⊥ ∩ (b⊥ ∩ c⊥ )) C (b⊥ ∩ c⊥ )
63	62	comcom2 183	. . . . . . 7 (a⊥ ∩ (b⊥ ∩ c⊥ )) C (b⊥ ∩ c⊥ )⊥
64		oran 87	. . . . . . . 8 (b ∪ c) = (b⊥ ∩ c⊥ )⊥
65	64	ax-r1 35	. . . . . . 7 (b⊥ ∩ c⊥ )⊥ = (b ∪ c)
66	63, 65	cbtr 182	. . . . . 6 (a⊥ ∩ (b⊥ ∩ c⊥ )) C (b ∪ c)
67	57, 59	com2an 484	. . . . . 6 (a⊥ ∩ (b⊥ ∩ c⊥ )) C ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))
68	66, 67	fh3 471	. . . . 5 ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ ((b ∪ c) ∩ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ ))))) = (((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ c)) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))))
69		anass 76	. . . . 5 ((((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ c)) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ )))) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (c ∪ (a⊥ ∩ c⊥ )))) = (((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ c)) ∩ (((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ ))) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (c ∪ (a⊥ ∩ c⊥ )))))
70	61, 68, 69	3tr1 63	. . . 4 ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ ((b ∪ c) ∩ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ ))))) = ((((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ c)) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ )))) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (c ∪ (a⊥ ∩ c⊥ ))))
71	52, 70	ax-r2 36	. . 3 (((a →2 b) ∩ (b ∪ c)⊥ ) ∪ ((a →2 b) ∩ ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c))))) = ((((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ c)) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ )))) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (c ∪ (a⊥ ∩ c⊥ ))))
72	10, 17, 71	3tr 65	. 2 ((a →2 b) ∩ ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))) = ((((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ c)) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ )))) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (c ∪ (a⊥ ∩ c⊥ ))))
73	8, 72, 47	le3tr1 140	1 ((a →2 b) ∩ ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))) ≤ (a →2 c)

This proof depends on syntax axioms:   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  0wf 9   →₁ wi1 12   →₂ 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-i1 44  df-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by:  1oai1  821  1oaiii  823  distoa  944