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 ) )