Metamath Proof Explorer

Theorem latjlej12

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

Ref Expression
Hypotheses latlej.b ⊢B=BaseK
latlej.l ⊢≤˙=≤K
latlej.j ⊢∨˙=join⁡K
Assertion latjlej12 ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→X≤˙Y∧Z≤˙W→X∨˙Z≤˙Y∨˙W

Proof

Step Hyp Ref Expression
1 latlej.b ⊢B=BaseK
2 latlej.l ⊢≤˙=≤K
3 latlej.j ⊢∨˙=join⁡K
4 simp1 ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→K∈Lat
5 simp2l ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→X∈B
6 simp2r ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→Y∈B
7 simp3l ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→Z∈B
8 1 2 3 latjlej1 ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B→X≤˙Y→X∨˙Z≤˙Y∨˙Z
9 4 5 6 7 8 syl13anc ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→X≤˙Y→X∨˙Z≤˙Y∨˙Z
10 simp3r ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→W∈B
11 1 2 3 latjlej2 ⊢K∈Lat∧Z∈B∧W∈B∧Y∈B→Z≤˙W→Y∨˙Z≤˙Y∨˙W
12 4 7 10 6 11 syl13anc ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→Z≤˙W→Y∨˙Z≤˙Y∨˙W
13 1 3 latjcl ⊢K∈Lat∧X∈B∧Z∈B→X∨˙Z∈B
14 4 5 7 13 syl3anc ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→X∨˙Z∈B
15 1 3 latjcl ⊢K∈Lat∧Y∈B∧Z∈B→Y∨˙Z∈B
16 4 6 7 15 syl3anc ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→Y∨˙Z∈B
17 1 3 latjcl ⊢K∈Lat∧Y∈B∧W∈B→Y∨˙W∈B
18 4 6 10 17 syl3anc ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→Y∨˙W∈B
19 1 2 lattr ⊢K∈Lat∧X∨˙Z∈B∧Y∨˙Z∈B∧Y∨˙W∈B→X∨˙Z≤˙Y∨˙Z∧Y∨˙Z≤˙Y∨˙W→X∨˙Z≤˙Y∨˙W
20 4 14 16 18 19 syl13anc ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→X∨˙Z≤˙Y∨˙Z∧Y∨˙Z≤˙Y∨˙W→X∨˙Z≤˙Y∨˙W
21 9 12 20 syl2and ⊢K∈Lat∧X∈B∧Y∈B∧Z∈B∧W∈B→X≤˙Y∧Z≤˙W→X∨˙Z≤˙Y∨˙W