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 ⊢ φ → R Or A
supssd.1 ⊢ φ → B ⊆ C
supssd.2 ⊢ φ → C ⊆ A
supssd.3 ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
supssd.4 ⊢ φ → ∃ x ∈ A ∀ y ∈ C ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ C y R z
Assertion supssd ⊢ φ → ¬ sup C A R R sup B A R

Proof

Step Hyp Ref Expression
1 supssd.0 ⊢ φ → R Or A
2 supssd.1 ⊢ φ → B ⊆ C
3 supssd.2 ⊢ φ → C ⊆ A
4 supssd.3 ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
5 supssd.4 ⊢ φ → ∃ x ∈ A ∀ y ∈ C ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ C y R z
6 1 5 supcl ⊢ φ → sup C A R ∈ A
7 2 sseld ⊢ φ → z ∈ B → z ∈ C
8 1 5 supub ⊢ φ → z ∈ C → ¬ sup C A R R z
9 7 8 syld ⊢ φ → z ∈ B → ¬ sup C A R R z
10 9 ralrimiv ⊢ φ → ∀ z ∈ B ¬ sup C A R R z
11 1 4 supnub ⊢ φ → sup C A R ∈ A ∧ ∀ z ∈ B ¬ sup C A R R z → ¬ sup C A R R sup B A R
12 6 10 11 mp2and ⊢ φ → ¬ sup C A R R sup B A R