This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )