Theorem fimin2g

Description: A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020)

	Ref	Expression
Assertion	fimin2g	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		3simpc	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) )
2		sopo	⊢ ( 𝑅 Or 𝐴 → 𝑅 Po 𝐴 )
3	2	3ad2ant1	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → 𝑅 Po 𝐴 )
4		simp2	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → 𝐴 ∈ Fin )
5		frfi	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝐴 ∈ Fin ) → 𝑅 Fr 𝐴 )
6	3 4 5	syl2anc	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → 𝑅 Fr 𝐴 )
7		ssid	⊢ 𝐴 ⊆ 𝐴
8		fri	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝑅 Fr 𝐴 ) ∧ ( 𝐴 ⊆ 𝐴 ∧ 𝐴 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 )
9	7 8	mpanr1	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝑅 Fr 𝐴 ) ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 )
10	9	an32s	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ∧ 𝑅 Fr 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 )
11	1 6 10	syl2anc	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 )