Theorem id5leid0 351

Description: Quantum identity is less than classical identity. (Contributed by NM, 4-Mar-2006.)

Assertion

Ref	Expression
id5leid0	(a ≡ b) ≤ (a ≡0 b)

Proof of Theorem id5leid0

Step	Hyp	Ref	Expression
1		ax-a2 31	. . 3 ((a ∩ b) ∪ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b⊥ ) ∪ (a ∩ b))
2		lea 160	. . . . 5 (a⊥ ∩ b⊥ ) ≤ a⊥
3		lear 161	. . . . 5 (a ∩ b) ≤ b
4	2, 3	le2or 168	. . . 4 ((a⊥ ∩ b⊥ ) ∪ (a ∩ b)) ≤ (a⊥ ∪ b)
5		lear 161	. . . . 5 (a⊥ ∩ b⊥ ) ≤ b⊥
6		lea 160	. . . . 5 (a ∩ b) ≤ a
7	5, 6	le2or 168	. . . 4 ((a⊥ ∩ b⊥ ) ∪ (a ∩ b)) ≤ (b⊥ ∪ a)
8	4, 7	ler2an 173	. . 3 ((a⊥ ∩ b⊥ ) ∪ (a ∩ b)) ≤ ((a⊥ ∪ b) ∩ (b⊥ ∪ a))
9	1, 8	bltr 138	. 2 ((a ∩ b) ∪ (a⊥ ∩ b⊥ )) ≤ ((a⊥ ∪ b) ∩ (b⊥ ∪ a))
10		dfb 94	. 2 (a ≡ b) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
11		df-id0 49	. 2 (a ≡0 b) = ((a⊥ ∪ b) ∩ (b⊥ ∪ a))
12	9, 10, 11	le3tr1 140	1 (a ≡ b) ≤ (a ≡0 b)

This proof depends on syntax axioms:   ≤ wle 2  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7   ≡₀ wid0 17

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-id0 49  df-le1 130  df-le2 131

This theorem is used by:  id5id0  352