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 ROrAAFinAxAyAxyxRy

Proof

Step Hyp Ref Expression
1 fimin2g ROrAAFinAxAyA¬yRx
2 nesym xy¬y=x
3 2 imbi1i xyxRy¬y=xxRy
4 pm4.64 ¬y=xxRyy=xxRy
5 3 4 bitri xyxRyy=xxRy
6 sotric ROrAyAxAyRx¬y=xxRy
7 6 ancom2s ROrAxAyAyRx¬y=xxRy
8 7 con2bid ROrAxAyAy=xxRy¬yRx
9 5 8 bitrid ROrAxAyAxyxRy¬yRx
10 9 anassrs ROrAxAyAxyxRy¬yRx
11 10 ralbidva ROrAxAyAxyxRyyA¬yRx
12 11 rexbidva ROrAxAyAxyxRyxAyA¬yRx
13 12 3ad2ant1 ROrAAFinAxAyAxyxRyxAyA¬yRx
14 1 13 mpbird ROrAAFinAxAyAxyxRy