Metamath Proof Explorer

Theorem joindm3

Description: The join of any two elements always exists iff all unordered pairs have LUB (expanded version). (Contributed by Zhi Wang, 25-Sep-2024)

Ref Expression
Hypotheses joindm2.b 
|- B = ( Base ` K )
joindm2.k 
|- ( ph -> K e. V )
joindm2.u 
|- U = ( lub ` K )
joindm2.j 
|- .\/ = ( join ` K )
joindm3.l 
|- .<_ = ( le ` K )
Assertion joindm3 
|- ( ph -> ( dom .\/ = ( B X. B ) <-> A. x e. B A. y e. B E! z e. B ( ( x .<_ z /\ y .<_ z ) /\ A. w e. B ( ( x .<_ w /\ y .<_ w ) -> z .<_ w ) ) ) )

Proof

Step Hyp Ref Expression
1 joindm2.b 
 |-  B = ( Base ` K )
2 joindm2.k 
 |-  ( ph -> K e. V )
3 joindm2.u 
 |-  U = ( lub ` K )
4 joindm2.j 
 |-  .\/ = ( join ` K )
5 joindm3.l 
 |-  .<_ = ( le ` K )
6 1 2 3 4 joindm2 
 |-  ( ph -> ( dom .\/ = ( B X. B ) <-> A. x e. B A. y e. B { x , y } e. dom U ) )
7 simprl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B )
8 simprr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B )
9 7 8 prssd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> { x , y } C_ B )
10 biid 
 |-  ( ( A. v e. { x , y } v .<_ z /\ A. w e. B ( A. v e. { x , y } v .<_ w -> z .<_ w ) ) <-> ( A. v e. { x , y } v .<_ z /\ A. w e. B ( A. v e. { x , y } v .<_ w -> z .<_ w ) ) )
11 1 5 3 10 2 lubeldm 
 |-  ( ph -> ( { x , y } e. dom U <-> ( { x , y } C_ B /\ E! z e. B ( A. v e. { x , y } v .<_ z /\ A. w e. B ( A. v e. { x , y } v .<_ w -> z .<_ w ) ) ) ) )
12 11 baibd 
 |-  ( ( ph /\ { x , y } C_ B ) -> ( { x , y } e. dom U <-> E! z e. B ( A. v e. { x , y } v .<_ z /\ A. w e. B ( A. v e. { x , y } v .<_ w -> z .<_ w ) ) ) )
13 9 12 syldan 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( { x , y } e. dom U <-> E! z e. B ( A. v e. { x , y } v .<_ z /\ A. w e. B ( A. v e. { x , y } v .<_ w -> z .<_ w ) ) ) )
14 2 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> K e. V )
15 1 5 4 14 7 8 joinval2lem 
 |-  ( ( x e. B /\ y e. B ) -> ( ( A. v e. { x , y } v .<_ z /\ A. w e. B ( A. v e. { x , y } v .<_ w -> z .<_ w ) ) <-> ( ( x .<_ z /\ y .<_ z ) /\ A. w e. B ( ( x .<_ w /\ y .<_ w ) -> z .<_ w ) ) ) )
16 15 reubidv 
 |-  ( ( x e. B /\ y e. B ) -> ( E! z e. B ( A. v e. { x , y } v .<_ z /\ A. w e. B ( A. v e. { x , y } v .<_ w -> z .<_ w ) ) <-> E! z e. B ( ( x .<_ z /\ y .<_ z ) /\ A. w e. B ( ( x .<_ w /\ y .<_ w ) -> z .<_ w ) ) ) )
17 16 adantl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E! z e. B ( A. v e. { x , y } v .<_ z /\ A. w e. B ( A. v e. { x , y } v .<_ w -> z .<_ w ) ) <-> E! z e. B ( ( x .<_ z /\ y .<_ z ) /\ A. w e. B ( ( x .<_ w /\ y .<_ w ) -> z .<_ w ) ) ) )
18 13 17 bitrd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( { x , y } e. dom U <-> E! z e. B ( ( x .<_ z /\ y .<_ z ) /\ A. w e. B ( ( x .<_ w /\ y .<_ w ) -> z .<_ w ) ) ) )
19 18 2ralbidva 
 |-  ( ph -> ( A. x e. B A. y e. B { x , y } e. dom U <-> A. x e. B A. y e. B E! z e. B ( ( x .<_ z /\ y .<_ z ) /\ A. w e. B ( ( x .<_ w /\ y .<_ w ) -> z .<_ w ) ) ) )
20 6 19 bitrd 
 |-  ( ph -> ( dom .\/ = ( B X. B ) <-> A. x e. B A. y e. B E! z e. B ( ( x .<_ z /\ y .<_ z ) /\ A. w e. B ( ( x .<_ w /\ y .<_ w ) -> z .<_ w ) ) ) )