Metamath Proof Explorer


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 )