# Metamath Proof Explorer

## Theorem fiinfg

Description: Lemma showing existence and closure of infimum of a finite set. (Contributed by AV, 6-Oct-2020)

Ref Expression
Assertion fiinfg ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}{R}{y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 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)$
2 equcom ${⊢}{x}={y}↔{y}={x}$
3 sotrieq2 ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({y}\in {A}\wedge {x}\in {A}\right)\right)\to \left({y}={x}↔\left(¬{y}{R}{x}\wedge ¬{x}{R}{y}\right)\right)$
4 3 ancom2s ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({y}={x}↔\left(¬{y}{R}{x}\wedge ¬{x}{R}{y}\right)\right)$
5 2 4 syl5bb ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({x}={y}↔\left(¬{y}{R}{x}\wedge ¬{x}{R}{y}\right)\right)$
6 5 simprbda ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\wedge {x}={y}\right)\to ¬{y}{R}{x}$
7 6 ex ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({x}={y}\to ¬{y}{R}{x}\right)$
8 7 anassrs ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge {x}\in {A}\right)\wedge {y}\in {A}\right)\to \left({x}={y}\to ¬{y}{R}{x}\right)$
9 8 a1dd ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge {x}\in {A}\right)\wedge {y}\in {A}\right)\to \left({x}={y}\to \left(\left({x}\ne {y}\to {x}{R}{y}\right)\to ¬{y}{R}{x}\right)\right)$
10 pm2.27 ${⊢}{x}\ne {y}\to \left(\left({x}\ne {y}\to {x}{R}{y}\right)\to {x}{R}{y}\right)$
11 soasym ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({x}{R}{y}\to ¬{y}{R}{x}\right)$
12 11 anassrs ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge {x}\in {A}\right)\wedge {y}\in {A}\right)\to \left({x}{R}{y}\to ¬{y}{R}{x}\right)$
13 10 12 syl9r ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge {x}\in {A}\right)\wedge {y}\in {A}\right)\to \left({x}\ne {y}\to \left(\left({x}\ne {y}\to {x}{R}{y}\right)\to ¬{y}{R}{x}\right)\right)$
14 9 13 pm2.61dne ${⊢}\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)\to ¬{y}{R}{x}\right)$
15 14 ralimdva ${⊢}\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)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\right)$
16 breq1 ${⊢}{z}={x}\to \left({z}{R}{y}↔{x}{R}{y}\right)$
17 16 rspcev ${⊢}\left({x}\in {A}\wedge {x}{R}{y}\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}{R}{y}$
18 17 ex ${⊢}{x}\in {A}\to \left({x}{R}{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}{R}{y}\right)$
19 18 ralrimivw ${⊢}{x}\in {A}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}{R}{y}\right)$
20 19 adantl ${⊢}\left({R}\mathrm{Or}{A}\wedge {x}\in {A}\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}{R}{y}\right)$
21 15 20 jctird ${⊢}\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)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}{R}{y}\right)\right)\right)$
22 21 reximdva ${⊢}{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)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}{R}{y}\right)\right)\right)$
23 22 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)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}{R}{y}\right)\right)\right)$
24 1 23 mpd ${⊢}\left({R}\mathrm{Or}{A}\wedge {A}\in \mathrm{Fin}\wedge {A}\ne \varnothing \right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{R}{x}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}{R}{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}{R}{y}\right)\right)$