# Metamath Proof Explorer

## Theorem meet0

Description: Lemma for odujoin . (Contributed by Stefan O'Rear, 29-Jan-2015) TODO ( df-riota update): This proof increased from 152 bytes to 547 bytes after the df-riota change. Any way to shorten it? join0 also.

Ref Expression
Assertion meet0
`|- ( meet ` (/) ) = (/)`

### Proof

Step Hyp Ref Expression
1 0ex
` |-  (/) e. _V`
2 eqid
` |-  ( glb ` (/) ) = ( glb ` (/) )`
3 eqid
` |-  ( meet ` (/) ) = ( meet ` (/) )`
4 2 3 meetfval
` |-  ( (/) e. _V -> ( meet ` (/) ) = { <. <. x , y >. , z >. | { x , y } ( glb ` (/) ) z } )`
5 1 4 ax-mp
` |-  ( meet ` (/) ) = { <. <. x , y >. , z >. | { x , y } ( glb ` (/) ) z }`
6 df-oprab
` |-  { <. <. x , y >. , z >. | { x , y } ( glb ` (/) ) z } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ { x , y } ( glb ` (/) ) z ) }`
7 br0
` |-  -. { x , y } (/) z`
8 base0
` |-  (/) = ( Base ` (/) )`
9 eqid
` |-  ( le ` (/) ) = ( le ` (/) )`
10 biid
` |-  ( ( A. z e. x y ( le ` (/) ) z /\ A. w e. (/) ( A. z e. x w ( le ` (/) ) z -> w ( le ` (/) ) y ) ) <-> ( A. z e. x y ( le ` (/) ) z /\ A. w e. (/) ( A. z e. x w ( le ` (/) ) z -> w ( le ` (/) ) y ) ) )`
11 id
` |-  ( (/) e. _V -> (/) e. _V )`
12 8 9 2 10 11 glbfval
` |-  ( (/) e. _V -> ( glb ` (/) ) = ( ( x e. ~P (/) |-> ( iota_ y e. (/) ( A. z e. x y ( le ` (/) ) z /\ A. w e. (/) ( A. z e. x w ( le ` (/) ) z -> w ( le ` (/) ) y ) ) ) ) |` { x | E! y e. (/) ( A. z e. x y ( le ` (/) ) z /\ A. w e. (/) ( A. z e. x w ( le ` (/) ) z -> w ( le ` (/) ) y ) ) } ) )`
13 1 12 ax-mp
` |-  ( glb ` (/) ) = ( ( x e. ~P (/) |-> ( iota_ y e. (/) ( A. z e. x y ( le ` (/) ) z /\ A. w e. (/) ( A. z e. x w ( le ` (/) ) z -> w ( le ` (/) ) y ) ) ) ) |` { x | E! y e. (/) ( A. z e. x y ( le ` (/) ) z /\ A. w e. (/) ( A. z e. x w ( le ` (/) ) z -> w ( le ` (/) ) y ) ) } )`
14 reu0
` |-  -. E! y e. (/) ( A. z e. x y ( le ` (/) ) z /\ A. w e. (/) ( A. z e. x w ( le ` (/) ) z -> w ( le ` (/) ) y ) )`
15 14 abf
` |-  { x | E! y e. (/) ( A. z e. x y ( le ` (/) ) z /\ A. w e. (/) ( A. z e. x w ( le ` (/) ) z -> w ( le ` (/) ) y ) ) } = (/)`
16 15 reseq2i
` |-  ( ( x e. ~P (/) |-> ( iota_ y e. (/) ( A. z e. x y ( le ` (/) ) z /\ A. w e. (/) ( A. z e. x w ( le ` (/) ) z -> w ( le ` (/) ) y ) ) ) ) |` { x | E! y e. (/) ( A. z e. x y ( le ` (/) ) z /\ A. w e. (/) ( A. z e. x w ( le ` (/) ) z -> w ( le ` (/) ) y ) ) } ) = ( ( x e. ~P (/) |-> ( iota_ y e. (/) ( A. z e. x y ( le ` (/) ) z /\ A. w e. (/) ( A. z e. x w ( le ` (/) ) z -> w ( le ` (/) ) y ) ) ) ) |` (/) )`
17 res0
` |-  ( ( x e. ~P (/) |-> ( iota_ y e. (/) ( A. z e. x y ( le ` (/) ) z /\ A. w e. (/) ( A. z e. x w ( le ` (/) ) z -> w ( le ` (/) ) y ) ) ) ) |` (/) ) = (/)`
18 16 17 eqtri
` |-  ( ( x e. ~P (/) |-> ( iota_ y e. (/) ( A. z e. x y ( le ` (/) ) z /\ A. w e. (/) ( A. z e. x w ( le ` (/) ) z -> w ( le ` (/) ) y ) ) ) ) |` { x | E! y e. (/) ( A. z e. x y ( le ` (/) ) z /\ A. w e. (/) ( A. z e. x w ( le ` (/) ) z -> w ( le ` (/) ) y ) ) } ) = (/)`
19 13 18 eqtri
` |-  ( glb ` (/) ) = (/)`
20 19 breqi
` |-  ( { x , y } ( glb ` (/) ) z <-> { x , y } (/) z )`
21 7 20 mtbir
` |-  -. { x , y } ( glb ` (/) ) z`
22 21 intnan
` |-  -. ( w = <. <. x , y >. , z >. /\ { x , y } ( glb ` (/) ) z )`
23 22 nex
` |-  -. E. z ( w = <. <. x , y >. , z >. /\ { x , y } ( glb ` (/) ) z )`
24 23 nex
` |-  -. E. y E. z ( w = <. <. x , y >. , z >. /\ { x , y } ( glb ` (/) ) z )`
25 24 nex
` |-  -. E. x E. y E. z ( w = <. <. x , y >. , z >. /\ { x , y } ( glb ` (/) ) z )`
26 25 abf
` |-  { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ { x , y } ( glb ` (/) ) z ) } = (/)`
27 6 26 eqtri
` |-  { <. <. x , y >. , z >. | { x , y } ( glb ` (/) ) z } = (/)`
28 5 27 eqtri
` |-  ( meet ` (/) ) = (/)`