# Metamath Proof Explorer

## Theorem meetval2

Description: Value of meet for a poset with LUB expanded. (Contributed by NM, 16-Sep-2011) (Revised by NM, 11-Sep-2018)

Ref Expression
Hypotheses meetval2.b
`|- B = ( Base ` K )`
meetval2.l
`|- .<_ = ( le ` K )`
meetval2.m
`|- ./\ = ( meet ` K )`
meetval2.k
`|- ( ph -> K e. V )`
meetval2.x
`|- ( ph -> X e. B )`
meetval2.y
`|- ( ph -> Y e. B )`
Assertion meetval2
`|- ( ph -> ( X ./\ Y ) = ( iota_ x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) )`

### Proof

Step Hyp Ref Expression
1 meetval2.b
` |-  B = ( Base ` K )`
2 meetval2.l
` |-  .<_ = ( le ` K )`
3 meetval2.m
` |-  ./\ = ( meet ` K )`
4 meetval2.k
` |-  ( ph -> K e. V )`
5 meetval2.x
` |-  ( ph -> X e. B )`
6 meetval2.y
` |-  ( ph -> Y e. B )`
7 eqid
` |-  ( glb ` K ) = ( glb ` K )`
8 7 3 4 5 6 meetval
` |-  ( ph -> ( X ./\ Y ) = ( ( glb ` K ) ` { X , Y } ) )`
9 biid
` |-  ( ( A. y e. { X , Y } x .<_ y /\ A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) ) <-> ( A. y e. { X , Y } x .<_ y /\ A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) ) )`
` |-  ( ph -> { X , Y } C_ B )`
` |-  ( ph -> ( ( glb ` K ) ` { X , Y } ) = ( iota_ x e. B ( A. y e. { X , Y } x .<_ y /\ A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) ) ) )`
` |-  ( ( X e. B /\ Y e. B ) -> ( ( A. y e. { X , Y } x .<_ y /\ A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) ) <-> ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) )`
` |-  ( ( X e. B /\ Y e. B ) -> ( iota_ x e. B ( A. y e. { X , Y } x .<_ y /\ A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) ) ) = ( iota_ x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) )`
` |-  ( ph -> ( iota_ x e. B ( A. y e. { X , Y } x .<_ y /\ A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) ) ) = ( iota_ x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) )`
` |-  ( ph -> ( X ./\ Y ) = ( iota_ x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) )`