Theorem latcl2

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

	Ref	Expression
Hypotheses	latcl2.b	$$⊢B={\mathrm{Base}}_K$$
	latcl2.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	latcl2.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	latcl2.k	$$⊢\phi \to K\in \mathrm{Lat}$$
	latcl2.x	$$⊢\phi \to X\in B$$
	latcl2.y	$$⊢\phi \to Y\in B$$
Assertion	latcl2	$$⊢\phi \to \left(⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }\wedge ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\wedge }\right)$$

Proof

Step	Hyp	Ref	Expression
1		latcl2.b	$$⊢B={\mathrm{Base}}_K$$
2		latcl2.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		latcl2.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		latcl2.k	$$⊢\phi \to K\in \mathrm{Lat}$$
5		latcl2.x	$$⊢\phi \to X\in B$$
6		latcl2.y	$$⊢\phi \to Y\in B$$
7	5 6	opelxpd	$$⊢\phi \to ⟨X,Y⟩\in \left(B\times B\right)$$
8	1 2 3	islat	$$⊢K\in \mathrm{Lat}\leftrightarrow \left(K\in \mathrm{Poset}\wedge \left(\mathrm{dom}\underset{\dot{}}{\vee }=B\times B\wedge \mathrm{dom}\underset{\dot{}}{\wedge }=B\times B\right)\right)$$
9	4 8	sylib	$$⊢\phi \to \left(K\in \mathrm{Poset}\wedge \left(\mathrm{dom}\underset{\dot{}}{\vee }=B\times B\wedge \mathrm{dom}\underset{\dot{}}{\wedge }=B\times B\right)\right)$$
10	9	simprld	$$⊢\phi \to \mathrm{dom}\underset{\dot{}}{\vee }=B\times B$$
11	7 10	eleqtrrd	$$⊢\phi \to ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }$$
12	9	simprrd	$$⊢\phi \to \mathrm{dom}\underset{\dot{}}{\wedge }=B\times B$$
13	7 12	eleqtrrd	$$⊢\phi \to ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\wedge }$$
14	11 13	jca	$$⊢\phi \to \left(⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }\wedge ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\wedge }\right)$$