# 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 ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}$

### Proof

Step Hyp Ref Expression
1 3simpc ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\to \left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)$
2 sopo ${⊢}{R}\mathrm{Or}{A}\to {R}\mathrm{Po}{A}$
3 2 3ad2ant1 ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\to {R}\mathrm{Po}{A}$
4 simp2 ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\to {A}\in \mathrm{Fin}$
5 frfi ${⊢}\left({R}\mathrm{Po}{A}\wedge {A}\in \mathrm{Fin}\right)\to {R}\mathrm{Fr}{A}$
6 3 4 5 syl2anc ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\to {R}\mathrm{Fr}{A}$
7 ssid ${⊢}{A}\subseteq {A}$
8 fri ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {R}\mathrm{Fr}{A}\right)\wedge \left({A}\subseteq {A}\wedge {A}\ne \varnothing \right)\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}$
9 7 8 mpanr1 ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {R}\mathrm{Fr}{A}\right)\wedge {A}\ne \varnothing \right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}$
10 9 an32s ${⊢}\left(\left({A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\wedge {R}\mathrm{Fr}{A}\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}$
11 1 6 10 syl2anc ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}$