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 ⊢ Ⅎ 𝑥 𝜑
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 ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) , 𝐴 , 𝑅 ) ∈ 𝐴 )