# Metamath Proof Explorer

## Theorem latm4

Description: Rearrangement of lattice meet of 4 classes. ( in4 analog.) (Contributed by NM, 8-Nov-2011)

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

### Proof

Step Hyp Ref Expression
1 olmass.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 olmass.m
3 simp1 ${⊢}\left({K}\in \mathrm{OL}\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{OL}$
4 simp2r ${⊢}\left({K}\in \mathrm{OL}\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}$
5 simp3l ${⊢}\left({K}\in \mathrm{OL}\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}$
6 simp3r ${⊢}\left({K}\in \mathrm{OL}\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}$
7 1 2 latm12
8 3 4 5 6 7 syl13anc
9 8 oveq2d
10 simp2l ${⊢}\left({K}\in \mathrm{OL}\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}$
11 ollat ${⊢}{K}\in \mathrm{OL}\to {K}\in \mathrm{Lat}$
12 11 3ad2ant1 ${⊢}\left({K}\in \mathrm{OL}\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}$
13 1 2 latmcl
14 12 5 6 13 syl3anc
15 1 2 latmassOLD
16 3 10 4 14 15 syl13anc
17 1 2 latmcl
18 12 4 6 17 syl3anc
19 1 2 latmassOLD
20 3 10 5 18 19 syl13anc
21 9 16 20 3eqtr4d