This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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