# Metamath Proof Explorer

## Theorem islat

Description: The predicate "is a lattice." (Contributed by NM, 18-Oct-2012) (Revised by NM, 12-Sep-2018)

Ref Expression
Hypotheses islat.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
islat.j
islat.m
Assertion islat

### Proof

Step Hyp Ref Expression
1 islat.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 islat.j
3 islat.m
4 fveq2 ${⊢}{l}={K}\to \mathrm{join}\left({l}\right)=\mathrm{join}\left({K}\right)$
5 4 2 eqtr4di
6 5 dmeqd
7 fveq2 ${⊢}{l}={K}\to {\mathrm{Base}}_{{l}}={\mathrm{Base}}_{{K}}$
8 7 1 eqtr4di ${⊢}{l}={K}\to {\mathrm{Base}}_{{l}}={B}$
9 8 sqxpeqd ${⊢}{l}={K}\to {\mathrm{Base}}_{{l}}×{\mathrm{Base}}_{{l}}={B}×{B}$
10 6 9 eqeq12d
11 fveq2 ${⊢}{l}={K}\to \mathrm{meet}\left({l}\right)=\mathrm{meet}\left({K}\right)$
12 11 3 eqtr4di
13 12 dmeqd
14 13 9 eqeq12d
15 10 14 anbi12d
16 df-lat ${⊢}\mathrm{Lat}=\left\{{l}\in \mathrm{Poset}|\left(\mathrm{dom}\mathrm{join}\left({l}\right)={\mathrm{Base}}_{{l}}×{\mathrm{Base}}_{{l}}\wedge \mathrm{dom}\mathrm{meet}\left({l}\right)={\mathrm{Base}}_{{l}}×{\mathrm{Base}}_{{l}}\right)\right\}$
17 15 16 elrab2