This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) ) } )