Theorem 1oa 802

Description: Orthoarguesian-like law with →₁ instead of →₀ but true in all OMLs.

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 153	. . 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 74	. . . . 5 (a⊥ ∩ (b⊥ ∩ c⊥ )) = (b⊥ ∩ (a⊥ ∩ c⊥ ))
3		lear 153	. . . . . 6 (b⊥ ∩ (a⊥ ∩ c⊥ )) ≤ (a⊥ ∩ c⊥ )
4	3	lerr 142	. . . . 5 (b⊥ ∩ (a⊥ ∩ c⊥ )) ≤ (c ∪ (a⊥ ∩ c⊥ ))
5	2, 4	bltr 130	. . . 4 (a⊥ ∩ (b⊥ ∩ c⊥ )) ≤ (c ∪ (a⊥ ∩ c⊥ ))
6		leid 140	. . . 4 (c ∪ (a⊥ ∩ c⊥ )) ≤ (c ∪ (a⊥ ∩ c⊥ ))
7	5, 6	lel2or 162	. . 3 ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (c ∪ (a⊥ ∩ c⊥ ))) ≤ (c ∪ (a⊥ ∩ c⊥ ))
8	1, 7	letr 129	. 2 ((((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ c)) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ )))) ∩ ((a⊥ ∩ (b⊥ ∩ c⊥ )) ∪ (c ∪ (a⊥ ∩ c⊥ )))) ≤ (c ∪ (a⊥ ∩ c⊥ ))
9		df-i1 43	. . . 4 ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c))) = ((b ∪ c)⊥ ∪ ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c))))
10	9	lan 70	. . 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 74	. . . . . 6 ((a →2 b) ∩ ((b ∪ c) ∩ (a →2 c))) = ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c)))
12	11	ax-r1 34	. . . . 5 ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c))) = ((a →2 b) ∩ ((b ∪ c) ∩ (a →2 c)))
13		coman1 177	. . . . 5 ((a →2 b) ∩ ((b ∪ c) ∩ (a →2 c))) C (a →2 b)
14	12, 13	bctr 173	. . . 4 ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c))) C (a →2 b)
15		coman1 177	. . . . 5 ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c))) C (b ∪ c)
16	15	comcom2 175	. . . 4 ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c))) C (b ∪ c)⊥
17	14, 16	fh2c 459	. . 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 44	. . . . . . 7 (a →2 b) = (b ∪ (a⊥ ∩ b⊥ ))
19		anor3 82	. . . . . . . 8 (b⊥ ∩ c⊥ ) = (b ∪ c)⊥
20	19	ax-r1 34	. . . . . . 7 (b ∪ c)⊥ = (b⊥ ∩ c⊥ )
21	18, 20	2an 72	. . . . . 6 ((a →2 b) ∩ (b ∪ c)⊥ ) = ((b ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ c⊥ ))
22		comid 179	. . . . . . . . . . 11 b C b
23	22	comcom3 436	. . . . . . . . . 10 b⊥ C b
24		comanr2 447	. . . . . . . . . 10 b⊥ C (a⊥ ∩ b⊥ )
25	23, 24	fh1r 455	. . . . . . . . 9 ((b ∪ (a⊥ ∩ b⊥ )) ∩ b⊥ ) = ((b ∩ b⊥ ) ∪ ((a⊥ ∩ b⊥ ) ∩ b⊥ ))
26		dff 93	. . . . . . . . . . 11 0 = (b ∩ b⊥ )
27	26	ax-r1 34	. . . . . . . . . 10 (b ∩ b⊥ ) = 0
28		anass 69	. . . . . . . . . . 11 ((a⊥ ∩ b⊥ ) ∩ b⊥ ) = (a⊥ ∩ (b⊥ ∩ b⊥ ))
29		anidm 103	. . . . . . . . . . . 12 (b⊥ ∩ b⊥ ) = b⊥
30	29	lan 70	. . . . . . . . . . 11 (a⊥ ∩ (b⊥ ∩ b⊥ )) = (a⊥ ∩ b⊥ )
31	28, 30	ax-r2 35	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
32	27, 31	2or 67	. . . . . . . . 9 ((b ∩ b⊥ ) ∪ ((a⊥ ∩ b⊥ ) ∩ b⊥ )) = (0 ∪ (a⊥ ∩ b⊥ ))
33		ax-a2 30	. . . . . . . . . 10 (0 ∪ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b⊥ ) ∪ 0)
34		or0 94	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∪ 0) = (a⊥ ∩ b⊥ )
35	33, 34	ax-r2 35	. . . . . . . . 9 (0 ∪ (a⊥ ∩ b⊥ )) = (a⊥ ∩ b⊥ )
36	25, 32, 35	3tr 62	. . . . . . . 8 ((b ∪ (a⊥ ∩ b⊥ )) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
37	36	ran 71	. . . . . . 7 (((b ∪ (a⊥ ∩ b⊥ )) ∩ b⊥ ) ∩ c⊥ ) = ((a⊥ ∩ b⊥ ) ∩ c⊥ )
38		anass 69	. . . . . . 7 (((b ∪ (a⊥ ∩ b⊥ )) ∩ b⊥ ) ∩ c⊥ ) = ((b ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ c⊥ ))
39		anass 69	. . . . . . 7 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) = (a⊥ ∩ (b⊥ ∩ c⊥ ))
40	37, 38, 39	3tr2 61	. . . . . 6 ((b ∪ (a⊥ ∩ b⊥ )) ∩ (b⊥ ∩ c⊥ )) = (a⊥ ∩ (b⊥ ∩ c⊥ ))
41	21, 40	ax-r2 35	. . . . 5 ((a →2 b) ∩ (b ∪ c)⊥ ) = (a⊥ ∩ (b⊥ ∩ c⊥ ))
42		an12 74	. . . . . 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 69	. . . . . . . . 9 (((a →2 b) ∩ (a →2 b)) ∩ (a →2 c)) = ((a →2 b) ∩ ((a →2 b) ∩ (a →2 c)))
44	43	ax-r1 34	. . . . . . . 8 ((a →2 b) ∩ ((a →2 b) ∩ (a →2 c))) = (((a →2 b) ∩ (a →2 b)) ∩ (a →2 c))
45		anidm 103	. . . . . . . . . 10 ((a →2 b) ∩ (a →2 b)) = (a →2 b)
46	45, 18	ax-r2 35	. . . . . . . . 9 ((a →2 b) ∩ (a →2 b)) = (b ∪ (a⊥ ∩ b⊥ ))
47		df-i2 44	. . . . . . . . 9 (a →2 c) = (c ∪ (a⊥ ∩ c⊥ ))
48	46, 47	2an 72	. . . . . . . 8 (((a →2 b) ∩ (a →2 b)) ∩ (a →2 c)) = ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))
49	44, 48	ax-r2 35	. . . . . . 7 ((a →2 b) ∩ ((a →2 b) ∩ (a →2 c))) = ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))
50	49	lan 70	. . . . . 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 35	. . . . 5 ((a →2 b) ∩ ((b ∪ c) ∩ ((a →2 b) ∩ (a →2 c)))) = ((b ∪ c) ∩ ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ ))))
52	41, 51	2or 67	. . . 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 34	. . . . . . . 8 (a⊥ ∩ (b⊥ ∩ c⊥ )) = ((a⊥ ∩ b⊥ ) ∩ c⊥ )
54		lea 152	. . . . . . . . . 10 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) ≤ (a⊥ ∩ b⊥ )
55	54	lerr 142	. . . . . . . . 9 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) ≤ (b ∪ (a⊥ ∩ b⊥ ))
56	55	lecom 172	. . . . . . . 8 ((a⊥ ∩ b⊥ ) ∩ c⊥ ) C (b ∪ (a⊥ ∩ b⊥ ))
57	53, 56	bctr 173	. . . . . . 7 (a⊥ ∩ (b⊥ ∩ c⊥ )) C (b ∪ (a⊥ ∩ b⊥ ))
58	4	lecom 172	. . . . . . . 8 (b⊥ ∩ (a⊥ ∩ c⊥ )) C (c ∪ (a⊥ ∩ c⊥ ))
59	2, 58	bctr 173	. . . . . . 7 (a⊥ ∩ (b⊥ ∩ c⊥ )) C (c ∪ (a⊥ ∩ c⊥ ))
60	57, 59	fh3 453	. . . . . 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 70	. . . . 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 178	. . . . . . . 8 (a⊥ ∩ (b⊥ ∩ c⊥ )) C (b⊥ ∩ c⊥ )
63	62	comcom2 175	. . . . . . 7 (a⊥ ∩ (b⊥ ∩ c⊥ )) C (b⊥ ∩ c⊥ )⊥
64		oran 79	. . . . . . . 8 (b ∪ c) = (b⊥ ∩ c⊥ )⊥
65	64	ax-r1 34	. . . . . . 7 (b⊥ ∩ c⊥ )⊥ = (b ∪ c)
66	63, 65	cbtr 174	. . . . . 6 (a⊥ ∩ (b⊥ ∩ c⊥ )) C (b ∪ c)
67	57, 59	com2an 466	. . . . . 6 (a⊥ ∩ (b⊥ ∩ c⊥ )) C ((b ∪ (a⊥ ∩ b⊥ )) ∩ (c ∪ (a⊥ ∩ c⊥ )))
68	66, 67	fh3 453	. . . . 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 69	. . . . 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 60	. . . 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 35	. . 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 62	. 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 132	1 ((a →2 b) ∩ ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))) ≤ (a →2 c)

Syntax hints:   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  0wf 10   →₁ wi1 13   →₂ wi2 14

This theorem is referenced by:  1oai1 803  1oaiii 805  distoa 924

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-i2 44  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org