Theorem atcvat2

Description: A Hilbert lattice element covered by the join of two distinct atoms is an atom. (Contributed by NM, 29-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	atcvat2	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( ¬ 𝐵 = 𝐶 ∧ 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) → 𝐴 ∈ HAtoms ) )

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) )
2	1	anbi2d	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ( ¬ 𝐵 = 𝐶 ∧ 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) ↔ ( ¬ 𝐵 = 𝐶 ∧ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) ) )
3		eleq1	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( 𝐴 ∈ HAtoms ↔ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∈ HAtoms ) )
4	2 3	imbi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ( ( ¬ 𝐵 = 𝐶 ∧ 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) → 𝐴 ∈ HAtoms ) ↔ ( ( ¬ 𝐵 = 𝐶 ∧ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) → if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∈ HAtoms ) ) )
5	4	imbi2d	⊢ ( 𝐴 = if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) → ( ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( ¬ 𝐵 = 𝐶 ∧ 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) → 𝐴 ∈ HAtoms ) ) ↔ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( ¬ 𝐵 = 𝐶 ∧ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) → if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∈ HAtoms ) ) ) )
6		h0elch	⊢ 0ℋ ∈ Cℋ
7	6	elimel	⊢ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∈ Cℋ
8	7	atcvat2i	⊢ ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( ¬ 𝐵 = 𝐶 ∧ if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) → if ( 𝐴 ∈ Cℋ , 𝐴 , 0ℋ ) ∈ HAtoms ) )
9	5 8	dedth	⊢ ( 𝐴 ∈ Cℋ → ( ( 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( ¬ 𝐵 = 𝐶 ∧ 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) → 𝐴 ∈ HAtoms ) ) )
10	9	3impib	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( ¬ 𝐵 = 𝐶 ∧ 𝐴 ⋖ℋ ( 𝐵 ∨ℋ 𝐶 ) ) → 𝐴 ∈ HAtoms ) )