Theorem safesnsupfiub

Description: If B is a finite subset of ordered class A , we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024)

	Ref	Expression
Hypotheses	safesnsupfiub.small	|- ( ph -> ( O = (/) \/ O = 1o ) )
	safesnsupfiub.finite	|- ( ph -> B e. Fin )
	safesnsupfiub.subset	|- ( ph -> B C_ A )
	safesnsupfiub.ordered	|- ( ph -> R Or A )
	safesnsupfiub.ub	|- ( ph -> A. x e. B A. y e. C x R y )
Assertion	safesnsupfiub	|- ( ph -> A. x e. if ( O ~< B , { sup ( B , A , R ) } , B ) A. y e. C x R y )

Proof

Step	Hyp	Ref	Expression
1		safesnsupfiub.small	|- ( ph -> ( O = (/) \/ O = 1o ) )
2		safesnsupfiub.finite	|- ( ph -> B e. Fin )
3		safesnsupfiub.subset	|- ( ph -> B C_ A )
4		safesnsupfiub.ordered	|- ( ph -> R Or A )
5		safesnsupfiub.ub	|- ( ph -> A. x e. B A. y e. C x R y )
6	1 2 3 4	safesnsupfiss	|- ( ph -> if ( O ~< B , { sup ( B , A , R ) } , B ) C_ B )
7	6	sseld	|- ( ph -> ( x e. if ( O ~< B , { sup ( B , A , R ) } , B ) -> x e. B ) )
8	7	imim1d	|- ( ph -> ( ( x e. B -> A. y e. C x R y ) -> ( x e. if ( O ~< B , { sup ( B , A , R ) } , B ) -> A. y e. C x R y ) ) )
9	8	ralimdv2	|- ( ph -> ( A. x e. B A. y e. C x R y -> A. x e. if ( O ~< B , { sup ( B , A , R ) } , B ) A. y e. C x R y ) )
10	5 9	mpd	|- ( ph -> A. x e. if ( O ~< B , { sup ( B , A , R ) } , B ) A. y e. C x R y )