Metamath Proof Explorer

Theorem nosupbday

Description: Birthday bounding law for surreal supremum. (Contributed by Scott Fenton, 5-Dec-2021)

Ref Expression
Hypothesis nosupbday.1 
|- S = if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
Assertion nosupbday 
|- ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) -> ( bday ` S ) C_ O )

Proof

Step Hyp Ref Expression
1 nosupbday.1 
 |-  S = if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
2 1 nosupno 
 |-  ( ( A C_ No /\ A e. _V ) -> S e. No )
3 2 adantr 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) -> S e. No )
4 bdayval 
 |-  ( S e. No -> ( bday ` S ) = dom S )
5 3 4 syl 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) -> ( bday ` S ) = dom S )
6 iftrue 
 |-  ( E. x e. A A. y e. A -. x  if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) ) = ( ( iota_ x e. A A. y e. A -. x . } ) )
7 1 6 syl5eq 
 |-  ( E. x e. A A. y e. A -. x  S = ( ( iota_ x e. A A. y e. A -. x . } ) )
8 7 dmeqd 
 |-  ( E. x e. A A. y e. A -. x  dom S = dom ( ( iota_ x e. A A. y e. A -. x . } ) )
9 2oex 
 |-  2o e. _V
10 9 dmsnop 
 |-  dom { <. dom ( iota_ x e. A A. y e. A -. x . } = { dom ( iota_ x e. A A. y e. A -. x
11 10 uneq2i 
 |-  ( dom ( iota_ x e. A A. y e. A -. x . } ) = ( dom ( iota_ x e. A A. y e. A -. x
12 dmun 
 |-  dom ( ( iota_ x e. A A. y e. A -. x . } ) = ( dom ( iota_ x e. A A. y e. A -. x . } )
13 df-suc 
 |-  suc dom ( iota_ x e. A A. y e. A -. x
14 11 12 13 3eqtr4i 
 |-  dom ( ( iota_ x e. A A. y e. A -. x . } ) = suc dom ( iota_ x e. A A. y e. A -. x
15 8 14 eqtrdi 
 |-  ( E. x e. A A. y e. A -. x  dom S = suc dom ( iota_ x e. A A. y e. A -. x
16 15 adantr 
 |-  ( ( E. x e. A A. y e. A -. x  dom S = suc dom ( iota_ x e. A A. y e. A -. x
17 simprrl 
 |-  ( ( E. x e. A A. y e. A -. x  O e. On )
18 eloni 
 |-  ( O e. On -> Ord O )
19 17 18 syl 
 |-  ( ( E. x e. A A. y e. A -. x  Ord O )
20 simprll 
 |-  ( ( E. x e. A A. y e. A -. x  A C_ No )
21 simpl 
 |-  ( ( E. x e. A A. y e. A -. x  E. x e. A A. y e. A -. x
22 nomaxmo 
 |-  ( A C_ No -> E* x e. A A. y e. A -. x
23 22 adantr 
 |-  ( ( A C_ No /\ A e. _V ) -> E* x e. A A. y e. A -. x
24 23 adantl 
 |-  ( ( E. x e. A A. y e. A -. x  E* x e. A A. y e. A -. x
25 reu5 
 |-  ( E! x e. A A. y e. A -. x  ( E. x e. A A. y e. A -. x
26 21 24 25 sylanbrc 
 |-  ( ( E. x e. A A. y e. A -. x  E! x e. A A. y e. A -. x
27 26 adantrr 
 |-  ( ( E. x e. A A. y e. A -. x  E! x e. A A. y e. A -. x
28 riotacl 
 |-  ( E! x e. A A. y e. A -. x  ( iota_ x e. A A. y e. A -. x
29 27 28 syl 
 |-  ( ( E. x e. A A. y e. A -. x  ( iota_ x e. A A. y e. A -. x
30 20 29 sseldd 
 |-  ( ( E. x e. A A. y e. A -. x  ( iota_ x e. A A. y e. A -. x
31 bdayval 
 |-  ( ( iota_ x e. A A. y e. A -. x  ( bday ` ( iota_ x e. A A. y e. A -. x
32 30 31 syl 
 |-  ( ( E. x e. A A. y e. A -. x  ( bday ` ( iota_ x e. A A. y e. A -. x
33 simprrr 
 |-  ( ( E. x e. A A. y e. A -. x  ( bday " A ) C_ O )
34 bdayfo 
 |-  bday : No -onto-> On
35 fofn 
 |-  ( bday : No -onto-> On -> bday Fn No )
36 34 35 ax-mp 
 |-  bday Fn No
37 fnfvima 
 |-  ( ( bday Fn No /\ A C_ No /\ ( iota_ x e. A A. y e. A -. x  ( bday ` ( iota_ x e. A A. y e. A -. x
38 36 20 29 37 mp3an2i 
 |-  ( ( E. x e. A A. y e. A -. x  ( bday ` ( iota_ x e. A A. y e. A -. x
39 33 38 sseldd 
 |-  ( ( E. x e. A A. y e. A -. x  ( bday ` ( iota_ x e. A A. y e. A -. x
40 32 39 eqeltrrd 
 |-  ( ( E. x e. A A. y e. A -. x  dom ( iota_ x e. A A. y e. A -. x
41 ordsucss 
 |-  ( Ord O -> ( dom ( iota_ x e. A A. y e. A -. x  suc dom ( iota_ x e. A A. y e. A -. x
42 19 40 41 sylc 
 |-  ( ( E. x e. A A. y e. A -. x  suc dom ( iota_ x e. A A. y e. A -. x
43 16 42 eqsstrd 
 |-  ( ( E. x e. A A. y e. A -. x  dom S C_ O )
44 iffalse 
 |-  ( -. E. x e. A A. y e. A -. x  if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) ) = ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
45 1 44 syl5eq 
 |-  ( -. E. x e. A A. y e. A -. x  S = ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
46 45 dmeqd 
 |-  ( -. E. x e. A A. y e. A -. x  dom S = dom ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
47 iotaex 
 |-  ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) e. _V
48 eqid 
 |-  ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) = ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) )
49 47 48 dmmpti 
 |-  dom ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v  ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) = { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) }
50 46 49 eqtrdi 
 |-  ( -. E. x e. A A. y e. A -. x  dom S = { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } )
51 50 adantr 
 |-  ( ( -. E. x e. A A. y e. A -. x  dom S = { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } )
52 simplrl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) /\ u e. A ) -> O e. On )
53 ssel2 
 |-  ( ( A C_ No /\ u e. A ) -> u e. No )
54 53 ad4ant14 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) /\ u e. A ) -> u e. No )
55 bdayval 
 |-  ( u e. No -> ( bday ` u ) = dom u )
56 54 55 syl 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) /\ u e. A ) -> ( bday ` u ) = dom u )
57 simplrr 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) /\ u e. A ) -> ( bday " A ) C_ O )
58 fnfvima 
 |-  ( ( bday Fn No /\ A C_ No /\ u e. A ) -> ( bday ` u ) e. ( bday " A ) )
59 36 58 mp3an1 
 |-  ( ( A C_ No /\ u e. A ) -> ( bday ` u ) e. ( bday " A ) )
60 59 ad4ant14 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) /\ u e. A ) -> ( bday ` u ) e. ( bday " A ) )
61 57 60 sseldd 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) /\ u e. A ) -> ( bday ` u ) e. O )
62 56 61 eqeltrrd 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) /\ u e. A ) -> dom u e. O )
63 onelss 
 |-  ( O e. On -> ( dom u e. O -> dom u C_ O ) )
64 52 62 63 sylc 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) /\ u e. A ) -> dom u C_ O )
65 64 sseld 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) /\ u e. A ) -> ( y e. dom u -> y e. O ) )
66 65 adantrd 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) /\ u e. A ) -> ( ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) -> y e. O ) )
67 66 rexlimdva 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) -> ( E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) -> y e. O ) )
68 67 abssdv 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) -> { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } C_ O )
69 68 adantl 
 |-  ( ( -. E. x e. A A. y e. A -. x  { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v  ( u |` suc y ) = ( v |` suc y ) ) ) } C_ O )
70 51 69 eqsstrd 
 |-  ( ( -. E. x e. A A. y e. A -. x  dom S C_ O )
71 43 70 pm2.61ian 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) -> dom S C_ O )
72 5 71 eqsstrd 
 |-  ( ( ( A C_ No /\ A e. _V ) /\ ( O e. On /\ ( bday " A ) C_ O ) ) -> ( bday ` S ) C_ O )