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