Metamath Proof Explorer

Theorem infeu

Description: An infimum is unique. (Contributed by AV, 6-Oct-2020)

Ref Expression
Hypotheses infmo.1 ⊢ φ → R Or A
infeu.2 ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y
Assertion infeu ⊢ φ → ∃! x ∈ A ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y

Proof

Step Hyp Ref Expression
1 infmo.1 ⊢ φ → R Or A
2 infeu.2 ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y
3 1 infmo ⊢ φ → ∃* x ∈ A ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y
4 reu5 ⊢ ∃! x ∈ A ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y ↔ ∃ x ∈ A ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y ∧ ∃* x ∈ A ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y
5 2 3 4 sylanbrc ⊢ φ → ∃! x ∈ A ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y