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 ⊢Ⅎxφ
fisupclrnmpt.r ⊢φ→ROrA
fisupclrnmpt.b ⊢φ→B∈Fin
fisupclrnmpt.n ⊢φ→B≠∅
fisupclrnmpt.c ⊢φ∧x∈B→C∈A
Assertion fisupclrnmpt ⊢φ→supran⁡x∈B⟼CAR∈A

Proof

Step Hyp Ref Expression
1 fisupclrnmpt.x ⊢Ⅎxφ
2 fisupclrnmpt.r ⊢φ→ROrA
3 fisupclrnmpt.b ⊢φ→B∈Fin
4 fisupclrnmpt.n ⊢φ→B≠∅
5 fisupclrnmpt.c ⊢φ∧x∈B→C∈A
6 eqid ⊢x∈B⟼C=x∈B⟼C
7 1 6 5 rnmptssd ⊢φ→ran⁡x∈B⟼C⊆A
8 6 rnmptfi ⊢B∈Fin→ran⁡x∈B⟼C∈Fin
9 3 8 syl ⊢φ→ran⁡x∈B⟼C∈Fin
10 1 5 6 4 rnmptn0 ⊢φ→ran⁡x∈B⟼C≠∅
11 fisupcl ⊢ROrA∧ran⁡x∈B⟼C∈Fin∧ran⁡x∈B⟼C≠∅∧ran⁡x∈B⟼C⊆A→supran⁡x∈B⟼CAR∈ran⁡x∈B⟼C
12 2 9 10 7 11 syl13anc ⊢φ→supran⁡x∈B⟼CAR∈ran⁡x∈B⟼C
13 7 12 sseldd ⊢φ→supran⁡x∈B⟼CAR∈A