This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑥 ≠ 𝑦 → 𝑦 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑦 ) )
9 8 anassrs ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ≠ 𝑦 → 𝑦 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑦 ) )
10 9 ralbidva ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) )
11 10 rexbidva ⊢ ( 𝑅 Or 𝐴 → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑦 𝑅 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) )
12 11 3ad2ant1 ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑦 𝑅 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) )
13 1 12 mpbird ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑦 𝑅 𝑥 ) )