Metamath Proof Explorer

Theorem somo

Description: A totally ordered set has at most one minimal element. (Contributed by Mario Carneiro, 24-Jun-2015) (Revised by NM, 16-Jun-2017)

Ref Expression
Assertion somo ( 𝑅 Or 𝐴 → ∃* 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 𝑅 𝑧 ↔ 𝑥 𝑅 𝑧 ) )
2 1 notbid ⊢ ( 𝑦 = 𝑥 → ( ¬ 𝑦 𝑅 𝑧 ↔ ¬ 𝑥 𝑅 𝑧 ) )
3 2 rspcv ⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 → ¬ 𝑥 𝑅 𝑧 ) )
4 breq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 𝑅 𝑥 ↔ 𝑧 𝑅 𝑥 ) )
5 4 notbid ⊢ ( 𝑦 = 𝑧 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑧 𝑅 𝑥 ) )
6 5 rspcv ⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 → ¬ 𝑧 𝑅 𝑥 ) )
7 3 6 im2anan9 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ) → ( ¬ 𝑥 𝑅 𝑧 ∧ ¬ 𝑧 𝑅 𝑥 ) ) )
8 7 ancomsd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 ) → ( ¬ 𝑥 𝑅 𝑧 ∧ ¬ 𝑧 𝑅 𝑥 ) ) )
9 8 imp ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 ) ) → ( ¬ 𝑥 𝑅 𝑧 ∧ ¬ 𝑧 𝑅 𝑥 ) )
10 ioran ⊢ ( ¬ ( 𝑥 𝑅 𝑧 ∨ 𝑧 𝑅 𝑥 ) ↔ ( ¬ 𝑥 𝑅 𝑧 ∧ ¬ 𝑧 𝑅 𝑥 ) )
11 solin ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) )
12 df-3or ⊢ ( ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧 𝑅 𝑥 ) ↔ ( ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ) ∨ 𝑧 𝑅 𝑥 ) )
13 11 12 sylib ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ) ∨ 𝑧 𝑅 𝑥 ) )
14 or32 ⊢ ( ( ( 𝑥 𝑅 𝑧 ∨ 𝑥 = 𝑧 ) ∨ 𝑧 𝑅 𝑥 ) ↔ ( ( 𝑥 𝑅 𝑧 ∨ 𝑧 𝑅 𝑥 ) ∨ 𝑥 = 𝑧 ) )
15 13 14 sylib ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑥 𝑅 𝑧 ∨ 𝑧 𝑅 𝑥 ) ∨ 𝑥 = 𝑧 ) )
16 15 ord ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ¬ ( 𝑥 𝑅 𝑧 ∨ 𝑧 𝑅 𝑥 ) → 𝑥 = 𝑧 ) )
17 10 16 biimtrrid ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ¬ 𝑥 𝑅 𝑧 ∧ ¬ 𝑧 𝑅 𝑥 ) → 𝑥 = 𝑧 ) )
18 9 17 syl5 ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 ) ) → 𝑥 = 𝑧 ) )
19 18 exp4b ⊢ ( 𝑅 Or 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 ) → 𝑥 = 𝑧 ) ) ) )
20 19 pm2.43d ⊢ ( 𝑅 Or 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 ) → 𝑥 = 𝑧 ) ) )
21 20 ralrimivv ⊢ ( 𝑅 Or 𝐴 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 ) → 𝑥 = 𝑧 ) )
22 breq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝑧 ) )
23 22 notbid ⊢ ( 𝑥 = 𝑧 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 𝑧 ) )
24 23 ralbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 ) )
25 24 rmo4 ⊢ ( ∃* 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 ) → 𝑥 = 𝑧 ) )
26 21 25 sylibr ⊢ ( 𝑅 Or 𝐴 → ∃* 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑥 )