Metamath Proof Explorer

Theorem madebdayim

Description: If a surreal is a member of a made set, its birthday is less than or equal to the level. (Contributed by Scott Fenton, 10-Aug-2024)

Ref Expression
Assertion madebdayim 
|- ( X e. ( _M ` A ) -> ( bday ` X ) C_ A )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( X e. ( _M ` A ) -> A e. dom _M )
2 madef 
 |-  _M : On --> ~P No
3 2 fdmi 
 |-  dom _M = On
4 1 3 eleqtrdi 
 |-  ( X e. ( _M ` A ) -> A e. On )
5 fveq2 
 |-  ( a = b -> ( _M ` a ) = ( _M ` b ) )
6 sseq2 
 |-  ( a = b -> ( ( bday ` x ) C_ a <-> ( bday ` x ) C_ b ) )
7 5 6 raleqbidv 
 |-  ( a = b -> ( A. x e. ( _M ` a ) ( bday ` x ) C_ a <-> A. x e. ( _M ` b ) ( bday ` x ) C_ b ) )
8 fveq2 
 |-  ( x = y -> ( bday ` x ) = ( bday ` y ) )
9 8 sseq1d 
 |-  ( x = y -> ( ( bday ` x ) C_ b <-> ( bday ` y ) C_ b ) )
10 9 cbvralvw 
 |-  ( A. x e. ( _M ` b ) ( bday ` x ) C_ b <-> A. y e. ( _M ` b ) ( bday ` y ) C_ b )
11 7 10 bitrdi 
 |-  ( a = b -> ( A. x e. ( _M ` a ) ( bday ` x ) C_ a <-> A. y e. ( _M ` b ) ( bday ` y ) C_ b ) )
12 fveq2 
 |-  ( a = A -> ( _M ` a ) = ( _M ` A ) )
13 sseq2 
 |-  ( a = A -> ( ( bday ` x ) C_ a <-> ( bday ` x ) C_ A ) )
14 12 13 raleqbidv 
 |-  ( a = A -> ( A. x e. ( _M ` a ) ( bday ` x ) C_ a <-> A. x e. ( _M ` A ) ( bday ` x ) C_ A ) )
15 elmade2 
 |-  ( a e. On -> ( x e. ( _M ` a ) <-> E. l e. ~P ( _Old ` a ) E. r e. ~P ( _Old ` a ) ( l <
16 15 adantr 
 |-  ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) -> ( x e. ( _M ` a ) <-> E. l e. ~P ( _Old ` a ) E. r e. ~P ( _Old ` a ) ( l <
17 elpwi 
 |-  ( l e. ~P ( _Old ` a ) -> l C_ ( _Old ` a ) )
18 elpwi 
 |-  ( r e. ~P ( _Old ` a ) -> r C_ ( _Old ` a ) )
19 17 18 anim12i 
 |-  ( ( l e. ~P ( _Old ` a ) /\ r e. ~P ( _Old ` a ) ) -> ( l C_ ( _Old ` a ) /\ r C_ ( _Old ` a ) ) )
20 unss 
 |-  ( ( l C_ ( _Old ` a ) /\ r C_ ( _Old ` a ) ) <-> ( l u. r ) C_ ( _Old ` a ) )
21 19 20 sylib 
 |-  ( ( l e. ~P ( _Old ` a ) /\ r e. ~P ( _Old ` a ) ) -> ( l u. r ) C_ ( _Old ` a ) )
22 simpr 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < l <
23 simplll 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < a e. On )
24 dfss3 
 |-  ( ( l u. r ) C_ ( _Old ` a ) <-> A. z e. ( l u. r ) z e. ( _Old ` a ) )
25 fveq2 
 |-  ( y = z -> ( bday ` y ) = ( bday ` z ) )
26 25 sseq1d 
 |-  ( y = z -> ( ( bday ` y ) C_ b <-> ( bday ` z ) C_ b ) )
27 26 rspccv 
 |-  ( A. y e. ( _M ` b ) ( bday ` y ) C_ b -> ( z e. ( _M ` b ) -> ( bday ` z ) C_ b ) )
28 27 ralimi 
 |-  ( A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b -> A. b e. a ( z e. ( _M ` b ) -> ( bday ` z ) C_ b ) )
29 rexim 
 |-  ( A. b e. a ( z e. ( _M ` b ) -> ( bday ` z ) C_ b ) -> ( E. b e. a z e. ( _M ` b ) -> E. b e. a ( bday ` z ) C_ b ) )
30 28 29 syl 
 |-  ( A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b -> ( E. b e. a z e. ( _M ` b ) -> E. b e. a ( bday ` z ) C_ b ) )
31 30 adantl 
 |-  ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) -> ( E. b e. a z e. ( _M ` b ) -> E. b e. a ( bday ` z ) C_ b ) )
32 elold 
 |-  ( a e. On -> ( z e. ( _Old ` a ) <-> E. b e. a z e. ( _M ` b ) ) )
33 32 adantr 
 |-  ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) -> ( z e. ( _Old ` a ) <-> E. b e. a z e. ( _M ` b ) ) )
34 bdayelon 
 |-  ( bday ` z ) e. On
35 onelssex 
 |-  ( ( ( bday ` z ) e. On /\ a e. On ) -> ( ( bday ` z ) e. a <-> E. b e. a ( bday ` z ) C_ b ) )
