Definition df-id3 52

Description: Define asymmetrical identity (for "Non-Orthomodular Models..." paper). (Contributed by NM, 7-Feb-1999.)

Assertion

Ref	Expression
df-id3	(a ≡3 b) = ((a⊥ ∪ b) ∩ (a ∪ (a⊥ ∩ b⊥ )))

Detailed syntax breakdown of Definition df-id3

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

This definition is referenced by:  nomb32  300  nom23  316  nom54  335  lem3.3.7i3e1  1066  lem3.3.7i3e2  1067  wdid0id3  1114