Theorem safesnsupfiss

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	safesnsupfiss.small	|- ( ph -> ( O = (/) \/ O = 1o ) )
	safesnsupfiss.finite	|- ( ph -> B e. Fin )
	safesnsupfiss.subset	|- ( ph -> B C_ A )
	safesnsupfiss.ordered	|- ( ph -> R Or A )
Assertion	safesnsupfiss	|- ( ph -> if ( O ~< B , { sup ( B , A , R ) } , B ) C_ B )

Proof

Step	Hyp	Ref	Expression
1		safesnsupfiss.small	|- ( ph -> ( O = (/) \/ O = 1o ) )
2		safesnsupfiss.finite	|- ( ph -> B e. Fin )
3		safesnsupfiss.subset	|- ( ph -> B C_ A )
4		safesnsupfiss.ordered	|- ( ph -> R Or A )
5		elif	|- ( x e. if ( O ~< B , { sup ( B , A , R ) } , B ) <-> ( ( O ~< B /\ x e. { sup ( B , A , R ) } ) \/ ( -. O ~< B /\ x e. B ) ) )
6		elsni	|- ( x e. { sup ( B , A , R ) } -> x = sup ( B , A , R ) )
7		simpr	|- ( ( ( ph /\ O ~< B ) /\ x = sup ( B , A , R ) ) -> x = sup ( B , A , R ) )
8	4	adantr	|- ( ( ph /\ O ~< B ) -> R Or A )
9	2	adantr	|- ( ( ph /\ O ~< B ) -> B e. Fin )
10		simpr	|- ( ( ph /\ O ~< B ) -> O ~< B )
11		0elon	|- (/) e. On
12		eleq1	|- ( O = (/) -> ( O e. On <-> (/) e. On ) )
13	11 12	mpbiri	|- ( O = (/) -> O e. On )
14		1on	|- 1o e. On
15		eleq1	|- ( O = 1o -> ( O e. On <-> 1o e. On ) )
16	14 15	mpbiri	|- ( O = 1o -> O e. On )
17	13 16	jaoi	|- ( ( O = (/) \/ O = 1o ) -> O e. On )
18	1 17	syl	|- ( ph -> O e. On )
19	18	adantr	|- ( ( ph /\ O ~< B ) -> O e. On )
20	10 19	sdomne0d	|- ( ( ph /\ O ~< B ) -> B =/= (/) )
21	3	adantr	|- ( ( ph /\ O ~< B ) -> B C_ A )
22		fisupcl	|- ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> sup ( B , A , R ) e. B )
23	8 9 20 21 22	syl13anc	|- ( ( ph /\ O ~< B ) -> sup ( B , A , R ) e. B )
24	23	adantr	|- ( ( ( ph /\ O ~< B ) /\ x = sup ( B , A , R ) ) -> sup ( B , A , R ) e. B )
25	7 24	eqeltrd	|- ( ( ( ph /\ O ~< B ) /\ x = sup ( B , A , R ) ) -> x e. B )
26	25	ex	|- ( ( ph /\ O ~< B ) -> ( x = sup ( B , A , R ) -> x e. B ) )
27	6 26	syl5	|- ( ( ph /\ O ~< B ) -> ( x e. { sup ( B , A , R ) } -> x e. B ) )
28	27	expimpd	|- ( ph -> ( ( O ~< B /\ x e. { sup ( B , A , R ) } ) -> x e. B ) )
29		simpr	|- ( ( -. O ~< B /\ x e. B ) -> x e. B )
30	29	a1i	|- ( ph -> ( ( -. O ~< B /\ x e. B ) -> x e. B ) )
31	28 30	jaod	|- ( ph -> ( ( ( O ~< B /\ x e. { sup ( B , A , R ) } ) \/ ( -. O ~< B /\ x e. B ) ) -> x e. B ) )
32	5 31	biimtrid	|- ( ph -> ( x e. if ( O ~< B , { sup ( B , A , R ) } , B ) -> x e. B ) )
33	32	ssrdv	|- ( ph -> if ( O ~< B , { sup ( B , A , R ) } , B ) C_ B )