Metamath Proof Explorer

Theorem eqsup

Description: Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015)

Ref Expression
Hypothesis supmo.1 ⊢ φ → R Or A
Assertion eqsup ⊢ φ → C ∈ A ∧ ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z → sup B A R = C

Proof

Step Hyp Ref Expression
1 supmo.1 ⊢ φ → R Or A
2 1 adantr ⊢ φ ∧ C ∈ A ∧ ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z → R Or A
3 2 supval2 ⊢ φ ∧ C ∈ A ∧ ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z → sup B A R = ι x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
4 3simpc ⊢ C ∈ A ∧ ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z → ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z
5 4 adantl ⊢ φ ∧ C ∈ A ∧ ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z → ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z
6 simpr1 ⊢ φ ∧ C ∈ A ∧ ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z → C ∈ A
7 breq1 ⊢ x = C → x R y ↔ C R y
8 7 notbid ⊢ x = C → ¬ x R y ↔ ¬ C R y
9 8 ralbidv ⊢ x = C → ∀ y ∈ B ¬ x R y ↔ ∀ y ∈ B ¬ C R y
10 breq2 ⊢ x = C → y R x ↔ y R C
11 10 imbi1d ⊢ x = C → y R x → ∃ z ∈ B y R z ↔ y R C → ∃ z ∈ B y R z
12 11 ralbidv ⊢ x = C → ∀ y ∈ A y R x → ∃ z ∈ B y R z ↔ ∀ y ∈ A y R C → ∃ z ∈ B y R z
13 9 12 anbi12d ⊢ x = C → ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z ↔ ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z
14 13 rspcev ⊢ C ∈ A ∧ ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z → ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
15 6 5 14 syl2anc ⊢ φ ∧ C ∈ A ∧ ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z → ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
16 2 15 supeu ⊢ φ ∧ C ∈ A ∧ ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z → ∃! x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
17 13 riota2 ⊢ C ∈ A ∧ ∃! x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z → ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z ↔ ι x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z = C
18 6 16 17 syl2anc ⊢ φ ∧ C ∈ A ∧ ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z → ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z ↔ ι x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z = C
19 5 18 mpbid ⊢ φ ∧ C ∈ A ∧ ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z → ι x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z = C
20 3 19 eqtrd ⊢ φ ∧ C ∈ A ∧ ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z → sup B A R = C
21 20 ex ⊢ φ → C ∈ A ∧ ∀ y ∈ B ¬ C R y ∧ ∀ y ∈ A y R C → ∃ z ∈ B y R z → sup B A R = C