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 ( 𝜑 → ( 𝐶 𝑅 𝑆𝐶 = 𝑆 ) )