Metamath Proof Explorer

Theorem fiming

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

Ref Expression
Assertion fiming ${⊢}\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}}\left({x}\ne {y}\to {x}{R}{y}\right)$

Proof

Step Hyp Ref Expression
1 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}$
2 nesym ${⊢}{x}\ne {y}↔¬{y}={x}$
3 2 imbi1i ${⊢}\left({x}\ne {y}\to {x}{R}{y}\right)↔\left(¬{y}={x}\to {x}{R}{y}\right)$
4 pm4.64 ${⊢}\left(¬{y}={x}\to {x}{R}{y}\right)↔\left({y}={x}\vee {x}{R}{y}\right)$
5 3 4 bitri ${⊢}\left({x}\ne {y}\to {x}{R}{y}\right)↔\left({y}={x}\vee {x}{R}{y}\right)$
6 sotric ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({y}\in {A}\wedge {x}\in {A}\right)\right)\to \left({y}{R}{x}↔¬\left({y}={x}\vee {x}{R}{y}\right)\right)$
7 6 ancom2s ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({y}{R}{x}↔¬\left({y}={x}\vee {x}{R}{y}\right)\right)$
8 7 con2bid ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left(\left({y}={x}\vee {x}{R}{y}\right)↔¬{y}{R}{x}\right)$
9 5 8 syl5bb ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left(\left({x}\ne {y}\to {x}{R}{y}\right)↔¬{y}{R}{x}\right)$
10 9 anassrs ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge {x}\in {A}\right)\wedge {y}\in {A}\right)\to \left(\left({x}\ne {y}\to {x}{R}{y}\right)↔¬{y}{R}{x}\right)$
11 10 ralbidva ${⊢}\left({R}\mathrm{Or}{A}\wedge {x}\in {A}\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\to {x}{R}{y}\right)↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\right)$
12 11 rexbidva ${⊢}{R}\mathrm{Or}{A}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\to {x}{R}{y}\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\right)$
13 12 3ad2ant1 ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\ne {y}\to {x}{R}{y}\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\right)$
14 1 13 mpbird ${⊢}\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}}\left({x}\ne {y}\to {x}{R}{y}\right)$