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 imassrn 
 |-  ( bday " A ) C_ ran bday
2 bdayrn 
 |-  ran bday = On
3 1 2 sseqtri 
 |-  ( bday " A ) C_ On
4 bdaydm 
 |-  dom bday = No
5 4 sseq2i 
 |-  ( A C_ dom bday <-> A C_ No )
6 bdayfun 
 |-  Fun bday
7 funfvima2 
 |-  ( ( Fun bday /\ A C_ dom bday ) -> ( x e. A -> ( bday ` x ) e. ( bday " A ) ) )
8 6 7 mpan 
 |-  ( A C_ dom bday -> ( x e. A -> ( bday ` x ) e. ( bday " A ) ) )
9 5 8 sylbir 
 |-  ( A C_ No -> ( x e. A -> ( bday ` x ) e. ( bday " A ) ) )
10 elex2 
 |-  ( ( bday ` x ) e. ( bday " A ) -> E. w w e. ( bday " A ) )
11 9 10 syl6 
 |-  ( A C_ No -> ( x e. A -> E. w w e. ( bday " A ) ) )
12 11 exlimdv 
 |-  ( A C_ No -> ( E. x x e. A -> E. w w e. ( bday " A ) ) )
13 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
14 n0 
 |-  ( ( bday " A ) =/= (/) <-> E. w w e. ( bday " A ) )
15 12 13 14 3imtr4g 
 |-  ( A C_ No -> ( A =/= (/) -> ( bday " A ) =/= (/) ) )
16 15 impcom 
 |-  ( ( A =/= (/) /\ A C_ No ) -> ( bday " A ) =/= (/) )
17 onint 
 |-  ( ( ( bday " A ) C_ On /\ ( bday " A ) =/= (/) ) -> |^| ( bday " A ) e. ( bday " A ) )
18 3 16 17 sylancr 
 |-  ( ( A =/= (/) /\ A C_ No ) -> |^| ( bday " A ) e. ( bday " A ) )
19 bdayfn 
 |-  bday Fn No
20 fvelimab 
 |-  ( ( bday Fn No /\ A C_ No ) -> ( |^| ( bday " A ) e. ( bday " A ) <-> E. w e. A ( bday ` w ) = |^| ( bday " A ) ) )
21 19 20 mpan 
 |-  ( A C_ No -> ( |^| ( bday " A ) e. ( bday " A ) <-> E. w e. A ( bday ` w ) = |^| ( bday " A ) ) )
22 21 adantl 
 |-  ( ( A =/= (/) /\ A C_ No ) -> ( |^| ( bday " A ) e. ( bday " A ) <-> E. w e. A ( bday ` w ) = |^| ( bday " A ) ) )
23 18 22 mpbid 
 |-  ( ( A =/= (/) /\ A C_ No ) -> E. w e. A ( bday ` w ) = |^| ( bday " A ) )
24 23 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 ) )
25 ssel 
 |-  ( A C_ No -> ( w e. A -> w e. No ) )
26 ssel 
 |-  ( A C_ No -> ( t e. A -> t e. No ) )
27 25 26 anim12d 
 |-  ( A C_ No -> ( ( w e. A /\ t e. A ) -> ( w e. No /\ t e. No ) ) )
28 27 imp 
 |-  ( ( A C_ No /\ ( w e. A /\ t e. A ) ) -> ( w e. No /\ t e. No ) )
29 28 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 ) )
30 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
31 30 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
32 ancom 
 |-  ( ( w e. A /\ t e. A ) <-> ( t e. A /\ w e. A ) )
33 ancom 
 |-  ( ( ( bday ` w ) = |^| ( bday " A ) /\ ( bday ` t ) = |^| ( bday " A ) ) <-> ( ( bday ` t ) = |^| ( bday " A ) /\ ( bday ` w ) = |^| ( bday " A ) ) )
34 32 33 anbi12i 
 |-  ( ( ( 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 ) ) ) )
35 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
36 34 35 syl5bi 
 |-  ( ( 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
37 36 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
38 slttrieq2 
 |-  ( ( w e. No /\ t e. No ) -> ( w = t <-> ( -. w
39 38 biimpar 
 |-  ( ( ( w e. No /\ t e. No ) /\ ( -. w  w = t )
40 29 31 37 39 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 )
41 40 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 ) ) )
42 41 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 ) )
43 42 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 ) )
44 fveqeq2 
 |-  ( w = t -> ( ( bday ` w ) = |^| ( bday " A ) <-> ( bday ` t ) = |^| ( bday " A ) ) )
45 44 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 ) ) )
46 24 43 45 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 ) )