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

Metamath Proof Explorer

Theorem meeteu

Description: Uniqueness of meet of elements in the domain. (Contributed by NM, 12-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 )
meetlem.e 
|- ( ph -> <. X , Y >. e. dom ./\ )
Assertion meeteu 
|- ( ph -> E! 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 meetlem.e 
 |-  ( ph -> <. X , Y >. e. dom ./\ )
8 eqid 
 |-  ( glb ` K ) = ( glb ` K )
9 8 3 4 5 6 meetdef 
 |-  ( ph -> ( <. X , Y >. e. dom ./\ <-> { X , Y } e. dom ( glb ` K ) ) )
10 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 ) ) )
11 4 adantr 
 |-  ( ( ph /\ { X , Y } e. dom ( glb ` K ) ) -> K e. V )
12 simpr 
 |-  ( ( ph /\ { X , Y } e. dom ( glb ` K ) ) -> { X , Y } e. dom ( glb ` K ) )
13 1 2 8 10 11 12 glbeu 
 |-  ( ( ph /\ { X , Y } e. dom ( glb ` K ) ) -> E! x e. B ( A. y e. { X , Y } x .<_ y /\ A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) ) )
14 13 ex 
 |-  ( ph -> ( { X , Y } e. dom ( glb ` K ) -> E! x e. B ( A. y e. { X , Y } x .<_ y /\ A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) ) ) )
15 1 2 3 4 5 6 meetval2lem 
 |-  ( ( 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 ) ) ) )
16 5 6 15 syl2anc 
 |-  ( ph -> ( ( 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 ) ) ) )
17 16 reubidv 
 |-  ( ph -> ( E! x e. B ( A. y e. { X , Y } x .<_ y /\ A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) ) <-> E! x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) )
18 14 17 sylibd 
 |-  ( ph -> ( { X , Y } e. dom ( glb ` K ) -> E! x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) )
19 9 18 sylbid 
 |-  ( ph -> ( <. X , Y >. e. dom ./\ -> E! x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) )
20 7 19 mpd 
 |-  ( ph -> E! x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) )