Metamath Proof Explorer

Theorem meetlem

Description: Lemma for meet properties. (Contributed by NM, 16-Sep-2011) (Revised 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 meetlem 
|- ( ph -> ( ( ( X ./\ Y ) .<_ X /\ ( X ./\ Y ) .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ ( X ./\ Y ) ) ) )

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 1 2 3 4 5 6 7 meeteu 
 |-  ( ph -> E! x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) )
9 riotasbc 
 |-  ( E! x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) -> [. ( iota_ x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) / x ]. ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) )
10 8 9 syl 
 |-  ( ph -> [. ( iota_ x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) / x ]. ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) )
11 1 2 3 4 5 6 meetval2 
 |-  ( ph -> ( X ./\ Y ) = ( iota_ x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) )
12 11 sbceq1d 
 |-  ( ph -> ( [. ( X ./\ Y ) / x ]. ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) <-> [. ( iota_ x e. B ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) / x ]. ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) ) )
13 10 12 mpbird 
 |-  ( ph -> [. ( X ./\ Y ) / x ]. ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) )
14 ovex 
 |-  ( X ./\ Y ) e. _V
15 breq1 
 |-  ( x = ( X ./\ Y ) -> ( x .<_ X <-> ( X ./\ Y ) .<_ X ) )
16 breq1 
 |-  ( x = ( X ./\ Y ) -> ( x .<_ Y <-> ( X ./\ Y ) .<_ Y ) )
17 15 16 anbi12d 
 |-  ( x = ( X ./\ Y ) -> ( ( x .<_ X /\ x .<_ Y ) <-> ( ( X ./\ Y ) .<_ X /\ ( X ./\ Y ) .<_ Y ) ) )
18 breq2 
 |-  ( x = ( X ./\ Y ) -> ( z .<_ x <-> z .<_ ( X ./\ Y ) ) )
19 18 imbi2d 
 |-  ( x = ( X ./\ Y ) -> ( ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) <-> ( ( z .<_ X /\ z .<_ Y ) -> z .<_ ( X ./\ Y ) ) ) )
20 19 ralbidv 
 |-  ( x = ( X ./\ Y ) -> ( A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) <-> A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ ( X ./\ Y ) ) ) )
21 17 20 anbi12d 
 |-  ( x = ( X ./\ Y ) -> ( ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) <-> ( ( ( X ./\ Y ) .<_ X /\ ( X ./\ Y ) .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ ( X ./\ Y ) ) ) ) )
22 14 21 sbcie 
 |-  ( [. ( X ./\ Y ) / x ]. ( ( x .<_ X /\ x .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) <-> ( ( ( X ./\ Y ) .<_ X /\ ( X ./\ Y ) .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ ( X ./\ Y ) ) ) )
23 13 22 sylib 
 |-  ( ph -> ( ( ( X ./\ Y ) .<_ X /\ ( X ./\ Y ) .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ ( X ./\ Y ) ) ) )