Theorem atoml2i

Description: An assertion holding in atomic orthomodular lattices that is equivalent to the exchange axiom. Proposition P8(ii) of BeltramettiCassinelli1 p. 400. (Contributed by NM, 12-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	atoml.1	⊢ 𝐴 ∈ Cℋ
Assertion	atoml2i	⊢ ( ( 𝐵 ∈ HAtoms ∧ ¬ 𝐵 ⊆ 𝐴 ) → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms )

Proof

Step	Hyp	Ref	Expression
1		atoml.1	⊢ 𝐴 ∈ Cℋ
2		atelch	⊢ ( 𝐵 ∈ HAtoms → 𝐵 ∈ Cℋ )
3		pjoml5	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( 𝐴 ∨ℋ 𝐵 ) )
4	1 2 3	sylancr	⊢ ( 𝐵 ∈ HAtoms → ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( 𝐴 ∨ℋ 𝐵 ) )
5		incom	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) )
6	5	eqeq1i	⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ↔ ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 0ℋ )
7	6	biimpi	⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ → ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 0ℋ )
8	7	oveq2d	⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ → ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( 𝐴 ∨ℋ 0ℋ ) )
9	1	chj0i	⊢ ( 𝐴 ∨ℋ 0ℋ ) = 𝐴
10	8 9	eqtrdi	⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ → ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = 𝐴 )
11	4 10	sylan9req	⊢ ( ( 𝐵 ∈ HAtoms ∧ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = 𝐴 )
12	11	ex	⊢ ( 𝐵 ∈ HAtoms → ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ → ( 𝐴 ∨ℋ 𝐵 ) = 𝐴 ) )
13		chlejb2	⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∨ℋ 𝐵 ) = 𝐴 ) )
14	2 1 13	sylancl	⊢ ( 𝐵 ∈ HAtoms → ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∨ℋ 𝐵 ) = 𝐴 ) )
15	12 14	sylibrd	⊢ ( 𝐵 ∈ HAtoms → ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ → 𝐵 ⊆ 𝐴 ) )
16	15	con3d	⊢ ( 𝐵 ∈ HAtoms → ( ¬ 𝐵 ⊆ 𝐴 → ¬ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ) )
17	1	atomli	⊢ ( 𝐵 ∈ HAtoms → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ ( HAtoms ∪ { 0ℋ } ) )
18		elun	⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ ( HAtoms ∪ { 0ℋ } ) ↔ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ { 0ℋ } ) )
19		h0elch	⊢ 0ℋ ∈ Cℋ
20	19	elexi	⊢ 0ℋ ∈ V
21	20	elsn2	⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ { 0ℋ } ↔ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ )
22	21	orbi2i	⊢ ( ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ { 0ℋ } ) ↔ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ) )
23		orcom	⊢ ( ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ) ↔ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ∨ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
24	18 22 23	3bitri	⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ ( HAtoms ∪ { 0ℋ } ) ↔ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ∨ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
25	17 24	sylib	⊢ ( 𝐵 ∈ HAtoms → ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ∨ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
26	25	ord	⊢ ( 𝐵 ∈ HAtoms → ( ¬ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
27	16 26	syld	⊢ ( 𝐵 ∈ HAtoms → ( ¬ 𝐵 ⊆ 𝐴 → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) )
28	27	imp	⊢ ( ( 𝐵 ∈ HAtoms ∧ ¬ 𝐵 ⊆ 𝐴 ) → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms )