This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ` (/) ) = (/)