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 
|- ( R Or A -> E* x e. A A. y e. A -. y R x )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( y = x -> ( y R z <-> x R z ) )
2 1 notbid 
 |-  ( y = x -> ( -. y R z <-> -. x R z ) )
3 2 rspcv 
 |-  ( x e. A -> ( A. y e. A -. y R z -> -. x R z ) )
4 breq1 
 |-  ( y = z -> ( y R x <-> z R x ) )
5 4 notbid 
 |-  ( y = z -> ( -. y R x <-> -. z R x ) )
6 5 rspcv 
 |-  ( z e. A -> ( A. y e. A -. y R x -> -. z R x ) )
7 3 6 im2anan9 
 |-  ( ( x e. A /\ z e. A ) -> ( ( A. y e. A -. y R z /\ A. y e. A -. y R x ) -> ( -. x R z /\ -. z R x ) ) )
8 7 ancomsd 
 |-  ( ( x e. A /\ z e. A ) -> ( ( A. y e. A -. y R x /\ A. y e. A -. y R z ) -> ( -. x R z /\ -. z R x ) ) )
9 8 imp 
 |-  ( ( ( x e. A /\ z e. A ) /\ ( A. y e. A -. y R x /\ A. y e. A -. y R z ) ) -> ( -. x R z /\ -. z R x ) )
10 ioran 
 |-  ( -. ( x R z \/ z R x ) <-> ( -. x R z /\ -. z R x ) )
11 solin 
 |-  ( ( R Or A /\ ( x e. A /\ z e. A ) ) -> ( x R z \/ x = z \/ z R x ) )
12 df-3or 
 |-  ( ( x R z \/ x = z \/ z R x ) <-> ( ( x R z \/ x = z ) \/ z R x ) )
13 11 12 sylib 
 |-  ( ( R Or A /\ ( x e. A /\ z e. A ) ) -> ( ( x R z \/ x = z ) \/ z R x ) )
14 or32 
 |-  ( ( ( x R z \/ x = z ) \/ z R x ) <-> ( ( x R z \/ z R x ) \/ x = z ) )
15 13 14 sylib 
 |-  ( ( R Or A /\ ( x e. A /\ z e. A ) ) -> ( ( x R z \/ z R x ) \/ x = z ) )
16 15 ord 
 |-  ( ( R Or A /\ ( x e. A /\ z e. A ) ) -> ( -. ( x R z \/ z R x ) -> x = z ) )
17 10 16 syl5bir 
 |-  ( ( R Or A /\ ( x e. A /\ z e. A ) ) -> ( ( -. x R z /\ -. z R x ) -> x = z ) )
18 9 17 syl5 
 |-  ( ( R Or A /\ ( x e. A /\ z e. A ) ) -> ( ( ( x e. A /\ z e. A ) /\ ( A. y e. A -. y R x /\ A. y e. A -. y R z ) ) -> x = z ) )
19 18 exp4b 
 |-  ( R Or A -> ( ( x e. A /\ z e. A ) -> ( ( x e. A /\ z e. A ) -> ( ( A. y e. A -. y R x /\ A. y e. A -. y R z ) -> x = z ) ) ) )
20 19 pm2.43d 
 |-  ( R Or A -> ( ( x e. A /\ z e. A ) -> ( ( A. y e. A -. y R x /\ A. y e. A -. y R z ) -> x = z ) ) )
21 20 ralrimivv 
 |-  ( R Or A -> A. x e. A A. z e. A ( ( A. y e. A -. y R x /\ A. y e. A -. y R z ) -> x = z ) )
22 breq2 
 |-  ( x = z -> ( y R x <-> y R z ) )
23 22 notbid 
 |-  ( x = z -> ( -. y R x <-> -. y R z ) )
24 23 ralbidv 
 |-  ( x = z -> ( A. y e. A -. y R x <-> A. y e. A -. y R z ) )
25 24 rmo4 
 |-  ( E* x e. A A. y e. A -. y R x <-> A. x e. A A. z e. A ( ( A. y e. A -. y R x /\ A. y e. A -. y R z ) -> x = z ) )
26 21 25 sylibr 
 |-  ( R Or A -> E* x e. A A. y e. A -. y R x )