Definition df-id2 50

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

Assertion

Ref	Expression
df-id2	(a ≡2 b) = ((a ∪ b⊥ ) ∩ (b ∪ (a⊥ ∩ b⊥ )))

Detailed syntax breakdown of Definition df-id2

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

This definition is referenced by:  nomb32 292  nomcon1 294  nomcon2 295  nom22 307  nom51 324

metamath.org