Metamath Proof Explorer

Theorem joinfval

Description: Value of join function for a poset. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018) TODO: prove joinfval2 first to reduce net proof size (existence part)?

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

Proof

Step Hyp Ref Expression
1 joinfval.u 
 |-  U = ( lub ` K )
2 joinfval.j 
 |-  .\/ = ( join ` K )
3 elex 
 |-  ( K e. V -> K e. _V )
4 fvex 
 |-  ( Base ` K ) e. _V
5 moeq 
 |-  E* z z = ( U ` { x , y } )
6 5 a1i 
 |-  ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) -> E* z z = ( U ` { x , y } ) )
7 eqid 
 |-  { <. <. x , y >. , z >. | ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z = ( U ` { x , y } ) ) } = { <. <. x , y >. , z >. | ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z = ( U ` { x , y } ) ) }
8 4 4 6 7 oprabex 
 |-  { <. <. x , y >. , z >. | ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z = ( U ` { x , y } ) ) } e. _V
9 8 a1i 
 |-  ( K e. _V -> { <. <. x , y >. , z >. | ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z = ( U ` { x , y } ) ) } e. _V )
10 1 lubfun 
 |-  Fun U
11 funbrfv2b 
 |-  ( Fun U -> ( { x , y } U z <-> ( { x , y } e. dom U /\ ( U ` { x , y } ) = z ) ) )
12 10 11 ax-mp 
 |-  ( { x , y } U z <-> ( { x , y } e. dom U /\ ( U ` { x , y } ) = z ) )
13 eqid 
 |-  ( Base ` K ) = ( Base ` K )
14 eqid 
 |-  ( le ` K ) = ( le ` K )
15 simpl 
 |-  ( ( K e. _V /\ { x , y } e. dom U ) -> K e. _V )
16 simpr 
 |-  ( ( K e. _V /\ { x , y } e. dom U ) -> { x , y } e. dom U )
17 13 14 1 15 16 lubelss 
 |-  ( ( K e. _V /\ { x , y } e. dom U ) -> { x , y } C_ ( Base ` K ) )
18 17 ex 
 |-  ( K e. _V -> ( { x , y } e. dom U -> { x , y } C_ ( Base ` K ) ) )
19 vex 
 |-  x e. _V
20 vex 
 |-  y e. _V
21 19 20 prss 
 |-  ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) <-> { x , y } C_ ( Base ` K ) )
22 18 21 syl6ibr 
 |-  ( K e. _V -> ( { x , y } e. dom U -> ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) )
23 eqcom 
 |-  ( ( U ` { x , y } ) = z <-> z = ( U ` { x , y } ) )
24 23 biimpi 
 |-  ( ( U ` { x , y } ) = z -> z = ( U ` { x , y } ) )
25 22 24 anim12d1 
 |-  ( K e. _V -> ( ( { x , y } e. dom U /\ ( U ` { x , y } ) = z ) -> ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z = ( U ` { x , y } ) ) ) )
26 12 25 syl5bi 
 |-  ( K e. _V -> ( { x , y } U z -> ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z = ( U ` { x , y } ) ) ) )
27 26 alrimiv 
 |-  ( K e. _V -> A. z ( { x , y } U z -> ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z = ( U ` { x , y } ) ) ) )
28 27 alrimiv 
 |-  ( K e. _V -> A. y A. z ( { x , y } U z -> ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z = ( U ` { x , y } ) ) ) )
29 28 alrimiv 
 |-  ( K e. _V -> A. x A. y A. z ( { x , y } U z -> ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z = ( U ` { x , y } ) ) ) )
30 ssoprab2 
 |-  ( A. x A. y A. z ( { x , y } U z -> ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z = ( U ` { x , y } ) ) ) -> { <. <. x , y >. , z >. | { x , y } U z } C_ { <. <. x , y >. , z >. | ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z = ( U ` { x , y } ) ) } )
31 29 30 syl 
 |-  ( K e. _V -> { <. <. x , y >. , z >. | { x , y } U z } C_ { <. <. x , y >. , z >. | ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z = ( U ` { x , y } ) ) } )
32 9 31 ssexd 
 |-  ( K e. _V -> { <. <. x , y >. , z >. | { x , y } U z } e. _V )
33 fveq2 
 |-  ( p = K -> ( lub ` p ) = ( lub ` K ) )
34 33 1 eqtr4di 
 |-  ( p = K -> ( lub ` p ) = U )
35 34 breqd 
 |-  ( p = K -> ( { x , y } ( lub ` p ) z <-> { x , y } U z ) )
36 35 oprabbidv 
 |-  ( p = K -> { <. <. x , y >. , z >. | { x , y } ( lub ` p ) z } = { <. <. x , y >. , z >. | { x , y } U z } )
37 df-join 
 |-  join = ( p e. _V |-> { <. <. x , y >. , z >. | { x , y } ( lub ` p ) z } )
38 36 37 fvmptg 
 |-  ( ( K e. _V /\ { <. <. x , y >. , z >. | { x , y } U z } e. _V ) -> ( join ` K ) = { <. <. x , y >. , z >. | { x , y } U z } )
39 32 38 mpdan 
 |-  ( K e. _V -> ( join ` K ) = { <. <. x , y >. , z >. | { x , y } U z } )
40 2 39 syl5eq 
 |-  ( K e. _V -> .\/ = { <. <. x , y >. , z >. | { x , y } U z } )
41 3 40 syl 
 |-  ( K e. V -> .\/ = { <. <. x , y >. , z >. | { x , y } U z } )