Metamath Proof Explorer

Theorem fiinf2g

Description: A finite set satisfies the conditions to have an infimum. (Contributed by AV, 6-Oct-2020)

Ref Expression
Assertion fiinf2g ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → ∃ x ∈ B ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y

Proof

Step Hyp Ref Expression
1 soss ⊢ B ⊆ A → R Or A → R Or B
2 simp1 ⊢ R Or B ∧ B ∈ Fin ∧ B ≠ ∅ → R Or B
3 fiinfg ⊢ R Or B ∧ B ∈ Fin ∧ B ≠ ∅ → ∃ x ∈ B ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ B x R y → ∃ z ∈ B z R y
4 2 3 infeu ⊢ R Or B ∧ B ∈ Fin ∧ B ≠ ∅ → ∃! x ∈ B ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ B x R y → ∃ z ∈ B z R y
5 4 3exp ⊢ R Or B → B ∈ Fin → B ≠ ∅ → ∃! x ∈ B ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ B x R y → ∃ z ∈ B z R y
6 1 5 syl6 ⊢ B ⊆ A → R Or A → B ∈ Fin → B ≠ ∅ → ∃! x ∈ B ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ B x R y → ∃ z ∈ B z R y
7 6 com4l ⊢ R Or A → B ∈ Fin → B ≠ ∅ → B ⊆ A → ∃! x ∈ B ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ B x R y → ∃ z ∈ B z R y
8 7 3imp2 ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → ∃! x ∈ B ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ B x R y → ∃ z ∈ B z R y
9 reurex ⊢ ∃! x ∈ B ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ B x R y → ∃ z ∈ B z R y → ∃ x ∈ B ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ B x R y → ∃ z ∈ B z R y
10 breq1 ⊢ z = x → z R y ↔ x R y
11 10 rspcev ⊢ x ∈ B ∧ x R y → ∃ z ∈ B z R y
12 11 ex ⊢ x ∈ B → x R y → ∃ z ∈ B z R y
13 12 ralrimivw ⊢ x ∈ B → ∀ y ∈ A x R y → ∃ z ∈ B z R y
14 13 a1d ⊢ x ∈ B → ∀ y ∈ B x R y → ∃ z ∈ B z R y → ∀ y ∈ A x R y → ∃ z ∈ B z R y
15 14 anim2d ⊢ x ∈ B → ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ B x R y → ∃ z ∈ B z R y → ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y
16 15 reximia ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ B x R y → ∃ z ∈ B z R y → ∃ x ∈ B ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y
17 8 9 16 3syl ⊢ R Or A ∧ B ∈ Fin ∧ B ≠ ∅ ∧ B ⊆ A → ∃ x ∈ B ∀ y ∈ B ¬ y R x ∧ ∀ y ∈ A x R y → ∃ z ∈ B z R y