This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )