Metamath Proof Explorer

Theorem lubeldm2

Description: Member of the domain of the least upper bound function of a poset. (Contributed by Zhi Wang, 26-Sep-2024)

Ref Expression
Hypotheses lubeldm2.b 
|- B = ( Base ` K )
lubeldm2.l 
|- .<_ = ( le ` K )
lubeldm2.u 
|- U = ( lub ` K )
lubeldm2.p 
|- ( ps <-> ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
lubeldm2.k 
|- ( ph -> K e. Poset )
Assertion lubeldm2 
|- ( ph -> ( S e. dom U <-> ( S C_ B /\ E. x e. B ps ) ) )

Proof

Step Hyp Ref Expression
1 lubeldm2.b 
 |-  B = ( Base ` K )
2 lubeldm2.l 
 |-  .<_ = ( le ` K )
3 lubeldm2.u 
 |-  U = ( lub ` K )
4 lubeldm2.p 
 |-  ( ps <-> ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
5 lubeldm2.k 
 |-  ( ph -> K e. Poset )
6 1 2 3 4 5 lubeldm 
 |-  ( ph -> ( S e. dom U <-> ( S C_ B /\ E! x e. B ps ) ) )
7 6 biimpa 
 |-  ( ( ph /\ S e. dom U ) -> ( S C_ B /\ E! x e. B ps ) )
8 reurex 
 |-  ( E! x e. B ps -> E. x e. B ps )
9 8 anim2i 
 |-  ( ( S C_ B /\ E! x e. B ps ) -> ( S C_ B /\ E. x e. B ps ) )
10 7 9 syl 
 |-  ( ( ph /\ S e. dom U ) -> ( S C_ B /\ E. x e. B ps ) )
11 simpl 
 |-  ( ( ph /\ ( S C_ B /\ E. x e. B ps ) ) -> ph )
12 simprl 
 |-  ( ( ph /\ ( S C_ B /\ E. x e. B ps ) ) -> S C_ B )
13 2 1 poslubmo 
 |-  ( ( K e. Poset /\ S C_ B ) -> E* x e. B ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
14 5 13 sylan 
 |-  ( ( ph /\ S C_ B ) -> E* x e. B ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
15 4 rmobii 
 |-  ( E* x e. B ps <-> E* x e. B ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
16 14 15 sylibr 
 |-  ( ( ph /\ S C_ B ) -> E* x e. B ps )
17 16 anim1ci 
 |-  ( ( ( ph /\ S C_ B ) /\ E. x e. B ps ) -> ( E. x e. B ps /\ E* x e. B ps ) )
18 reu5 
 |-  ( E! x e. B ps <-> ( E. x e. B ps /\ E* x e. B ps ) )
19 17 18 sylibr 
 |-  ( ( ( ph /\ S C_ B ) /\ E. x e. B ps ) -> E! x e. B ps )
20 19 anasss 
 |-  ( ( ph /\ ( S C_ B /\ E. x e. B ps ) ) -> E! x e. B ps )
21 6 biimpar 
 |-  ( ( ph /\ ( S C_ B /\ E! x e. B ps ) ) -> S e. dom U )
22 11 12 20 21 syl12anc 
 |-  ( ( ph /\ ( S C_ B /\ E. x e. B ps ) ) -> S e. dom U )
23 10 22 impbida 
 |-  ( ph -> ( S e. dom U <-> ( S C_ B /\ E. x e. B ps ) ) )