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 
|- ( ( A e. On /\ X e. ( _M ` A ) ) -> ( bday ` X ) C_ A )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( a = b -> ( _M ` a ) = ( _M ` b ) )
2 sseq2 
 |-  ( a = b -> ( ( bday ` x ) C_ a <-> ( bday ` x ) C_ b ) )
3 1 2 raleqbidv 
 |-  ( a = b -> ( A. x e. ( _M ` a ) ( bday ` x ) C_ a <-> A. x e. ( _M ` b ) ( bday ` x ) C_ b ) )
4 fveq2 
 |-  ( x = y -> ( bday ` x ) = ( bday ` y ) )
5 4 sseq1d 
 |-  ( x = y -> ( ( bday ` x ) C_ b <-> ( bday ` y ) C_ b ) )
6 5 cbvralvw 
 |-  ( A. x e. ( _M ` b ) ( bday ` x ) C_ b <-> A. y e. ( _M ` b ) ( bday ` y ) C_ b )
7 3 6 bitrdi 
 |-  ( a = b -> ( A. x e. ( _M ` a ) ( bday ` x ) C_ a <-> A. y e. ( _M ` b ) ( bday ` y ) C_ b ) )
8 fveq2 
 |-  ( a = A -> ( _M ` a ) = ( _M ` A ) )
9 sseq2 
 |-  ( a = A -> ( ( bday ` x ) C_ a <-> ( bday ` x ) C_ A ) )
10 8 9 raleqbidv 
 |-  ( a = A -> ( A. x e. ( _M ` a ) ( bday ` x ) C_ a <-> A. x e. ( _M ` A ) ( bday ` x ) C_ A ) )
11 elmade2 
 |-  ( a e. On -> ( x e. ( _M ` a ) <-> E. l e. ~P ( _Old ` a ) E. r e. ~P ( _Old ` a ) ( l <
12 11 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 <
13 pwuncl 
 |-  ( ( l e. ~P ( _Old ` a ) /\ r e. ~P ( _Old ` a ) ) -> ( l u. r ) e. ~P ( _Old ` a ) )
14 13 elpwid 
 |-  ( ( l e. ~P ( _Old ` a ) /\ r e. ~P ( _Old ` a ) ) -> ( l u. r ) C_ ( _Old ` a ) )
15 simprr 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) /\ ( ( l u. r ) C_ ( _Old ` a ) /\ l < l <
16 simpll 
 |-  ( ( ( 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 )
17 dfss3 
 |-  ( ( l u. r ) C_ ( _Old ` a ) <-> A. z e. ( l u. r ) z e. ( _Old ` a ) )
18 fveq2 
 |-  ( y = z -> ( bday ` y ) = ( bday ` z ) )
19 18 sseq1d 
 |-  ( y = z -> ( ( bday ` y ) C_ b <-> ( bday ` z ) C_ b ) )
20 19 rspccv 
 |-  ( A. y e. ( _M ` b ) ( bday ` y ) C_ b -> ( z e. ( _M ` b ) -> ( bday ` z ) C_ b ) )
21 20 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 ) )
22 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 ) )
23 21 22 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 ) )
24 23 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 ) )
25 elold 
 |-  ( a e. On -> ( z e. ( _Old ` a ) <-> E. b e. a z e. ( _M ` b ) ) )
26 25 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 ) ) )
27 bdayelon 
 |-  ( bday ` z ) e. On
28 onelssex 
 |-  ( ( ( bday ` z ) e. On /\ a e. On ) -> ( ( bday ` z ) e. a <-> E. b e. a ( bday ` z ) C_ b ) )
29 27 28 mpan 
 |-  ( a e. On -> ( ( bday ` z ) e. a <-> E. b e. a ( bday ` z ) C_ b ) )
30 29 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 ) )
31 24 26 30 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 ) )
32 31 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 ) )
33 17 32 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 ) )
34 33 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 )
35 34 adantrr 
 |-  ( ( ( 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 )
36 bdayfun 
 |-  Fun bday
37 ssltss1 
 |-  ( l < l C_ No )
38 ssltss2 
 |-  ( l < r C_ No )
39 37 38 unssd 
 |-  ( l < ( l u. r ) C_ No )
40 39 adantl 
 |-  ( ( ( l u. r ) C_ ( _Old ` a ) /\ l < ( l u. r ) C_ No )
41 40 adantl 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) /\ ( ( l u. r ) C_ ( _Old ` a ) /\ l < ( l u. r ) C_ No )
42 bdaydm 
 |-  dom bday = No
43 41 42 sseqtrrdi 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. ( _M ` b ) ( bday ` y ) C_ b ) /\ ( ( l u. r ) C_ ( _Old ` a ) /\ l < ( l u. r ) C_ dom bday )
44 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 ) )
45 36 43 44 sylancr 
 |-  ( ( ( 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 ) )
46 35 45 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 )
47 scutbdaybnd 
 |-  ( ( l < ( bday ` ( l |s r ) ) C_ a )
48 15 16 46 47 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 )
49 fveq2 
 |-  ( ( l |s r ) = x -> ( bday ` ( l |s r ) ) = ( bday ` x ) )
50 49 sseq1d 
 |-  ( ( l |s r ) = x -> ( ( bday ` ( l |s r ) ) C_ a <-> ( bday ` x ) C_ a ) )
51 48 50 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 ) )
52 51 expr 
 |-  ( ( ( 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 ) ) )
53 52 impd 
 |-  ( ( ( 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 ) )
54 53 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 ) ) )
55 14 54 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 ) ) )
56 55 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 ) )
57 12 56 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 ) )
58 57 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 )
59 58 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 ) )
60 7 10 59 tfis3 
 |-  ( A e. On -> A. x e. ( _M ` A ) ( bday ` x ) C_ A )
61 fveq2 
 |-  ( x = X -> ( bday ` x ) = ( bday ` X ) )
62 61 sseq1d 
 |-  ( x = X -> ( ( bday ` x ) C_ A <-> ( bday ` X ) C_ A ) )
63 62 rspccva 
 |-  ( ( A. x e. ( _M ` A ) ( bday ` x ) C_ A /\ X e. ( _M ` A ) ) -> ( bday ` X ) C_ A )
64 60 63 sylan 
 |-  ( ( A e. On /\ X e. ( _M ` A ) ) -> ( bday ` X ) C_ A )