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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ) )