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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
isatlat.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
isatlat.l ⊢ ≤ = ( le ‘ 𝐾 )
isatlat.z ⊢ 0 = ( 0. ‘ 𝐾 )
isatlat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion isatl ( 𝐾 ∈ AtLat ↔ ( 𝐾 ∈ Lat ∧ 𝐵 ∈ dom 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≠ 0 → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 isatlat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 isatlat.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
3 isatlat.l ⊢ ≤ = ( le ‘ 𝐾 )
4 isatlat.z ⊢ 0 = ( 0. ‘ 𝐾 )
5 isatlat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = ( Base ‘ 𝐾 ) )
7 6 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = 𝐵 )
8 fveq2 ⊢ ( 𝑘 = 𝐾 → ( glb ‘ 𝑘 ) = ( glb ‘ 𝐾 ) )
9 8 2 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( glb ‘ 𝑘 ) = 𝐺 )
10 9 dmeqd ⊢ ( 𝑘 = 𝐾 → dom ( glb ‘ 𝑘 ) = dom 𝐺 )
11 7 10 eleq12d ⊢ ( 𝑘 = 𝐾 → ( ( Base ‘ 𝑘 ) ∈ dom ( glb ‘ 𝑘 ) ↔ 𝐵 ∈ dom 𝐺 ) )
12 fveq2 ⊢ ( 𝑘 = 𝐾 → ( 0. ‘ 𝑘 ) = ( 0. ‘ 𝐾 ) )
13 12 4 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( 0. ‘ 𝑘 ) = 0 )
14 13 neeq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑥 ≠ ( 0. ‘ 𝑘 ) ↔ 𝑥 ≠ 0 ) )
15 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
16 15 5 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
17 fveq2 ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
18 17 3 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ≤ )
19 18 breqd ⊢ ( 𝑘 = 𝐾 → ( 𝑦 ( le ‘ 𝑘 ) 𝑥 ↔ 𝑦 ≤ 𝑥 ) )
20 16 19 rexeqbidv ⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑦 ∈ ( Atoms ‘ 𝑘 ) 𝑦 ( le ‘ 𝑘 ) 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
21 14 20 imbi12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑦 ∈ ( Atoms ‘ 𝑘 ) 𝑦 ( le ‘ 𝑘 ) 𝑥 ) ↔ ( 𝑥 ≠ 0 → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ) )
22 7 21 raleqbidv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑦 ∈ ( Atoms ‘ 𝑘 ) 𝑦 ( le ‘ 𝑘 ) 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≠ 0 → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ) )
23 11 22 anbi12d ⊢ ( 𝑘 = 𝐾 → ( ( ( Base ‘ 𝑘 ) ∈ dom ( glb ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑦 ∈ ( Atoms ‘ 𝑘 ) 𝑦 ( le ‘ 𝑘 ) 𝑥 ) ) ↔ ( 𝐵 ∈ dom 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≠ 0 → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ) ) )
24 df-atl ⊢ AtLat = { 𝑘 ∈ Lat ∣ ( ( Base ‘ 𝑘 ) ∈ dom ( glb ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑦 ∈ ( Atoms ‘ 𝑘 ) 𝑦 ( le ‘ 𝑘 ) 𝑥 ) ) }
25 23 24 elrab2 ⊢ ( 𝐾 ∈ AtLat ↔ ( 𝐾 ∈ Lat ∧ ( 𝐵 ∈ dom 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≠ 0 → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ) ) )
26 3anass ⊢ ( ( 𝐾 ∈ Lat ∧ 𝐵 ∈ dom 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≠ 0 → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ) ↔ ( 𝐾 ∈ Lat ∧ ( 𝐵 ∈ dom 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≠ 0 → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ) ) )
27 25 26 bitr4i ⊢ ( 𝐾 ∈ AtLat ↔ ( 𝐾 ∈ Lat ∧ 𝐵 ∈ dom 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≠ 0 → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ) )