Theorem fimax2g

Description: A finite set has a maximum under a total order. (Contributed by Jeff Madsen, 18-Jun-2010) (Proof shortened by Mario Carneiro, 29-Jan-2014)

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

Proof

Step	Hyp	Ref	Expression
1		sopo	⊢ ( 𝑅 Or 𝐴 → 𝑅 Po 𝐴 )
2		cnvpo	⊢ ( 𝑅 Po 𝐴 ↔ ◡ 𝑅 Po 𝐴 )
3	1 2	sylib	⊢ ( 𝑅 Or 𝐴 → ◡ 𝑅 Po 𝐴 )
4		frfi	⊢ ( ( ◡ 𝑅 Po 𝐴 ∧ 𝐴 ∈ Fin ) → ◡ 𝑅 Fr 𝐴 )
5	3 4	sylan	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ◡ 𝑅 Fr 𝐴 )
6	5	3adant3	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ◡ 𝑅 Fr 𝐴 )
7		ssid	⊢ 𝐴 ⊆ 𝐴
8		fri	⊢ ( ( ( 𝐴 ∈ Fin ∧ ◡ 𝑅 Fr 𝐴 ) ∧ ( 𝐴 ⊆ 𝐴 ∧ 𝐴 ≠ ∅ ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ◡ 𝑅 𝑥 )
9	7 8	mpanr1	⊢ ( ( ( 𝐴 ∈ Fin ∧ ◡ 𝑅 Fr 𝐴 ) ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ◡ 𝑅 𝑥 )
10	9	an32s	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ∧ ◡ 𝑅 Fr 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ◡ 𝑅 𝑥 )
11		vex	⊢ 𝑦 ∈ V
12		vex	⊢ 𝑥 ∈ V
13	11 12	brcnv	⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 )
14	13	notbii	⊢ ( ¬ 𝑦 ◡ 𝑅 𝑥 ↔ ¬ 𝑥 𝑅 𝑦 )
15	14	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ◡ 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 )
16	15	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 ◡ 𝑅 𝑥 ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 )
17	10 16	sylib	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) ∧ ◡ 𝑅 Fr 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 )
18	17	ex	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( ◡ 𝑅 Fr 𝐴 → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) )
19	18	3adant1	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( ◡ 𝑅 Fr 𝐴 → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ) )
20	6 19	mpd	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 )