# Metamath Proof Explorer

## Theorem meeteu

Description: Uniqueness of meet of elements in the domain. (Contributed by NM, 12-Sep-2018)

Ref Expression
Hypotheses meetval2.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
meetval2.l
meetval2.m
meetval2.k ${⊢}{\phi }\to {K}\in {V}$
meetval2.x ${⊢}{\phi }\to {X}\in {B}$
meetval2.y ${⊢}{\phi }\to {Y}\in {B}$
meetlem.e
Assertion meeteu

### Proof

Step Hyp Ref Expression
1 meetval2.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 meetval2.l
3 meetval2.m
4 meetval2.k ${⊢}{\phi }\to {K}\in {V}$
5 meetval2.x ${⊢}{\phi }\to {X}\in {B}$
6 meetval2.y ${⊢}{\phi }\to {Y}\in {B}$
7 meetlem.e
8 eqid ${⊢}\mathrm{glb}\left({K}\right)=\mathrm{glb}\left({K}\right)$
9 8 3 4 5 6 meetdef
10 biid
11 4 adantr ${⊢}\left({\phi }\wedge \left\{{X},{Y}\right\}\in \mathrm{dom}\mathrm{glb}\left({K}\right)\right)\to {K}\in {V}$
12 simpr ${⊢}\left({\phi }\wedge \left\{{X},{Y}\right\}\in \mathrm{dom}\mathrm{glb}\left({K}\right)\right)\to \left\{{X},{Y}\right\}\in \mathrm{dom}\mathrm{glb}\left({K}\right)$
13 1 2 8 10 11 12 glbeu
14 13 ex
15 1 2 3 4 5 6 meetval2lem
16 5 6 15 syl2anc
17 16 reubidv
18 14 17 sylibd
19 9 18 sylbid
20 7 19 mpd