Metamath Proof Explorer

Theorem joindm2

Description: The join of any two elements always exists iff all unordered pairs have LUB. (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 )
Assertion joindm2 
|- ( ph -> ( dom .\/ = ( B X. B ) <-> A. x e. B A. y e. B { x , y } e. dom U ) )

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 1 4 2 joindmss 
 |-  ( ph -> dom .\/ C_ ( B X. B ) )
6 eqss 
 |-  ( dom .\/ = ( B X. B ) <-> ( dom .\/ C_ ( B X. B ) /\ ( B X. B ) C_ dom .\/ ) )
7 6 baib 
 |-  ( dom .\/ C_ ( B X. B ) -> ( dom .\/ = ( B X. B ) <-> ( B X. B ) C_ dom .\/ ) )
8 5 7 syl 
 |-  ( ph -> ( dom .\/ = ( B X. B ) <-> ( B X. B ) C_ dom .\/ ) )
9 relxp 
 |-  Rel ( B X. B )
10 ssrel 
 |-  ( Rel ( B X. B ) -> ( ( B X. B ) C_ dom .\/ <-> A. x A. y ( <. x , y >. e. ( B X. B ) -> <. x , y >. e. dom .\/ ) ) )
11 9 10 mp1i 
 |-  ( ph -> ( ( B X. B ) C_ dom .\/ <-> A. x A. y ( <. x , y >. e. ( B X. B ) -> <. x , y >. e. dom .\/ ) ) )
12 opelxp 
 |-  ( <. x , y >. e. ( B X. B ) <-> ( x e. B /\ y e. B ) )
13 12 a1i 
 |-  ( ph -> ( <. x , y >. e. ( B X. B ) <-> ( x e. B /\ y e. B ) ) )
14 vex 
 |-  x e. _V
15 14 a1i 
 |-  ( ph -> x e. _V )
16 vex 
 |-  y e. _V
17 16 a1i 
 |-  ( ph -> y e. _V )
18 3 4 2 15 17 joindef 
 |-  ( ph -> ( <. x , y >. e. dom .\/ <-> { x , y } e. dom U ) )
19 13 18 imbi12d 
 |-  ( ph -> ( ( <. x , y >. e. ( B X. B ) -> <. x , y >. e. dom .\/ ) <-> ( ( x e. B /\ y e. B ) -> { x , y } e. dom U ) ) )
20 19 2albidv 
 |-  ( ph -> ( A. x A. y ( <. x , y >. e. ( B X. B ) -> <. x , y >. e. dom .\/ ) <-> A. x A. y ( ( x e. B /\ y e. B ) -> { x , y } e. dom U ) ) )
21 r2al 
 |-  ( A. x e. B A. y e. B { x , y } e. dom U <-> A. x A. y ( ( x e. B /\ y e. B ) -> { x , y } e. dom U ) )
22 20 21 bitr4di 
 |-  ( ph -> ( A. x A. y ( <. x , y >. e. ( B X. B ) -> <. x , y >. e. dom .\/ ) <-> A. x e. B A. y e. B { x , y } e. dom U ) )
23 8 11 22 3bitrd 
 |-  ( ph -> ( dom .\/ = ( B X. B ) <-> A. x e. B A. y e. B { x , y } e. dom U ) )