Theorem lei3 238

Description: L.e. to Kalmbach implication.

Hypothesis

Ref	Expression
lei3.1	a ≤ b

Assertion

Ref	Expression
lei3	(a →3 b) = 1

Proof of Theorem lei3

Step	Hyp	Ref	Expression
1		ax-a3 31	. . 3 (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b))) = ((a⊥ ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a ∩ (a⊥ ∪ b))))
2		ax-a2 30	. . . . 5 (b⊥ ∪ a) = (a ∪ b⊥ )
3		ancom 68	. . . . . . 7 (a⊥ ∩ b⊥ ) = (b⊥ ∩ a⊥ )
4		lei3.1	. . . . . . . . 9 a ≤ b
5	4	lecon 146	. . . . . . . 8 b⊥ ≤ a⊥
6	5	df2le2 128	. . . . . . 7 (b⊥ ∩ a⊥ ) = b⊥
7	3, 6	ax-r2 35	. . . . . 6 (a⊥ ∩ b⊥ ) = b⊥
8	4	sklem 222	. . . . . . . 8 (a⊥ ∪ b) = 1
9	8	lan 70	. . . . . . 7 (a ∩ (a⊥ ∪ b)) = (a ∩ 1)
10		an1 98	. . . . . . 7 (a ∩ 1) = a
11	9, 10	ax-r2 35	. . . . . 6 (a ∩ (a⊥ ∪ b)) = a
12	7, 11	2or 67	. . . . 5 ((a⊥ ∩ b⊥ ) ∪ (a ∩ (a⊥ ∪ b))) = (b⊥ ∪ a)
13		anor2 81	. . . . . 6 (a⊥ ∩ b) = (a ∪ b⊥ )⊥
14	13	con2 64	. . . . 5 (a⊥ ∩ b)⊥ = (a ∪ b⊥ )
15	2, 12, 14	3tr1 60	. . . 4 ((a⊥ ∩ b⊥ ) ∪ (a ∩ (a⊥ ∪ b))) = (a⊥ ∩ b)⊥
16	15	lor 66	. . 3 ((a⊥ ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a ∩ (a⊥ ∪ b)))) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b)⊥ )
17	1, 16	ax-r2 35	. 2 (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b))) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b)⊥ )
18		df-i3 45	. 2 (a →3 b) = (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b)))
19		df-t 40	. 2 1 = ((a⊥ ∩ b) ∪ (a⊥ ∩ b)⊥ )
20	17, 18, 19	3tr1 60	1 (a →3 b) = 1

Syntax hints:   = wb 1   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 9   →₃ wi3 15

This theorem is referenced by:  bina3 276  bina4 277  bina5 278  bii3 498  binr1 499  binr2 500  binr3 501  i3ri3 520  i3li3 521  i32i3 522  i3th5 529  i3th7 531  i3th8 532

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

This theorem depends on definitions:  df-a 39  df-t 40  df-f 41  df-i3 45  df-le1 122  df-le2 123

metamath.org