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

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

Proof

Step Hyp Ref Expression
1 fimin2g ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 )
2 nesym ⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑦 = 𝑥 )
3 2 imbi1i ⊢ ( ( 𝑥 ≠ 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ( ¬ 𝑦 = 𝑥 → 𝑥 𝑅 𝑦 ) )
4 pm4.64 ⊢ ( ( ¬ 𝑦 = 𝑥 → 𝑥 𝑅 𝑦 ) ↔ ( 𝑦 = 𝑥 ∨ 𝑥 𝑅 𝑦 ) )
5 3 4 bitri ⊢ ( ( 𝑥 ≠ 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ( 𝑦 = 𝑥 ∨ 𝑥 𝑅 𝑦 ) )
6 sotric ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑦 𝑅 𝑥 ↔ ¬ ( 𝑦 = 𝑥 ∨ 𝑥 𝑅 𝑦 ) ) )
7 6 ancom2s ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑦 𝑅 𝑥 ↔ ¬ ( 𝑦 = 𝑥 ∨ 𝑥 𝑅 𝑦 ) ) )
8 7 con2bid ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑦 = 𝑥 ∨ 𝑥 𝑅 𝑦 ) ↔ ¬ 𝑦 𝑅 𝑥 ) )
9 5 8 bitrid ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑥 ≠ 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ¬ 𝑦 𝑅 𝑥 ) )
10 9 anassrs ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ≠ 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ¬ 𝑦 𝑅 𝑥 ) )
11 10 ralbidva ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) )
12 11 rexbidva ⊢ ( 𝑅 Or 𝐴 → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) )
13 12 3ad2ant1 ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) )
14 1 13 mpbird ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → 𝑥 𝑅 𝑦 ) )