36 34 35 mpan 
 |-  ( a e. On -> ( ( bday ` z ) e. a <-> E. b e. a ( bday ` z ) C_ b ) )
37 36 adantr 
 |-  ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) -> ( ( bday ` z ) e. a <-> E. b e. a ( bday ` z ) C_ b ) )
38 31 33 37 3imtr4d 
 |-  ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) -> ( z e. ( _Old ` a ) -> ( bday ` z ) e. a ) )
39 38 ralimdv 
 |-  ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) -> ( A. z e. ( l u. r ) z e. ( _Old ` a ) -> A. z e. ( l u. r ) ( bday ` z ) e. a ) )
40 24 39 syl5bi 
 |-  ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) -> ( ( l u. r ) C_ ( _Old ` a ) -> A. z e. ( l u. r ) ( bday ` z ) e. a ) )
41 40 imp 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) -> A. z e. ( l u. r ) ( bday ` z ) e. a )
42 41 adantr 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < A. z e. ( l u. r ) ( bday ` z ) e. a )
43 bdayfun 
 |-  Fun bday
44 oldssno 
 |-  ( _Old ` a ) C_ No
45 sstr 
 |-  ( ( ( l u. r ) C_ ( _Old ` a ) /\ ( _Old ` a ) C_ No ) -> ( l u. r ) C_ No )
46 44 45 mpan2 
 |-  ( ( l u. r ) C_ ( _Old ` a ) -> ( l u. r ) C_ No )
47 bdaydm 
 |-  dom bday = No
48 46 47 sseqtrrdi 
 |-  ( ( l u. r ) C_ ( _Old ` a ) -> ( l u. r ) C_ dom bday )
49 funimass4 
 |-  ( ( Fun bday /\ ( l u. r ) C_ dom bday ) -> ( ( bday " ( l u. r ) ) C_ a <-> A. z e. ( l u. r ) ( bday ` z ) e. a ) )
50 43 48 49 sylancr 
 |-  ( ( l u. r ) C_ ( _Old ` a ) -> ( ( bday " ( l u. r ) ) C_ a <-> A. z e. ( l u. r ) ( bday ` z ) e. a ) )
51 50 adantl 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) -> ( ( bday " ( l u. r ) ) C_ a <-> A. z e. ( l u. r ) ( bday ` z ) e. a ) )
52 51 adantr 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < ( ( bday " ( l u. r ) ) C_ a <-> A. z e. ( l u. r ) ( bday ` z ) e. a ) )
53 42 52 mpbird 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < ( bday " ( l u. r ) ) C_ a )
54 scutbdaybnd 
 |-  ( ( l < ( bday ` ( l |s r ) ) C_ a )
55 22 23 53 54 syl3anc 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < ( bday ` ( l |s r ) ) C_ a )
56 fveq2 
 |-  ( ( l |s r ) = x -> ( bday ` ( l |s r ) ) = ( bday ` x ) )
57 56 sseq1d 
 |-  ( ( l |s r ) = x -> ( ( bday ` ( l |s r ) ) C_ a <-> ( bday ` x ) C_ a ) )
58 55 57 syl5ibcom 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < ( ( l |s r ) = x -> ( bday ` x ) C_ a ) )
59 58 expimpd 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) -> ( ( l < ( bday ` x ) C_ a ) )
60 59 ex 
 |-  ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) -> ( ( l u. r ) C_ ( _Old ` a ) -> ( ( l < ( bday ` x ) C_ a ) ) )
61 21 60 syl5 
 |-  ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) -> ( ( l e. ~P ( _Old ` a ) /\ r e. ~P ( _Old ` a ) ) -> ( ( l < ( bday ` x ) C_ a ) ) )
62 61 rexlimdvv 
 |-  ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) -> ( E. l e. ~P ( _Old ` a ) E. r e. ~P ( _Old ` a ) ( l < ( bday ` x ) C_ a ) )
63 16 62 sylbid 
 |-  ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) -> ( x e. ( _M ` a ) -> ( bday ` x ) C_ a ) )
64 63 ralrimiv 
 |-  ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) -> A. x e. ( _M ` a ) ( bday ` x ) C_ a )
65 64 ex 
 |-  ( a e. On -> ( A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b -> A. x e. ( _M ` a ) ( bday ` x ) C_ a ) )
66 11 14 65 tfis3 
 |-  ( A e. On -> A. x e. ( _M ` A ) ( bday ` x ) C_ A )
67 fveq2 
 |-  ( x = X -> ( bday ` x ) = ( bday ` X ) )
68 67 sseq1d 
 |-  ( x = X -> ( ( bday ` x ) C_ A <-> ( bday ` X ) C_ A ) )
69 68 rspccv 
 |-  ( A. x e. ( _M ` A ) ( bday ` x ) C_ A -> ( X e. ( _M ` A ) -> ( bday ` X ) C_ A ) )
70 66 69 syl 
 |-  ( A e. On -> ( X e. ( _M ` A ) -> ( bday ` X ) C_ A ) )
71 4 70 mpcom 
 |-  ( X e. ( _M ` A ) -> ( bday ` X ) C_ A )