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 ( ( 𝑅 Or 𝐴𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 𝑅 𝑦 )

Proof

Step Hyp Ref Expression
1 sopo ( 𝑅 Or 𝐴𝑅 Po 𝐴 )
2 cnvpo ( 𝑅 Po 𝐴 𝑅 Po 𝐴 )
3 1 2 sylib ( 𝑅 Or 𝐴 𝑅 Po 𝐴 )
4 frfi ( ( 𝑅 Po 𝐴𝐴 ∈ Fin ) → 𝑅 Fr 𝐴 )
5 3 4 sylan ( ( 𝑅 Or 𝐴𝐴 ∈ Fin ) → 𝑅 Fr 𝐴 )
6 5 3adant3 ( ( 𝑅 Or 𝐴𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → 𝑅 Fr 𝐴 )
7 ssid 𝐴𝐴
8 fri ( ( ( 𝐴 ∈ Fin ∧ 𝑅 Fr 𝐴 ) ∧ ( 𝐴𝐴𝐴 ≠ ∅ ) ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑦 𝑅 𝑥 )
9 7 8 mpanr1 ( ( ( 𝐴 ∈ Fin ∧ 𝑅 Fr 𝐴 ) ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑦 𝑅 𝑥 )
10 9 an32s ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ∧ 𝑅 Fr 𝐴 ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑦 𝑅 𝑥 )
11 vex 𝑦 ∈ V
12 vex 𝑥 ∈ V
13 11 12 brcnv ( 𝑦 𝑅 𝑥𝑥 𝑅 𝑦 )
14 13 notbii ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑥 𝑅 𝑦 )
15 14 ralbii ( ∀ 𝑦𝐴 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦𝐴 ¬ 𝑥 𝑅 𝑦 )
16 15 rexbii ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑦 𝑅 𝑥 ↔ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 𝑅 𝑦 )
17 10 16 sylib ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ∧ 𝑅 Fr 𝐴 ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 𝑅 𝑦 )
18 17 ex ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( 𝑅 Fr 𝐴 → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 𝑅 𝑦 ) )
19 18 3adant1 ( ( 𝑅 Or 𝐴𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( 𝑅 Fr 𝐴 → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 𝑅 𝑦 ) )
20 6 19 mpd ( ( 𝑅 Or 𝐴𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 𝑅 𝑦 )