Theorem joindm

Description: Domain of join function for a poset-type structure. (Contributed by NM, 16-Sep-2018)

	Ref	Expression
Hypotheses	joinfval.u	|- U = ( lub ` K )
	joinfval.j	|- .\/ = ( join ` K )
Assertion	joindm	|- ( K e. V -> dom .\/ = { <. x , y >. | { x , y } e. dom U } )

Proof

Step	Hyp	Ref	Expression
1		joinfval.u	|- U = ( lub ` K )
2		joinfval.j	|- .\/ = ( join ` K )
3	1 2	joinfval2	|- ( K e. V -> .\/ = { <. <. x , y >. , z >. | ( { x , y } e. dom U /\ z = ( U ` { x , y } ) ) } )
4	3	dmeqd	|- ( K e. V -> dom .\/ = dom { <. <. x , y >. , z >. | ( { x , y } e. dom U /\ z = ( U ` { x , y } ) ) } )
5		dmoprab	|- dom { <. <. x , y >. , z >. | ( { x , y } e. dom U /\ z = ( U ` { x , y } ) ) } = { <. x , y >. | E. z ( { x , y } e. dom U /\ z = ( U ` { x , y } ) ) }
6		fvex	|- ( U ` { x , y } ) e. _V
7	6	isseti	|- E. z z = ( U ` { x , y } )
8		19.42v	|- ( E. z ( { x , y } e. dom U /\ z = ( U ` { x , y } ) ) <-> ( { x , y } e. dom U /\ E. z z = ( U ` { x , y } ) ) )
9	7 8	mpbiran2	|- ( E. z ( { x , y } e. dom U /\ z = ( U ` { x , y } ) ) <-> { x , y } e. dom U )
10	9	opabbii	|- { <. x , y >. | E. z ( { x , y } e. dom U /\ z = ( U ` { x , y } ) ) } = { <. x , y >. | { x , y } e. dom U }
11	5 10	eqtri	|- dom { <. <. x , y >. , z >. | ( { x , y } e. dom U /\ z = ( U ` { x , y } ) ) } = { <. x , y >. | { x , y } e. dom U }
12	4 11	eqtrdi	|- ( K e. V -> dom .\/ = { <. x , y >. | { x , y } e. dom U } )