# Metamath Proof Explorer

## Theorem latmlem12

Description: Add join to both sides of a lattice ordering. ( ss2in analog.) (Contributed by NM, 10-Nov-2011)

Ref Expression
Hypotheses latmle.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
latmle.l
latmle.m
Assertion latmlem12

### Proof

Step Hyp Ref Expression
1 latmle.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 latmle.l
3 latmle.m
4 simp1 ${⊢}\left({K}\in \mathrm{Lat}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({Z}\in {B}\wedge {W}\in {B}\right)\right)\to {K}\in \mathrm{Lat}$
5 simp2l ${⊢}\left({K}\in \mathrm{Lat}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({Z}\in {B}\wedge {W}\in {B}\right)\right)\to {X}\in {B}$
6 simp2r ${⊢}\left({K}\in \mathrm{Lat}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({Z}\in {B}\wedge {W}\in {B}\right)\right)\to {Y}\in {B}$
7 simp3l ${⊢}\left({K}\in \mathrm{Lat}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({Z}\in {B}\wedge {W}\in {B}\right)\right)\to {Z}\in {B}$
8 1 2 3 latmlem1
9 4 5 6 7 8 syl13anc
10 simp3r ${⊢}\left({K}\in \mathrm{Lat}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({Z}\in {B}\wedge {W}\in {B}\right)\right)\to {W}\in {B}$
11 1 2 3 latmlem2
12 4 7 10 6 11 syl13anc
13 1 3 latmcl
14 4 5 7 13 syl3anc
15 1 3 latmcl
16 4 6 7 15 syl3anc
17 1 3 latmcl
18 4 6 10 17 syl3anc
19 1 2 lattr
20 4 14 16 18 19 syl13anc
21 9 12 20 syl2and