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 ⊢φ→ROrA
supgtoreq.2 ⊢φ→B⊆A
supgtoreq.3 ⊢φ→B∈Fin
supgtoreq.4 ⊢φ→C∈B
supgtoreq.5 ⊢φ→S=supBAR
Assertion supgtoreq ⊢φ→CRS∨C=S

Proof

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