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

Metamath Proof Explorer

Theorem joinval2lem

Description: Lemma for joinval2 and joineu . (Contributed by NM, 12-Sep-2018) TODO: combine this through joineu into joinlem ?

Ref Expression
Hypotheses joinval2.b 
|- B = ( Base ` K )
joinval2.l 
|- .<_ = ( le ` K )
joinval2.j 
|- .\/ = ( join ` K )
joinval2.k 
|- ( ph -> K e. V )
joinval2.x 
|- ( ph -> X e. B )
joinval2.y 
|- ( ph -> Y e. B )
Assertion joinval2lem 
|- ( ( X e. B /\ Y e. B ) -> ( ( A. y e. { X , Y } y .<_ x /\ A. z e. B ( A. y e. { X , Y } y .<_ z -> x .<_ z ) ) <-> ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) ) )

Proof

Step Hyp Ref Expression
1 joinval2.b 
 |-  B = ( Base ` K )
2 joinval2.l 
 |-  .<_ = ( le ` K )
3 joinval2.j 
 |-  .\/ = ( join ` K )
4 joinval2.k 
 |-  ( ph -> K e. V )
5 joinval2.x 
 |-  ( ph -> X e. B )
6 joinval2.y 
 |-  ( ph -> Y e. B )
7 breq1 
 |-  ( y = X -> ( y .<_ x <-> X .<_ x ) )
8 breq1 
 |-  ( y = Y -> ( y .<_ x <-> Y .<_ x ) )
9 7 8 ralprg 
 |-  ( ( X e. B /\ Y e. B ) -> ( A. y e. { X , Y } y .<_ x <-> ( X .<_ x /\ Y .<_ x ) ) )
10 breq1 
 |-  ( y = X -> ( y .<_ z <-> X .<_ z ) )
11 breq1 
 |-  ( y = Y -> ( y .<_ z <-> Y .<_ z ) )
12 10 11 ralprg 
 |-  ( ( X e. B /\ Y e. B ) -> ( A. y e. { X , Y } y .<_ z <-> ( X .<_ z /\ Y .<_ z ) ) )
13 12 imbi1d 
 |-  ( ( X e. B /\ Y e. B ) -> ( ( A. y e. { X , Y } y .<_ z -> x .<_ z ) <-> ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) )
14 13 ralbidv 
 |-  ( ( X e. B /\ Y e. B ) -> ( A. z e. B ( A. y e. { X , Y } y .<_ z -> x .<_ z ) <-> A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) )
15 9 14 anbi12d 
 |-  ( ( X e. B /\ Y e. B ) -> ( ( A. y e. { X , Y } y .<_ x /\ A. z e. B ( A. y e. { X , Y } y .<_ z -> x .<_ z ) ) <-> ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) ) )