Theorem latcl2

Description: The join and meet of any two elements exist. (Contributed by NM, 14-Sep-2018)

	Ref	Expression
Hypotheses	latcl2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	latcl2.j	⊢ ∨ = ( join ‘ 𝐾 )
	latcl2.m	⊢ ∧ = ( meet ‘ 𝐾 )
	latcl2.k	⊢ ( 𝜑 → 𝐾 ∈ Lat )
	latcl2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	latcl2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	latcl2	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ ∧ ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ ) )

Proof

Step	Hyp	Ref	Expression
1		latcl2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		latcl2.j	⊢ ∨ = ( join ‘ 𝐾 )
3		latcl2.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		latcl2.k	⊢ ( 𝜑 → 𝐾 ∈ Lat )
5		latcl2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		latcl2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7	5 6	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
8	1 2 3	islat	⊢ ( 𝐾 ∈ Lat ↔ ( 𝐾 ∈ Poset ∧ ( dom ∨ = ( 𝐵 × 𝐵 ) ∧ dom ∧ = ( 𝐵 × 𝐵 ) ) ) )
9	4 8	sylib	⊢ ( 𝜑 → ( 𝐾 ∈ Poset ∧ ( dom ∨ = ( 𝐵 × 𝐵 ) ∧ dom ∧ = ( 𝐵 × 𝐵 ) ) ) )
10	9	simprld	⊢ ( 𝜑 → dom ∨ = ( 𝐵 × 𝐵 ) )
11	7 10	eleqtrrd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ )
12	9	simprrd	⊢ ( 𝜑 → dom ∧ = ( 𝐵 × 𝐵 ) )
13	7 12	eleqtrrd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ )
14	11 13	jca	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∨ ∧ ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ ) )