# Metamath Proof Explorer

## Theorem fisupg

Description: Lemma showing existence and closure of supremum of a finite set. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion fisupg ${⊢}\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}}¬{x}{R}{y}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)\right)$

### Proof

Step Hyp Ref Expression
1 fimaxg ${⊢}\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 {y}{R}{x}\right)$
2 sotrieq2 ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({x}={y}↔\left(¬{x}{R}{y}\wedge ¬{y}{R}{x}\right)\right)$
3 2 simprbda ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\wedge {x}={y}\right)\to ¬{x}{R}{y}$
4 3 ex ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({x}={y}\to ¬{x}{R}{y}\right)$
5 4 anassrs ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge {x}\in {A}\right)\wedge {y}\in {A}\right)\to \left({x}={y}\to ¬{x}{R}{y}\right)$
6 5 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 {y}{R}{x}\right)\to ¬{x}{R}{y}\right)\right)$
7 pm2.27 ${⊢}{x}\ne {y}\to \left(\left({x}\ne {y}\to {y}{R}{x}\right)\to {y}{R}{x}\right)$
8 so2nr ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to ¬\left({x}{R}{y}\wedge {y}{R}{x}\right)$
9 pm3.21 ${⊢}{y}{R}{x}\to \left({x}{R}{y}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)$
10 9 con3d ${⊢}{y}{R}{x}\to \left(¬\left({x}{R}{y}\wedge {y}{R}{x}\right)\to ¬{x}{R}{y}\right)$
11 8 10 syl5com ${⊢}\left({R}\mathrm{Or}{A}\wedge \left({x}\in {A}\wedge {y}\in {A}\right)\right)\to \left({y}{R}{x}\to ¬{x}{R}{y}\right)$
12 11 anassrs ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge {x}\in {A}\right)\wedge {y}\in {A}\right)\to \left({y}{R}{x}\to ¬{x}{R}{y}\right)$
13 7 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 {y}{R}{x}\right)\to ¬{x}{R}{y}\right)\right)$
14 6 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 {y}{R}{x}\right)\to ¬{x}{R}{y}\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 {y}{R}{x}\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\right)$
16 breq2 ${⊢}{z}={x}\to \left({y}{R}{z}↔{y}{R}{x}\right)$
17 16 rspcev ${⊢}\left({x}\in {A}\wedge {y}{R}{x}\right)\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{R}{z}$
18 17 ex ${⊢}{x}\in {A}\to \left({y}{R}{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)$
19 18 ralrimivw ${⊢}{x}\in {A}\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)$
20 19 adantl ${⊢}\left({R}\mathrm{Or}{A}\wedge {x}\in {A}\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\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 {y}{R}{x}\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\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 {y}{R}{x}\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\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 {y}{R}{x}\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{R}{y}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\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}}¬{x}{R}{y}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{R}{z}\right)\right)$