Metamath Proof Explorer


Theorem fimax2g

Description: A finite set has a maximum under a total order. (Contributed by Jeff Madsen, 18-Jun-2010) (Proof shortened by Mario Carneiro, 29-Jan-2014)

Ref Expression
Assertion fimax2g R Or A A Fin A x A y A ¬ x R y

Proof

Step Hyp Ref Expression
1 sopo R Or A R Po A
2 cnvpo R Po A R -1 Po A
3 1 2 sylib R Or A R -1 Po A
4 frfi R -1 Po A A Fin R -1 Fr A
5 3 4 sylan R Or A A Fin R -1 Fr A
6 5 3adant3 R Or A A Fin A R -1 Fr A
7 ssid A A
8 fri A Fin R -1 Fr A A A A x A y A ¬ y R -1 x
9 7 8 mpanr1 A Fin R -1 Fr A A x A y A ¬ y R -1 x
10 9 an32s A Fin A R -1 Fr A x A y A ¬ y R -1 x
11 vex y V
12 vex x V
13 11 12 brcnv y R -1 x x R y
14 13 notbii ¬ y R -1 x ¬ x R y
15 14 ralbii y A ¬ y R -1 x y A ¬ x R y
16 15 rexbii x A y A ¬ y R -1 x x A y A ¬ x R y
17 10 16 sylib A Fin A R -1 Fr A x A y A ¬ x R y
18 17 ex A Fin A R -1 Fr A x A y A ¬ x R y
19 18 3adant1 R Or A A Fin A R -1 Fr A x A y A ¬ x R y
20 6 19 mpd R Or A A Fin A x A y A ¬ x R y