Metamath Proof Explorer

Theorem elat2

Description: Expanded membership relation for the set of atoms, i.e. the predicate "is an atom (of the Hilbert lattice)." An atom is a nonzero element of a lattice such that anything less than it is zero, i.e. it is the smallest nonzero element of the lattice. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion elat2 
|- ( A e. HAtoms <-> ( A e. CH /\ ( A =/= 0H /\ A. x e. CH ( x C_ A -> ( x = A \/ x = 0H ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ela 
 |-  ( A e. HAtoms <-> ( A e. CH /\ 0H
2 h0elch 
 |-  0H e. CH
3 cvbr2 
 |-  ( ( 0H e. CH /\ A e. CH ) -> ( 0H  ( 0H C. A /\ A. x e. CH ( ( 0H C. x /\ x C_ A ) -> x = A ) ) ) )
4 2 3 mpan 
 |-  ( A e. CH -> ( 0H  ( 0H C. A /\ A. x e. CH ( ( 0H C. x /\ x C_ A ) -> x = A ) ) ) )
5 ch0pss 
 |-  ( A e. CH -> ( 0H C. A <-> A =/= 0H ) )
6 ch0pss 
 |-  ( x e. CH -> ( 0H C. x <-> x =/= 0H ) )
7 6 imbi1d 
 |-  ( x e. CH -> ( ( 0H C. x -> x = A ) <-> ( x =/= 0H -> x = A ) ) )
8 7 imbi2d 
 |-  ( x e. CH -> ( ( x C_ A -> ( 0H C. x -> x = A ) ) <-> ( x C_ A -> ( x =/= 0H -> x = A ) ) ) )
9 impexp 
 |-  ( ( ( 0H C. x /\ x C_ A ) -> x = A ) <-> ( 0H C. x -> ( x C_ A -> x = A ) ) )
10 bi2.04 
 |-  ( ( 0H C. x -> ( x C_ A -> x = A ) ) <-> ( x C_ A -> ( 0H C. x -> x = A ) ) )
11 9 10 bitri 
 |-  ( ( ( 0H C. x /\ x C_ A ) -> x = A ) <-> ( x C_ A -> ( 0H C. x -> x = A ) ) )
12 orcom 
 |-  ( ( x = A \/ x = 0H ) <-> ( x = 0H \/ x = A ) )
13 neor 
 |-  ( ( x = 0H \/ x = A ) <-> ( x =/= 0H -> x = A ) )
14 12 13 bitri 
 |-  ( ( x = A \/ x = 0H ) <-> ( x =/= 0H -> x = A ) )
15 14 imbi2i 
 |-  ( ( x C_ A -> ( x = A \/ x = 0H ) ) <-> ( x C_ A -> ( x =/= 0H -> x = A ) ) )
16 8 11 15 3bitr4g 
 |-  ( x e. CH -> ( ( ( 0H C. x /\ x C_ A ) -> x = A ) <-> ( x C_ A -> ( x = A \/ x = 0H ) ) ) )
17 16 ralbiia 
 |-  ( A. x e. CH ( ( 0H C. x /\ x C_ A ) -> x = A ) <-> A. x e. CH ( x C_ A -> ( x = A \/ x = 0H ) ) )
18 17 a1i 
 |-  ( A e. CH -> ( A. x e. CH ( ( 0H C. x /\ x C_ A ) -> x = A ) <-> A. x e. CH ( x C_ A -> ( x = A \/ x = 0H ) ) ) )
19 5 18 anbi12d 
 |-  ( A e. CH -> ( ( 0H C. A /\ A. x e. CH ( ( 0H C. x /\ x C_ A ) -> x = A ) ) <-> ( A =/= 0H /\ A. x e. CH ( x C_ A -> ( x = A \/ x = 0H ) ) ) ) )
20 4 19 bitr2d 
 |-  ( A e. CH -> ( ( A =/= 0H /\ A. x e. CH ( x C_ A -> ( x = A \/ x = 0H ) ) ) <-> 0H
21 20 pm5.32i 
 |-  ( ( A e. CH /\ ( A =/= 0H /\ A. x e. CH ( x C_ A -> ( x = A \/ x = 0H ) ) ) ) <-> ( A e. CH /\ 0H
22 1 21 bitr4i 
 |-  ( A e. HAtoms <-> ( A e. CH /\ ( A =/= 0H /\ A. x e. CH ( x C_ A -> ( x = A \/ x = 0H ) ) ) ) )