Metamath Proof Explorer

Theorem fimin2g

Description: A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020)

Ref Expression
Assertion fimin2g ⊢ R Or A ∧ A ∈ Fin ∧ A ≠ ∅ → ∃ x ∈ A ∀ y ∈ A ¬ y R x

Proof

Step Hyp Ref Expression
1 3simpc ⊢ R Or A ∧ A ∈ Fin ∧ A ≠ ∅ → A ∈ Fin ∧ A ≠ ∅
2 sopo ⊢ R Or A → R Po A
3 2 3ad2ant1 ⊢ R Or A ∧ A ∈ Fin ∧ A ≠ ∅ → R Po A
4 simp2 ⊢ R Or A ∧ A ∈ Fin ∧ A ≠ ∅ → A ∈ Fin
5 frfi ⊢ R Po A ∧ A ∈ Fin → R Fr A
6 3 4 5 syl2anc ⊢ R Or A ∧ A ∈ Fin ∧ A ≠ ∅ → R Fr A
7 ssid ⊢ A ⊆ A
8 fri ⊢ A ∈ Fin ∧ R Fr A ∧ A ⊆ A ∧ A ≠ ∅ → ∃ x ∈ A ∀ y ∈ A ¬ y R x
9 7 8 mpanr1 ⊢ A ∈ Fin ∧ R Fr A ∧ A ≠ ∅ → ∃ x ∈ A ∀ y ∈ A ¬ y R x
10 9 an32s ⊢ A ∈ Fin ∧ A ≠ ∅ ∧ R Fr A → ∃ x ∈ A ∀ y ∈ A ¬ y R x
11 1 6 10 syl2anc ⊢ R Or A ∧ A ∈ Fin ∧ A ≠ ∅ → ∃ x ∈ A ∀ y ∈ A ¬ y R x