Metamath Proof Explorer

Theorem joinlem

Description: Lemma for join properties. (Contributed by NM, 16-Sep-2011) (Revised by NM, 12-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 )
joinlem.e 
|- ( ph -> <. X , Y >. e. dom .\/ )
Assertion joinlem 
|- ( ph -> ( ( X .<_ ( X .\/ Y ) /\ Y .<_ ( X .\/ Y ) ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> ( X .\/ Y ) .<_ 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 joinlem.e 
 |-  ( ph -> <. X , Y >. e. dom .\/ )
8 1 2 3 4 5 6 7 joineu 
 |-  ( ph -> E! x e. B ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) )
9 riotasbc 
 |-  ( E! x e. B ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) -> [. ( iota_ x e. B ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) ) / x ]. ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) )
10 8 9 syl 
 |-  ( ph -> [. ( iota_ x e. B ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) ) / x ]. ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) )
11 1 2 3 4 5 6 joinval2 
 |-  ( ph -> ( X .\/ Y ) = ( iota_ x e. B ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) ) )
12 11 sbceq1d 
 |-  ( ph -> ( [. ( X .\/ Y ) / x ]. ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) <-> [. ( iota_ x e. B ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) ) / x ]. ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) ) )
13 10 12 mpbird 
 |-  ( ph -> [. ( X .\/ Y ) / x ]. ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) )
14 ovex 
 |-  ( X .\/ Y ) e. _V
15 breq2 
 |-  ( x = ( X .\/ Y ) -> ( X .<_ x <-> X .<_ ( X .\/ Y ) ) )
16 breq2 
 |-  ( x = ( X .\/ Y ) -> ( Y .<_ x <-> Y .<_ ( X .\/ Y ) ) )
17 15 16 anbi12d 
 |-  ( x = ( X .\/ Y ) -> ( ( X .<_ x /\ Y .<_ x ) <-> ( X .<_ ( X .\/ Y ) /\ Y .<_ ( X .\/ Y ) ) ) )
18 breq1 
 |-  ( x = ( X .\/ Y ) -> ( x .<_ z <-> ( X .\/ Y ) .<_ z ) )
19 18 imbi2d 
 |-  ( x = ( X .\/ Y ) -> ( ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) <-> ( ( X .<_ z /\ Y .<_ z ) -> ( X .\/ Y ) .<_ z ) ) )
20 19 ralbidv 
 |-  ( x = ( X .\/ Y ) -> ( A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) <-> A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> ( X .\/ Y ) .<_ z ) ) )
21 17 20 anbi12d 
 |-  ( x = ( X .\/ Y ) -> ( ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) <-> ( ( X .<_ ( X .\/ Y ) /\ Y .<_ ( X .\/ Y ) ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> ( X .\/ Y ) .<_ z ) ) ) )
22 14 21 sbcie 
 |-  ( [. ( X .\/ Y ) / x ]. ( ( X .<_ x /\ Y .<_ x ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> x .<_ z ) ) <-> ( ( X .<_ ( X .\/ Y ) /\ Y .<_ ( X .\/ Y ) ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> ( X .\/ Y ) .<_ z ) ) )
23 13 22 sylib 
 |-  ( ph -> ( ( X .<_ ( X .\/ Y ) /\ Y .<_ ( X .\/ Y ) ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> ( X .\/ Y ) .<_ z ) ) )