Metamath Proof Explorer

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