This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem glbdm

Description: Domain of the greatest lower bound function of a poset. (Contributed by NM, 6-Sep-2018)

Ref Expression
Hypotheses glbfval.b 
|- B = ( Base ` K )
glbfval.l 
|- .<_ = ( le ` K )
glbfval.g 
|- G = ( glb ` K )
glbfval.p 
|- ( ps <-> ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) )
glbfval.k 
|- ( ph -> K e. V )
Assertion glbdm 
|- ( ph -> dom G = { s e. ~P B | E! x e. B ps } )

Proof

Step Hyp Ref Expression
1 glbfval.b 
 |-  B = ( Base ` K )
2 glbfval.l 
 |-  .<_ = ( le ` K )
3 glbfval.g 
 |-  G = ( glb ` K )
4 glbfval.p 
 |-  ( ps <-> ( A. y e. s x .<_ y /\ A. z e. B ( A. y e. s z .<_ y -> z .<_ x ) ) )
5 glbfval.k 
 |-  ( ph -> K e. V )
6 1 2 3 4 5 glbfval 
 |-  ( ph -> G = ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) )
7 6 dmeqd 
 |-  ( ph -> dom G = dom ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) )
8 riotaex 
 |-  ( iota_ x e. B ps ) e. _V
9 eqid 
 |-  ( s e. ~P B |-> ( iota_ x e. B ps ) ) = ( s e. ~P B |-> ( iota_ x e. B ps ) )
10 8 9 dmmpti 
 |-  dom ( s e. ~P B |-> ( iota_ x e. B ps ) ) = ~P B
11 10 ineq2i 
 |-  ( { s | E! x e. B ps } i^i dom ( s e. ~P B |-> ( iota_ x e. B ps ) ) ) = ( { s | E! x e. B ps } i^i ~P B )
12 dmres 
 |-  dom ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) = ( { s | E! x e. B ps } i^i dom ( s e. ~P B |-> ( iota_ x e. B ps ) ) )
13 dfrab2 
 |-  { s e. ~P B | E! x e. B ps } = ( { s | E! x e. B ps } i^i ~P B )
14 11 12 13 3eqtr4i 
 |-  dom ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) = { s e. ~P B | E! x e. B ps }
15 7 14 eqtrdi 
 |-  ( ph -> dom G = { s e. ~P B | E! x e. B ps } )