Theorem joindef

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

	Ref	Expression
Hypotheses	joindef.u	|- U = ( lub ` K )
	joindef.j	|- .\/ = ( join ` K )
	joindef.k	|- ( ph -> K e. V )
	joindef.x	|- ( ph -> X e. W )
	joindef.y	|- ( ph -> Y e. Z )
Assertion	joindef	|- ( ph -> ( <. X , Y >. e. dom .\/ <-> { X , Y } e. dom U ) )

Proof

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