Metamath Proof Explorer

Theorem joinval2

Description: Value of join for a poset with LUB expanded. (Contributed by NM, 16-Sep-2011) (Revised by NM, 11-Sep-2018)

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 joinval2 
|- ( ph -> ( X .\/ Y ) = ( iota_ x e. B ( ( 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 eqid 
 |-  ( lub ` K ) = ( lub ` K )
8 7 3 4 5 6 joinval 
 |-  ( ph -> ( X .\/ Y ) = ( ( lub ` K ) ` { X , Y } ) )
9 biid 
 |-  ( ( A. y e. { X , Y } y .<_ x /\ A. z e. B ( A. y e. { X , Y } y .<_ z -> x .<_ z ) ) <-> ( A. y e. { X , Y } y .<_ x /\ A. z e. B ( A. y e. { X , Y } y .<_ z -> x .<_ z ) ) )
10 5 6 prssd 
 |-  ( ph -> { X , Y } C_ B )
11 1 2 7 9 4 10 lubval 
 |-  ( ph -> ( ( lub ` K ) ` { X , Y } ) = ( iota_ x e. B ( A. y e. { X , Y } y .<_ x /\ A. z e. B ( A. y e. { X , Y } y .<_ z -> x .<_ z ) ) ) )
12 1 2 3 4 5 6 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 ) ) ) )
13 12 riotabidv 
 |-  ( ( X e. B /\ Y e. B ) -> ( iota_ x e. B ( A. y e. { X , Y } y .<_ x /\ A. z e. B ( A. y e. { X , Y } y .<_ z -> x .<_ z ) ) ) = ( iota_ x e. B ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) ) )
14 5 6 13 syl2anc 
 |-  ( ph -> ( iota_ x e. B ( A. y e. { X , Y } y .<_ x /\ A. z e. B ( A. y e. { X , Y } y .<_ z -> x .<_ z ) ) ) = ( iota_ x e. B ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) ) )
15 8 11 14 3eqtrd 
 |-  ( ph -> ( X .\/ Y ) = ( iota_ x e. B ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) ) )