Theorem fisupclrnmpt

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

	Ref	Expression
Hypotheses	fisupclrnmpt.x	⊢ Ⅎ 𝑥 𝜑
	fisupclrnmpt.r	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
	fisupclrnmpt.b	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	fisupclrnmpt.n	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
	fisupclrnmpt.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ 𝐴 )
Assertion	fisupclrnmpt	⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) , 𝐴 , 𝑅 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fisupclrnmpt.x	⊢ Ⅎ 𝑥 𝜑
2		fisupclrnmpt.r	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
3		fisupclrnmpt.b	⊢ ( 𝜑 → 𝐵 ∈ Fin )
4		fisupclrnmpt.n	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
5		fisupclrnmpt.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ 𝐴 )
6		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
7	1 6 5	rnmptssd	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ⊆ 𝐴 )
8	6	rnmptfi	⊢ ( 𝐵 ∈ Fin → ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ Fin )
9	3 8	syl	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ Fin )
10	1 5 6 4	rnmptn0	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ≠ ∅ )
11		fisupcl	⊢ ( ( 𝑅 Or 𝐴 ∧ ( ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ Fin ∧ ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ≠ ∅ ∧ ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ⊆ 𝐴 ) ) → sup ( ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) , 𝐴 , 𝑅 ) ∈ ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )
12	2 9 10 7 11	syl13anc	⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) , 𝐴 , 𝑅 ) ∈ ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) )
13	7 12	sseldd	⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) , 𝐴 , 𝑅 ) ∈ 𝐴 )