This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem latlem

Description: Lemma for lattice properties. (Contributed by NM, 14-Sep-2011)

Ref Expression
Hypotheses latlem.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
latlem.j ⊢ ∨ = ( join ‘ 𝐾 )
latlem.m ⊢ ∧ = ( meet ‘ 𝐾 )
Assertion latlem ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 latlem.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 latlem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 latlem.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 simp1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Lat )
5 simp2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
6 simp3 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
7 opelxpi ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
8 7 3adant1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
9 1 2 3 islat ⊢ ( 𝐾 ∈ Lat ↔ ( 𝐾 ∈ Poset ∧ ( dom ∨ = ( 𝐵 × 𝐵 ) ∧ dom ∧ = ( 𝐵 × 𝐵 ) ) ) )
10 simprl ⊢ ( ( 𝐾 ∈ Poset ∧ ( dom ∨ = ( 𝐵 × 𝐵 ) ∧ dom ∧ = ( 𝐵 × 𝐵 ) ) ) → dom ∨ = ( 𝐵 × 𝐵 ) )
11 9 10 sylbi ⊢ ( 𝐾 ∈ Lat → dom ∨ = ( 𝐵 × 𝐵 ) )
12 11 3ad2ant1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → dom ∨ = ( 𝐵 × 𝐵 ) )
13 8 12 eleqtrrd ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ )
14 1 2 4 5 6 13 joincl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
15 simprr ⊢ ( ( 𝐾 ∈ Poset ∧ ( dom ∨ = ( 𝐵 × 𝐵 ) ∧ dom ∧ = ( 𝐵 × 𝐵 ) ) ) → dom ∧ = ( 𝐵 × 𝐵 ) )
16 9 15 sylbi ⊢ ( 𝐾 ∈ Lat → dom ∧ = ( 𝐵 × 𝐵 ) )
17 16 3ad2ant1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → dom ∧ = ( 𝐵 × 𝐵 ) )
18 8 17 eleqtrrd ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ )
19 1 3 4 5 6 18 meetcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
20 14 19 jca ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ) )