Theorem fisupclrnmpt

Description: A nonempty finite indexed set contains its supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	fisupclrnmpt.x	|- F/ x ph
	fisupclrnmpt.r	|- ( ph -> R Or A )
	fisupclrnmpt.b	|- ( ph -> B e. Fin )
	fisupclrnmpt.n	|- ( ph -> B =/= (/) )
	fisupclrnmpt.c	|- ( ( ph /\ x e. B ) -> C e. A )
Assertion	fisupclrnmpt	|- ( ph -> sup ( ran ( x e. B |-> C ) , A , R ) e. A )

Proof

Step	Hyp	Ref	Expression
1		fisupclrnmpt.x	|- F/ x ph
2		fisupclrnmpt.r	|- ( ph -> R Or A )
3		fisupclrnmpt.b	|- ( ph -> B e. Fin )
4		fisupclrnmpt.n	|- ( ph -> B =/= (/) )
5		fisupclrnmpt.c	|- ( ( ph /\ x e. B ) -> C e. A )
6		eqid	|- ( x e. B |-> C ) = ( x e. B |-> C )
7	1 6 5	rnmptssd	|- ( ph -> ran ( x e. B |-> C ) C_ A )
8	6	rnmptfi	|- ( B e. Fin -> ran ( x e. B |-> C ) e. Fin )
9	3 8	syl	|- ( ph -> ran ( x e. B |-> C ) e. Fin )
10	1 5 6 4	rnmptn0	|- ( ph -> ran ( x e. B |-> C ) =/= (/) )
11		fisupcl	|- ( ( R Or A /\ ( ran ( x e. B |-> C ) e. Fin /\ ran ( x e. B |-> C ) =/= (/) /\ ran ( x e. B |-> C ) C_ A ) ) -> sup ( ran ( x e. B |-> C ) , A , R ) e. ran ( x e. B |-> C ) )
12	2 9 10 7 11	syl13anc	|- ( ph -> sup ( ran ( x e. B |-> C ) , A , R ) e. ran ( x e. B |-> C ) )
13	7 12	sseldd	|- ( ph -> sup ( ran ( x e. B |-> C ) , A , R ) e. A )