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

Metamath Proof Explorer

Theorem lubdm

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

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

Proof

Step Hyp Ref Expression
1 lubfval.b 
 |-  B = ( Base ` K )
2 lubfval.l 
 |-  .<_ = ( le ` K )
3 lubfval.u 
 |-  U = ( lub ` K )
4 lubfval.p 
 |-  ( ps <-> ( A. y e. s y .<_ x /\ A. z e. B ( A. y e. s y .<_ z -> x .<_ z ) ) )
5 lubfval.k 
 |-  ( ph -> K e. V )
6 1 2 3 4 5 lubfval 
 |-  ( ph -> U = ( ( s e. ~P B |-> ( iota_ x e. B ps ) ) |` { s | E! x e. B ps } ) )
7 6 dmeqd 
 |-  ( ph -> dom U = 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 U = { s e. ~P B | E! x e. B ps } )