Metamath Proof Explorer


Theorem fimaxg

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

Ref Expression
Assertion fimaxg ( ( 𝑅 Or 𝐴𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦𝑦 𝑅 𝑥 ) )

Proof

Step Hyp Ref Expression
1 fimax2g ( ( 𝑅 Or 𝐴𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 𝑅 𝑦 )
2 df-ne ( 𝑥𝑦 ↔ ¬ 𝑥 = 𝑦 )
3 2 imbi1i ( ( 𝑥𝑦𝑦 𝑅 𝑥 ) ↔ ( ¬ 𝑥 = 𝑦𝑦 𝑅 𝑥 ) )
4 pm4.64 ( ( ¬ 𝑥 = 𝑦𝑦 𝑅 𝑥 ) ↔ ( 𝑥 = 𝑦𝑦 𝑅 𝑥 ) )
5 3 4 bitri ( ( 𝑥𝑦𝑦 𝑅 𝑥 ) ↔ ( 𝑥 = 𝑦𝑦 𝑅 𝑥 ) )
6 sotric ( ( 𝑅 Or 𝐴 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝑥 𝑅 𝑦 ↔ ¬ ( 𝑥 = 𝑦𝑦 𝑅 𝑥 ) ) )
7 6 con2bid ( ( 𝑅 Or 𝐴 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( ( 𝑥 = 𝑦𝑦 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑦 ) )
8 5 7 syl5bb ( ( 𝑅 Or 𝐴 ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( ( 𝑥𝑦𝑦 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑦 ) )
9 8 anassrs ( ( ( 𝑅 Or 𝐴𝑥𝐴 ) ∧ 𝑦𝐴 ) → ( ( 𝑥𝑦𝑦 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑦 ) )
10 9 ralbidva ( ( 𝑅 Or 𝐴𝑥𝐴 ) → ( ∀ 𝑦𝐴 ( 𝑥𝑦𝑦 𝑅 𝑥 ) ↔ ∀ 𝑦𝐴 ¬ 𝑥 𝑅 𝑦 ) )
11 10 rexbidva ( 𝑅 Or 𝐴 → ( ∃ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦𝑦 𝑅 𝑥 ) ↔ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 𝑅 𝑦 ) )
12 11 3ad2ant1 ( ( 𝑅 Or 𝐴𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦𝑦 𝑅 𝑥 ) ↔ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 𝑅 𝑦 ) )
13 1 12 mpbird ( ( 𝑅 Or 𝐴𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥𝐴𝑦𝐴 ( 𝑥𝑦𝑦 𝑅 𝑥 ) )