Metamath Proof Explorer

Theorem meetdm2

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

Ref Expression
Hypotheses joindm2.b 
|- B = ( Base ` K )
joindm2.k 
|- ( ph -> K e. V )
meetdm2.g 
|- G = ( glb ` K )
meetdm2.m 
|- ./\ = ( meet ` K )
Assertion meetdm2 
|- ( ph -> ( dom ./\ = ( B X. B ) <-> A. x e. B A. y e. B { x , y } e. dom G ) )

Proof

Step Hyp Ref Expression
1 joindm2.b 
 |-  B = ( Base ` K )
2 joindm2.k 
 |-  ( ph -> K e. V )
3 meetdm2.g 
 |-  G = ( glb ` K )
4 meetdm2.m 
 |-  ./\ = ( meet ` K )
5 1 4 2 meetdmss 
 |-  ( 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 meetdef 
 |-  ( ph -> ( <. x , y >. e. dom ./\ <-> { x , y } e. dom G ) )
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 G ) ) )
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 G ) ) )
21 r2al 
 |-  ( A. x e. B A. y e. B { x , y } e. dom G <-> A. x A. y ( ( x e. B /\ y e. B ) -> { x , y } e. dom G ) )
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 G ) )
23 8 11 22 3bitrd 
 |-  ( ph -> ( dom ./\ = ( B X. B ) <-> A. x e. B A. y e. B { x , y } e. dom G ) )