Metamath Proof Explorer

Theorem isatl

Description: The predicate "is an atomic lattice." Every nonzero element is less than or equal to an atom. (Contributed by NM, 18-Sep-2011) (Revised by NM, 14-Sep-2018)

Ref Expression
Hypotheses isatlat.b 
|- B = ( Base ` K )
isatlat.g 
|- G = ( glb ` K )
isatlat.l 
|- .<_ = ( le ` K )
isatlat.z 
|- .0. = ( 0. ` K )
isatlat.a 
|- A = ( Atoms ` K )
Assertion isatl 
|- ( K e. AtLat <-> ( K e. Lat /\ B e. dom G /\ A. x e. B ( x =/= .0. -> E. y e. A y .<_ x ) ) )

Proof

Step Hyp Ref Expression
1 isatlat.b 
 |-  B = ( Base ` K )
2 isatlat.g 
 |-  G = ( glb ` K )
3 isatlat.l 
 |-  .<_ = ( le ` K )
4 isatlat.z 
 |-  .0. = ( 0. ` K )
5 isatlat.a 
 |-  A = ( Atoms ` K )
6 fveq2 
 |-  ( k = K -> ( Base ` k ) = ( Base ` K ) )
7 6 1 eqtr4di 
 |-  ( k = K -> ( Base ` k ) = B )
8 fveq2 
 |-  ( k = K -> ( glb ` k ) = ( glb ` K ) )
9 8 2 eqtr4di 
 |-  ( k = K -> ( glb ` k ) = G )
10 9 dmeqd 
 |-  ( k = K -> dom ( glb ` k ) = dom G )
11 7 10 eleq12d 
 |-  ( k = K -> ( ( Base ` k ) e. dom ( glb ` k ) <-> B e. dom G ) )
12 fveq2 
 |-  ( k = K -> ( 0. ` k ) = ( 0. ` K ) )
13 12 4 eqtr4di 
 |-  ( k = K -> ( 0. ` k ) = .0. )
14 13 neeq2d 
 |-  ( k = K -> ( x =/= ( 0. ` k ) <-> x =/= .0. ) )
15 fveq2 
 |-  ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
16 15 5 eqtr4di 
 |-  ( k = K -> ( Atoms ` k ) = A )
17 fveq2 
 |-  ( k = K -> ( le ` k ) = ( le ` K ) )
18 17 3 eqtr4di 
 |-  ( k = K -> ( le ` k ) = .<_ )
19 18 breqd 
 |-  ( k = K -> ( y ( le ` k ) x <-> y .<_ x ) )
20 16 19 rexeqbidv 
 |-  ( k = K -> ( E. y e. ( Atoms ` k ) y ( le ` k ) x <-> E. y e. A y .<_ x ) )
21 14 20 imbi12d 
 |-  ( k = K -> ( ( x =/= ( 0. ` k ) -> E. y e. ( Atoms ` k ) y ( le ` k ) x ) <-> ( x =/= .0. -> E. y e. A y .<_ x ) ) )
22 7 21 raleqbidv 
 |-  ( k = K -> ( A. x e. ( Base ` k ) ( x =/= ( 0. ` k ) -> E. y e. ( Atoms ` k ) y ( le ` k ) x ) <-> A. x e. B ( x =/= .0. -> E. y e. A y .<_ x ) ) )
23 11 22 anbi12d 
 |-  ( k = K -> ( ( ( Base ` k ) e. dom ( glb ` k ) /\ A. x e. ( Base ` k ) ( x =/= ( 0. ` k ) -> E. y e. ( Atoms ` k ) y ( le ` k ) x ) ) <-> ( B e. dom G /\ A. x e. B ( x =/= .0. -> E. y e. A y .<_ x ) ) ) )
24 df-atl 
 |-  AtLat = { k e. Lat | ( ( Base ` k ) e. dom ( glb ` k ) /\ A. x e. ( Base ` k ) ( x =/= ( 0. ` k ) -> E. y e. ( Atoms ` k ) y ( le ` k ) x ) ) }
25 23 24 elrab2 
 |-  ( K e. AtLat <-> ( K e. Lat /\ ( B e. dom G /\ A. x e. B ( x =/= .0. -> E. y e. A y .<_ x ) ) ) )
26 3anass 
 |-  ( ( K e. Lat /\ B e. dom G /\ A. x e. B ( x =/= .0. -> E. y e. A y .<_ x ) ) <-> ( K e. Lat /\ ( B e. dom G /\ A. x e. B ( x =/= .0. -> E. y e. A y .<_ x ) ) ) )
27 25 26 bitr4i 
 |-  ( K e. AtLat <-> ( K e. Lat /\ B e. dom G /\ A. x e. B ( x =/= .0. -> E. y e. A y .<_ x ) ) )