Metamath Proof Explorer

Theorem nocvxmin

Description: Given a nonempty convex class of surreals, there is a unique birthday-minimal element of that class. Lemma 0 of Alling p. 185. (Contributed by Scott Fenton, 30-Jun-2011)

Ref Expression
Assertion nocvxmin 
|- ( ( A =/= (/) /\ A C_ No /\ A. x e. A A. y e. A A. z e. No ( ( x  z e. A ) ) -> E! w e. A ( bday ` w ) = |^| ( bday " A ) )

Proof

Step Hyp Ref Expression
1 nobdaymin 
 |-  ( ( A C_ No /\ A =/= (/) ) -> E. w e. A ( bday ` w ) = |^| ( bday " A ) )
2 1 ancoms 
 |-  ( ( A =/= (/) /\ A C_ No ) -> E. w e. A ( bday ` w ) = |^| ( bday " A ) )
3 2 3adant3 
 |-  ( ( A =/= (/) /\ A C_ No /\ A. x e. A A. y e. A A. z e. No ( ( x  z e. A ) ) -> E. w e. A ( bday ` w ) = |^| ( bday " A ) )
4 ssel 
 |-  ( A C_ No -> ( w e. A -> w e. No ) )
5 ssel 
 |-  ( A C_ No -> ( t e. A -> t e. No ) )
6 4 5 anim12d 
 |-  ( A C_ No -> ( ( w e. A /\ t e. A ) -> ( w e. No /\ t e. No ) ) )
7 6 imp 
 |-  ( ( A C_ No /\ ( w e. A /\ t e. A ) ) -> ( w e. No /\ t e. No ) )
8 7 ad2ant2r 
 |-  ( ( ( A C_ No /\ A. x e. A A. y e. A A. z e. No ( ( x  z e. A ) ) /\ ( ( w e. A /\ t e. A ) /\ ( ( bday ` w ) = |^| ( bday " A ) /\ ( bday ` t ) = |^| ( bday " A ) ) ) ) -> ( w e. No /\ t e. No ) )
9 nocvxminlem 
 |-  ( ( A C_ No /\ A. x e. A A. y e. A A. z e. No ( ( x  z e. A ) ) -> ( ( ( w e. A /\ t e. A ) /\ ( ( bday ` w ) = |^| ( bday " A ) /\ ( bday ` t ) = |^| ( bday " A ) ) ) -> -. w
10 9 imp 
 |-  ( ( ( A C_ No /\ A. x e. A A. y e. A A. z e. No ( ( x  z e. A ) ) /\ ( ( w e. A /\ t e. A ) /\ ( ( bday ` w ) = |^| ( bday " A ) /\ ( bday ` t ) = |^| ( bday " A ) ) ) ) -> -. w
11 an2anr 
 |-  ( ( ( w e. A /\ t e. A ) /\ ( ( bday ` w ) = |^| ( bday " A ) /\ ( bday ` t ) = |^| ( bday " A ) ) ) <-> ( ( t e. A /\ w e. A ) /\ ( ( bday ` t ) = |^| ( bday " A ) /\ ( bday ` w ) = |^| ( bday " A ) ) ) )
12 nocvxminlem 
 |-  ( ( A C_ No /\ A. x e. A A. y e. A A. z e. No ( ( x  z e. A ) ) -> ( ( ( t e. A /\ w e. A ) /\ ( ( bday ` t ) = |^| ( bday " A ) /\ ( bday ` w ) = |^| ( bday " A ) ) ) -> -. t
13 11 12 biimtrid 
 |-  ( ( A C_ No /\ A. x e. A A. y e. A A. z e. No ( ( x  z e. A ) ) -> ( ( ( w e. A /\ t e. A ) /\ ( ( bday ` w ) = |^| ( bday " A ) /\ ( bday ` t ) = |^| ( bday " A ) ) ) -> -. t
14 13 imp 
 |-  ( ( ( A C_ No /\ A. x e. A A. y e. A A. z e. No ( ( x  z e. A ) ) /\ ( ( w e. A /\ t e. A ) /\ ( ( bday ` w ) = |^| ( bday " A ) /\ ( bday ` t ) = |^| ( bday " A ) ) ) ) -> -. t
15 slttrieq2 
 |-  ( ( w e. No /\ t e. No ) -> ( w = t <-> ( -. w
16 15 biimpar 
 |-  ( ( ( w e. No /\ t e. No ) /\ ( -. w  w = t )
17 8 10 14 16 syl12anc 
 |-  ( ( ( A C_ No /\ A. x e. A A. y e. A A. z e. No ( ( x  z e. A ) ) /\ ( ( w e. A /\ t e. A ) /\ ( ( bday ` w ) = |^| ( bday " A ) /\ ( bday ` t ) = |^| ( bday " A ) ) ) ) -> w = t )
18 17 exp32 
 |-  ( ( A C_ No /\ A. x e. A A. y e. A A. z e. No ( ( x  z e. A ) ) -> ( ( w e. A /\ t e. A ) -> ( ( ( bday ` w ) = |^| ( bday " A ) /\ ( bday ` t ) = |^| ( bday " A ) ) -> w = t ) ) )
19 18 ralrimivv 
 |-  ( ( A C_ No /\ A. x e. A A. y e. A A. z e. No ( ( x  z e. A ) ) -> A. w e. A A. t e. A ( ( ( bday ` w ) = |^| ( bday " A ) /\ ( bday ` t ) = |^| ( bday " A ) ) -> w = t ) )
20 19 3adant1 
 |-  ( ( A =/= (/) /\ A C_ No /\ A. x e. A A. y e. A A. z e. No ( ( x  z e. A ) ) -> A. w e. A A. t e. A ( ( ( bday ` w ) = |^| ( bday " A ) /\ ( bday ` t ) = |^| ( bday " A ) ) -> w = t ) )
21 fveqeq2 
 |-  ( w = t -> ( ( bday ` w ) = |^| ( bday " A ) <-> ( bday ` t ) = |^| ( bday " A ) ) )
22 21 reu4 
 |-  ( E! w e. A ( bday ` w ) = |^| ( bday " A ) <-> ( E. w e. A ( bday ` w ) = |^| ( bday " A ) /\ A. w e. A A. t e. A ( ( ( bday ` w ) = |^| ( bday " A ) /\ ( bday ` t ) = |^| ( bday " A ) ) -> w = t ) ) )
23 3 20 22 sylanbrc 
 |-  ( ( A =/= (/) /\ A C_ No /\ A. x e. A A. y e. A A. z e. No ( ( x  z e. A ) ) -> E! w e. A ( bday ` w ) = |^| ( bday " A ) )