Theorem latcl2

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

	Ref	Expression
Hypotheses	latcl2.b	|- B = ( Base ` K )
	latcl2.j	|- .\/ = ( join ` K )
	latcl2.m	|- ./\ = ( meet ` K )
	latcl2.k	|- ( ph -> K e. Lat )
	latcl2.x	|- ( ph -> X e. B )
	latcl2.y	|- ( ph -> Y e. B )
Assertion	latcl2	|- ( ph -> ( <. X , Y >. e. dom .\/ /\ <. X , Y >. e. dom ./\ ) )

Proof

Step	Hyp	Ref	Expression
1		latcl2.b	|- B = ( Base ` K )
2		latcl2.j	|- .\/ = ( join ` K )
3		latcl2.m	|- ./\ = ( meet ` K )
4		latcl2.k	|- ( ph -> K e. Lat )
5		latcl2.x	|- ( ph -> X e. B )
6		latcl2.y	|- ( ph -> Y e. B )
7	5 6	opelxpd	|- ( ph -> <. X , Y >. e. ( B X. B ) )
8	1 2 3	islat	|- ( K e. Lat <-> ( K e. Poset /\ ( dom .\/ = ( B X. B ) /\ dom ./\ = ( B X. B ) ) ) )
9	4 8	sylib	|- ( ph -> ( K e. Poset /\ ( dom .\/ = ( B X. B ) /\ dom ./\ = ( B X. B ) ) ) )
10	9	simprld	|- ( ph -> dom .\/ = ( B X. B ) )
11	7 10	eleqtrrd	|- ( ph -> <. X , Y >. e. dom .\/ )
12	9	simprrd	|- ( ph -> dom ./\ = ( B X. B ) )
13	7 12	eleqtrrd	|- ( ph -> <. X , Y >. e. dom ./\ )
14	11 13	jca	|- ( ph -> ( <. X , Y >. e. dom .\/ /\ <. X , Y >. e. dom ./\ ) )