Theorem joinfval2

Description: Value of join function for a poset-type structure. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018)

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

Proof

Step	Hyp	Ref	Expression
1		joinfval.u	|- U = ( lub ` K )
2		joinfval.j	|- .\/ = ( join ` K )
3	1 2	joinfval	|- ( K e. V -> .\/ = { <. <. x , y >. , z >. | { x , y } U z } )
4	1	lubfun	|- Fun U
5		funbrfv2b	|- ( Fun U -> ( { x , y } U z <-> ( { x , y } e. dom U /\ ( U ` { x , y } ) = z ) ) )
6	4 5	ax-mp	|- ( { x , y } U z <-> ( { x , y } e. dom U /\ ( U ` { x , y } ) = z ) )
7		eqcom	|- ( ( U ` { x , y } ) = z <-> z = ( U ` { x , y } ) )
8	7	anbi2i	|- ( ( { x , y } e. dom U /\ ( U ` { x , y } ) = z ) <-> ( { x , y } e. dom U /\ z = ( U ` { x , y } ) ) )
9	6 8	bitri	|- ( { x , y } U z <-> ( { x , y } e. dom U /\ z = ( U ` { x , y } ) ) )
10	9	oprabbii	|- { <. <. x , y >. , z >. | { x , y } U z } = { <. <. x , y >. , z >. | ( { x , y } e. dom U /\ z = ( U ` { x , y } ) ) }
11	3 10	eqtrdi	|- ( K e. V -> .\/ = { <. <. x , y >. , z >. | ( { x , y } e. dom U /\ z = ( U ` { x , y } ) ) } )