Theorem meetdef

Description: Two ways to say that a meet is defined. (Contributed by NM, 9-Sep-2018)

	Ref	Expression
Hypotheses	meetdef.u	|- G = ( glb ` K )
	meetdef.m	|- ./\ = ( meet ` K )
	meetdef.k	|- ( ph -> K e. V )
	meetdef.x	|- ( ph -> X e. W )
	meetdef.y	|- ( ph -> Y e. Z )
Assertion	meetdef	|- ( ph -> ( <. X , Y >. e. dom ./\ <-> { X , Y } e. dom G ) )

Proof

Step	Hyp	Ref	Expression
1		meetdef.u	|- G = ( glb ` K )
2		meetdef.m	|- ./\ = ( meet ` K )
3		meetdef.k	|- ( ph -> K e. V )
4		meetdef.x	|- ( ph -> X e. W )
5		meetdef.y	|- ( ph -> Y e. Z )
6	1 2	meetdm	|- ( K e. V -> dom ./\ = { <. x , y >. | { x , y } e. dom G } )
7	6	eleq2d	|- ( K e. V -> ( <. X , Y >. e. dom ./\ <-> <. X , Y >. e. { <. x , y >. | { x , y } e. dom G } ) )
8	3 7	syl	|- ( ph -> ( <. X , Y >. e. dom ./\ <-> <. X , Y >. e. { <. x , y >. | { x , y } e. dom G } ) )
9		preq1	|- ( x = X -> { x , y } = { X , y } )
10	9	eleq1d	|- ( x = X -> ( { x , y } e. dom G <-> { X , y } e. dom G ) )
11		preq2	|- ( y = Y -> { X , y } = { X , Y } )
12	11	eleq1d	|- ( y = Y -> ( { X , y } e. dom G <-> { X , Y } e. dom G ) )
13	10 12	opelopabg	|- ( ( X e. W /\ Y e. Z ) -> ( <. X , Y >. e. { <. x , y >. | { x , y } e. dom G } <-> { X , Y } e. dom G ) )
14	4 5 13	syl2anc	|- ( ph -> ( <. X , Y >. e. { <. x , y >. | { x , y } e. dom G } <-> { X , Y } e. dom G ) )
15	8 14	bitrd	|- ( ph -> ( <. X , Y >. e. dom ./\ <-> { X , Y } e. dom G ) )