Metamath Proof Explorer

Theorem meetdm3

Description: The meet of any two elements always exists iff all unordered pairs have GLB (expanded version). (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 )
meetdm3.l 
|- .<_ = ( le ` K )
Assertion meetdm3 
|- ( ph -> ( dom ./\ = ( B X. B ) <-> A. x e. B A. y e. B E! z e. B ( ( z .<_ x /\ z .<_ y ) /\ A. w e. B ( ( w .<_ x /\ w .<_ y ) -> w .<_ z ) ) ) )

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 meetdm3.l 
 |-  .<_ = ( le ` K )
6 1 2 3 4 meetdm2 
 |-  ( ph -> ( dom ./\ = ( B X. B ) <-> A. x e. B A. y e. B { x , y } e. dom G ) )
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 } z .<_ v /\ A. w e. B ( A. v e. { x , y } w .<_ v -> w .<_ z ) ) <-> ( A. v e. { x , y } z .<_ v /\ A. w e. B ( A. v e. { x , y } w .<_ v -> w .<_ z ) ) )
11 1 5 3 10 2 glbeldm 
 |-  ( ph -> ( { x , y } e. dom G <-> ( { x , y } C_ B /\ E! z e. B ( A. v e. { x , y } z .<_ v /\ A. w e. B ( A. v e. { x , y } w .<_ v -> w .<_ z ) ) ) ) )
12 11 baibd 
 |-  ( ( ph /\ { x , y } C_ B ) -> ( { x , y } e. dom G <-> E! z e. B ( A. v e. { x , y } z .<_ v /\ A. w e. B ( A. v e. { x , y } w .<_ v -> w .<_ z ) ) ) )
13 9 12 syldan 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( { x , y } e. dom G <-> E! z e. B ( A. v e. { x , y } z .<_ v /\ A. w e. B ( A. v e. { x , y } w .<_ v -> w .<_ z ) ) ) )
14 2 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> K e. V )
15 1 5 4 14 7 8 meetval2lem 
 |-  ( ( x e. B /\ y e. B ) -> ( ( A. v e. { x , y } z .<_ v /\ A. w e. B ( A. v e. { x , y } w .<_ v -> w .<_ z ) ) <-> ( ( z .<_ x /\ z .<_ y ) /\ A. w e. B ( ( w .<_ x /\ w .<_ y ) -> w .<_ z ) ) ) )
16 15 reubidv 
 |-  ( ( x e. B /\ y e. B ) -> ( E! z e. B ( A. v e. { x , y } z .<_ v /\ A. w e. B ( A. v e. { x , y } w .<_ v -> w .<_ z ) ) <-> E! z e. B ( ( z .<_ x /\ z .<_ y ) /\ A. w e. B ( ( w .<_ x /\ w .<_ y ) -> w .<_ z ) ) ) )
17 16 adantl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E! z e. B ( A. v e. { x , y } z .<_ v /\ A. w e. B ( A. v e. { x , y } w .<_ v -> w .<_ z ) ) <-> E! z e. B ( ( z .<_ x /\ z .<_ y ) /\ A. w e. B ( ( w .<_ x /\ w .<_ y ) -> w .<_ z ) ) ) )
18 13 17 bitrd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( { x , y } e. dom G <-> E! z e. B ( ( z .<_ x /\ z .<_ y ) /\ A. w e. B ( ( w .<_ x /\ w .<_ y ) -> w .<_ z ) ) ) )
19 18 2ralbidva 
 |-  ( ph -> ( A. x e. B A. y e. B { x , y } e. dom G <-> A. x e. B A. y e. B E! z e. B ( ( z .<_ x /\ z .<_ y ) /\ A. w e. B ( ( w .<_ x /\ w .<_ y ) -> w .<_ z ) ) ) )
20 6 19 bitrd 
 |-  ( ph -> ( dom ./\ = ( B X. B ) <-> A. x e. B A. y e. B E! z e. B ( ( z .<_ x /\ z .<_ y ) /\ A. w e. B ( ( w .<_ x /\ w .<_ y ) -> w .<_ z ) ) ) )