Definition df-id5 1046

Description: Define asymmetrical identity (for "Non-Orthomodular Models..." paper).

Assertion

Ref	Expression
df-id5	(a ≡5 b) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))

Detailed syntax breakdown of Definition df-id5

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3	1, 2	wid5 22	. 2 term  (a ≡5 b)
4	1, 2	wa 7	. . 3 term  (a ∩ b)
5	1	wn 4	. . . 4 term  a⊥
6	2	wn 4	. . . 4 term  b⊥
7	5, 6	wa 7	. . 3 term  (a⊥ ∩ b⊥ )
8	4, 7	wo 6	. 2 term  ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
9	3, 8	wb 1	1 wff  (a ≡5 b) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))

This definition is referenced by:  lem3.3.3lem1 1048  lem3.3.3lem2 1049  lem3.3.4 1052  lem3.3.7i5e1 1071  lem3.3.7i5e2 1072  lem3.4.3 1075  lem3.4.6 1078

Copyright terms: Public domain