Metamath Proof Explorer

Theorem meetfval

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

Ref Expression
Hypotheses meetfval.u 
|- G = ( glb ` K )
meetfval.m 
|- ./\ = ( meet ` K )
Assertion meetfval 
|- ( K e. V -> ./\ = { <. <. x , y >. , z >. | { x , y } G z } )

Proof

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