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 e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A -. x R y )

Proof

Step Hyp Ref Expression
1 sopo 
 |-  ( R Or A -> R Po A )
2 cnvpo 
 |-  ( R Po A <-> `' R Po A )
3 1 2 sylib 
 |-  ( R Or A -> `' R Po A )
4 frfi 
 |-  ( ( `' R Po A /\ A e. Fin ) -> `' R Fr A )
5 3 4 sylan 
 |-  ( ( R Or A /\ A e. Fin ) -> `' R Fr A )
6 5 3adant3 
 |-  ( ( R Or A /\ A e. Fin /\ A =/= (/) ) -> `' R Fr A )
7 ssid 
 |-  A C_ A
8 fri 
 |-  ( ( ( A e. Fin /\ `' R Fr A ) /\ ( A C_ A /\ A =/= (/) ) ) -> E. x e. A A. y e. A -. y `' R x )
9 7 8 mpanr1 
 |-  ( ( ( A e. Fin /\ `' R Fr A ) /\ A =/= (/) ) -> E. x e. A A. y e. A -. y `' R x )
10 9 an32s 
 |-  ( ( ( A e. Fin /\ A =/= (/) ) /\ `' R Fr A ) -> E. x e. A A. y e. A -. y `' R x )
11 vex 
 |-  y e. _V
12 vex 
 |-  x e. _V
13 11 12 brcnv 
 |-  ( y `' R x <-> x R y )
14 13 notbii 
 |-  ( -. y `' R x <-> -. x R y )
15 14 ralbii 
 |-  ( A. y e. A -. y `' R x <-> A. y e. A -. x R y )
16 15 rexbii 
 |-  ( E. x e. A A. y e. A -. y `' R x <-> E. x e. A A. y e. A -. x R y )
17 10 16 sylib 
 |-  ( ( ( A e. Fin /\ A =/= (/) ) /\ `' R Fr A ) -> E. x e. A A. y e. A -. x R y )
18 17 ex 
 |-  ( ( A e. Fin /\ A =/= (/) ) -> ( `' R Fr A -> E. x e. A A. y e. A -. x R y ) )
19 18 3adant1 
 |-  ( ( R Or A /\ A e. Fin /\ A =/= (/) ) -> ( `' R Fr A -> E. x e. A A. y e. A -. x R y ) )
20 6 19 mpd 
 |-  ( ( R Or A /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A -. x R y )