Metamath Proof Explorer


Theorem supssd

Description: Inequality deduction for supremum of a subset. (Contributed by Thierry Arnoux, 21-Mar-2017)

Ref Expression
Hypotheses supssd.0 ( 𝜑𝑅 Or 𝐴 )
supssd.1 ( 𝜑𝐵𝐶 )
supssd.2 ( 𝜑𝐶𝐴 )
supssd.3 ( 𝜑 → ∃ 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) )
supssd.4 ( 𝜑 → ∃ 𝑥𝐴 ( ∀ 𝑦𝐶 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐶 𝑦 𝑅 𝑧 ) ) )
Assertion supssd ( 𝜑 → ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) )

Proof

Step Hyp Ref Expression
1 supssd.0 ( 𝜑𝑅 Or 𝐴 )
2 supssd.1 ( 𝜑𝐵𝐶 )
3 supssd.2 ( 𝜑𝐶𝐴 )
4 supssd.3 ( 𝜑 → ∃ 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) )
5 supssd.4 ( 𝜑 → ∃ 𝑥𝐴 ( ∀ 𝑦𝐶 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐶 𝑦 𝑅 𝑧 ) ) )
6 1 5 supcl ( 𝜑 → sup ( 𝐶 , 𝐴 , 𝑅 ) ∈ 𝐴 )
7 2 sseld ( 𝜑 → ( 𝑧𝐵𝑧𝐶 ) )
8 1 5 supub ( 𝜑 → ( 𝑧𝐶 → ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 𝑧 ) )
9 7 8 syld ( 𝜑 → ( 𝑧𝐵 → ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 𝑧 ) )
10 9 ralrimiv ( 𝜑 → ∀ 𝑧𝐵 ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 𝑧 )
11 1 4 supnub ( 𝜑 → ( ( sup ( 𝐶 , 𝐴 , 𝑅 ) ∈ 𝐴 ∧ ∀ 𝑧𝐵 ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 𝑧 ) → ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
12 6 10 11 mp2and ( 𝜑 → ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) )