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

Metamath Proof Explorer

Theorem mrelatlubALT

Description: Least upper bounds in a Moore space are realized by the closure of the union. (Contributed by Stefan O'Rear, 31-Jan-2015) (Proof shortened by Zhi Wang, 29-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses mreclatGOOD.i 
|- I = ( toInc ` C )
mrelatlubALT.f 
|- F = ( mrCls ` C )
mrelatlubALT.l 
|- L = ( lub ` I )
Assertion mrelatlubALT 
|- ( ( C e. ( Moore ` X ) /\ U C_ C ) -> ( L ` U ) = ( F ` U. U ) )

Proof

Step Hyp Ref Expression
1 mreclatGOOD.i 
 |-  I = ( toInc ` C )
2 mrelatlubALT.f 
 |-  F = ( mrCls ` C )
3 mrelatlubALT.l 
 |-  L = ( lub ` I )
4 simpl 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> C e. ( Moore ` X ) )
5 simpr 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> U C_ C )
6 3 a1i 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> L = ( lub ` I ) )
7 mreuniss 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> U. U C_ X )
8 2 mrcval 
 |-  ( ( C e. ( Moore ` X ) /\ U. U C_ X ) -> ( F ` U. U ) = |^| { x e. C | U. U C_ x } )
9 7 8 syldan 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> ( F ` U. U ) = |^| { x e. C | U. U C_ x } )
10 2 mrccl 
 |-  ( ( C e. ( Moore ` X ) /\ U. U C_ X ) -> ( F ` U. U ) e. C )
11 7 10 syldan 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> ( F ` U. U ) e. C )
12 1 4 5 6 9 11 ipolub 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> ( L ` U ) = ( F ` U. U ) )