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 ⊢ φ → R Or A
fisupclrnmpt.b ⊢ φ → B ∈ Fin
fisupclrnmpt.n ⊢ φ → B ≠ ∅
fisupclrnmpt.c ⊢ φ ∧ x ∈ B → C ∈ A
Assertion fisupclrnmpt ⊢ φ → sup ran ⁡ x ∈ B ⟼ C A R ∈ A

Proof

Step Hyp Ref Expression
1 fisupclrnmpt.x ⊢ Ⅎ x φ
2 fisupclrnmpt.r ⊢ φ → R Or A
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 ⊢ R Or A ∧ ran ⁡ x ∈ B ⟼ C ∈ Fin ∧ ran ⁡ x ∈ B ⟼ C ≠ ∅ ∧ ran ⁡ x ∈ B ⟼ C ⊆ A → sup ran ⁡ x ∈ B ⟼ C A R ∈ ran ⁡ x ∈ B ⟼ C
12 2 9 10 7 11 syl13anc ⊢ φ → sup ran ⁡ x ∈ B ⟼ C A R ∈ ran ⁡ x ∈ B ⟼ C
13 7 12 sseldd ⊢ φ → sup ran ⁡ x ∈ B ⟼ C A R ∈ A