This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐵 , 𝐴 , 𝑅 ) )