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