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

Metamath Proof Explorer

Theorem meetval2lem

Description: Lemma for meetval2 and meeteu . (Contributed by NM, 12-Sep-2018) TODO: combine this through meeteu into meetlem ?

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 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 ) ) ) )

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 breq2 
 |-  ( y = X -> ( x .<_ y <-> x .<_ X ) )
8 breq2 
 |-  ( y = Y -> ( x .<_ y <-> x .<_ Y ) )
9 7 8 ralprg 
 |-  ( ( X e. B /\ Y e. B ) -> ( A. y e. { X , Y } x .<_ y <-> ( x .<_ X /\ x .<_ Y ) ) )
10 breq2 
 |-  ( y = X -> ( z .<_ y <-> z .<_ X ) )
11 breq2 
 |-  ( y = Y -> ( z .<_ y <-> z .<_ Y ) )
12 10 11 ralprg 
 |-  ( ( X e. B /\ Y e. B ) -> ( A. y e. { X , Y } z .<_ y <-> ( z .<_ X /\ z .<_ Y ) ) )
13 12 imbi1d 
 |-  ( ( X e. B /\ Y e. B ) -> ( ( A. y e. { X , Y } z .<_ y -> z .<_ x ) <-> ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) )
14 13 ralbidv 
 |-  ( ( X e. B /\ Y e. B ) -> ( A. z e. B ( A. y e. { X , Y } z .<_ y -> z .<_ x ) <-> A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ x ) ) )
15 9 14 anbi12d 
 |-  ( ( 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 ) ) ) )