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 ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
supgtoreq.2 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
supgtoreq.3 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
supgtoreq.4 ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
supgtoreq.5 ⊢ ( 𝜑 → 𝑆 = sup ( 𝐵 , 𝐴 , 𝑅 ) )
Assertion supgtoreq ( 𝜑 → ( 𝐶 𝑅 𝑆 ∨ 𝐶 = 𝑆 ) )

Proof

Step Hyp Ref Expression
1 supgtoreq.1 ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2 supgtoreq.2 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
3 supgtoreq.3 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
4 supgtoreq.4 ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
5 supgtoreq.5 ⊢ ( 𝜑 → 𝑆 = sup ( 𝐵 , 𝐴 , 𝑅 ) )
6 4 ne0d ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
7 fisup2g ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
8 1 3 6 2 7 syl13anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
9 ssrexv ⊢ ( 𝐵 ⊆ 𝐴 → ( ∃ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) )
10 2 8 9 sylc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
11 1 10 supub ⊢ ( 𝜑 → ( 𝐶 ∈ 𝐵 → ¬ sup ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ) )
12 4 11 mpd ⊢ ( 𝜑 → ¬ sup ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 )
13 5 12 eqnbrtrd ⊢ ( 𝜑 → ¬ 𝑆 𝑅 𝐶 )
14 fisupcl ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴 ) ) → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐵 )
15 1 3 6 2 14 syl13anc ⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐵 )
16 2 15 sseldd ⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐴 )
17 5 16 eqeltrd ⊢ ( 𝜑 → 𝑆 ∈ 𝐴 )
18 2 4 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
19 sotric ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝑆 𝑅 𝐶 ↔ ¬ ( 𝑆 = 𝐶 ∨ 𝐶 𝑅 𝑆 ) ) )
20 1 17 18 19 syl12anc ⊢ ( 𝜑 → ( 𝑆 𝑅 𝐶 ↔ ¬ ( 𝑆 = 𝐶 ∨ 𝐶 𝑅 𝑆 ) ) )
21 orcom ⊢ ( ( 𝑆 = 𝐶 ∨ 𝐶 𝑅 𝑆 ) ↔ ( 𝐶 𝑅 𝑆 ∨ 𝑆 = 𝐶 ) )
22 eqcom ⊢ ( 𝑆 = 𝐶 ↔ 𝐶 = 𝑆 )
23 22 orbi2i ⊢ ( ( 𝐶 𝑅 𝑆 ∨ 𝑆 = 𝐶 ) ↔ ( 𝐶 𝑅 𝑆 ∨ 𝐶 = 𝑆 ) )
24 21 23 bitri ⊢ ( ( 𝑆 = 𝐶 ∨ 𝐶 𝑅 𝑆 ) ↔ ( 𝐶 𝑅 𝑆 ∨ 𝐶 = 𝑆 ) )
25 24 notbii ⊢ ( ¬ ( 𝑆 = 𝐶 ∨ 𝐶 𝑅 𝑆 ) ↔ ¬ ( 𝐶 𝑅 𝑆 ∨ 𝐶 = 𝑆 ) )
26 20 25 bitr2di ⊢ ( 𝜑 → ( ¬ ( 𝐶 𝑅 𝑆 ∨ 𝐶 = 𝑆 ) ↔ 𝑆 𝑅 𝐶 ) )
27 13 26 mtbird ⊢ ( 𝜑 → ¬ ¬ ( 𝐶 𝑅 𝑆 ∨ 𝐶 = 𝑆 ) )
28 27 notnotrd ⊢ ( 𝜑 → ( 𝐶 𝑅 𝑆 ∨ 𝐶 = 𝑆 ) )