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

Metamath Proof Explorer

Theorem lublecl

Description: The set of all elements less than a given element has an LUB. (Contributed by NM, 8-Sep-2018)

Ref Expression
Hypotheses lublecl.b 
|- B = ( Base ` K )
lublecl.l 
|- .<_ = ( le ` K )
lublecl.u 
|- U = ( lub ` K )
lublecl.k 
|- ( ph -> K e. Poset )
lublecl.x 
|- ( ph -> X e. B )
Assertion lublecl 
|- ( ph -> { y e. B | y .<_ X } e. dom U )

Proof

Step Hyp Ref Expression
1 lublecl.b 
 |-  B = ( Base ` K )
2 lublecl.l 
 |-  .<_ = ( le ` K )
3 lublecl.u 
 |-  U = ( lub ` K )
4 lublecl.k 
 |-  ( ph -> K e. Poset )
5 lublecl.x 
 |-  ( ph -> X e. B )
6 ssrab2 
 |-  { y e. B | y .<_ X } C_ B
7 6 a1i 
 |-  ( ph -> { y e. B | y .<_ X } C_ B )
8 1 2 3 4 5 lublecllem 
 |-  ( ( ph /\ x e. B ) -> ( ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) <-> x = X ) )
9 8 ralrimiva 
 |-  ( ph -> A. x e. B ( ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) <-> x = X ) )
10 reu6i 
 |-  ( ( X e. B /\ A. x e. B ( ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) <-> x = X ) ) -> E! x e. B ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) )
11 5 9 10 syl2anc 
 |-  ( ph -> E! x e. B ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) )
12 biid 
 |-  ( ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) <-> ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) )
13 1 2 3 12 4 lubeldm 
 |-  ( ph -> ( { y e. B | y .<_ X } e. dom U <-> ( { y e. B | y .<_ X } C_ B /\ E! x e. B ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) ) ) )
14 7 11 13 mpbir2and 
 |-  ( ph -> { y e. B | y .<_ X } e. dom U )