Metamath Proof Explorer

Theorem supgtoreq

Description: The supremum of a finite set is greater than or equal to all the elements of the set. (Contributed by AV, 1-Oct-2019)

Ref Expression
Hypotheses supgtoreq.1 ⊢ φ → R Or A
supgtoreq.2 ⊢ φ → B ⊆ A
supgtoreq.3 ⊢ φ → B ∈ Fin
supgtoreq.4 ⊢ φ → C ∈ B
supgtoreq.5 ⊢ φ → S = sup B A R
Assertion supgtoreq ⊢ φ → C R S ∨ C = S

Proof

Step Hyp Ref Expression
1 supgtoreq.1 ⊢ φ → R Or A
2 supgtoreq.2 ⊢ φ → B ⊆ A
3 supgtoreq.3 ⊢ φ → B ∈ Fin
4 supgtoreq.4 ⊢ φ → C ∈ B
5 supgtoreq.5 ⊢ φ → S = sup B A R
6 4 ne0d ⊢ φ → B ≠ ∅
7 fisup2g ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → ∃ x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
8 1 3 6 2 7 syl13anc ⊢ φ → ∃ x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
9 ssrexv ⊢ B ⊆ A → ∃ x ∈ B ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z → ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
10 2 8 9 sylc ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
11 1 10 supub ⊢ φ → C ∈ B → ¬ sup B A R R C
12 4 11 mpd ⊢ φ → ¬ sup B A R R C
13 5 12 eqnbrtrd ⊢ φ → ¬ S R C
14 fisupcl ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → sup B A R ∈ B
15 1 3 6 2 14 syl13anc ⊢ φ → sup B A R ∈ B
16 2 15 sseldd ⊢ φ → sup B A R ∈ A
17 5 16 eqeltrd ⊢ φ → S ∈ A
18 2 4 sseldd ⊢ φ → C ∈ A
19 sotric ⊢ R Or A ∧ S ∈ A ∧ C ∈ A → S R C ↔ ¬ S = C ∨ C R S
20 1 17 18 19 syl12anc ⊢ φ → S R C ↔ ¬ S = C ∨ C R S
21 orcom ⊢ S = C ∨ C R S ↔ C R S ∨ S = C
22 eqcom ⊢ S = C ↔ C = S
23 22 orbi2i ⊢ C R S ∨ S = C ↔ C R S ∨ C = S
24 21 23 bitri ⊢ S = C ∨ C R S ↔ C R S ∨ C = S
25 24 notbii ⊢ ¬ S = C ∨ C R S ↔ ¬ C R S ∨ C = S
26 20 25 bitr2di ⊢ φ → ¬ C R S ∨ C = S ↔ S R C
27 13 26 mtbird ⊢ φ → ¬ ¬ C R S ∨ C = S
28 27 notnotrd ⊢ φ → C R S ∨ C = S