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