Metamath Proof Explorer

Theorem madebday

Description: A surreal is part of the set made by ordinal A iff its birthday is less than or equal to A . Remark in Conway p. 29. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Assertion madebday 
|- ( ( A e. On /\ X e. No ) -> ( X e. ( _M ` A ) <-> ( bday ` X ) C_ A ) )

Proof

Step Hyp Ref Expression
1 madebdayim 
 |-  ( ( A e. On /\ X e. ( _M ` A ) ) -> ( bday ` X ) C_ A )
2 1 ex 
 |-  ( A e. On -> ( X e. ( _M ` A ) -> ( bday ` X ) C_ A ) )
3 2 adantr 
 |-  ( ( A e. On /\ X e. No ) -> ( X e. ( _M ` A ) -> ( bday ` X ) C_ A ) )
4 sseq2 
 |-  ( a = b -> ( ( bday ` x ) C_ a <-> ( bday ` x ) C_ b ) )
5 fveq2 
 |-  ( a = b -> ( _M ` a ) = ( _M ` b ) )
6 5 eleq2d 
 |-  ( a = b -> ( x e. ( _M ` a ) <-> x e. ( _M ` b ) ) )
7 4 6 imbi12d 
 |-  ( a = b -> ( ( ( bday ` x ) C_ a -> x e. ( _M ` a ) ) <-> ( ( bday ` x ) C_ b -> x e. ( _M ` b ) ) ) )
8 7 ralbidv 
 |-  ( a = b -> ( A. x e. No ( ( bday ` x ) C_ a -> x e. ( _M ` a ) ) <-> A. x e. No ( ( bday ` x ) C_ b -> x e. ( _M ` b ) ) ) )
9 fveq2 
 |-  ( x = y -> ( bday ` x ) = ( bday ` y ) )
10 9 sseq1d 
 |-  ( x = y -> ( ( bday ` x ) C_ b <-> ( bday ` y ) C_ b ) )
11 eleq1 
 |-  ( x = y -> ( x e. ( _M ` b ) <-> y e. ( _M ` b ) ) )
12 10 11 imbi12d 
 |-  ( x = y -> ( ( ( bday ` x ) C_ b -> x e. ( _M ` b ) ) <-> ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) )
13 12 cbvralvw 
 |-  ( A. x e. No ( ( bday ` x ) C_ b -> x e. ( _M ` b ) ) <-> A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) )
14 8 13 bitrdi 
 |-  ( a = b -> ( A. x e. No ( ( bday ` x ) C_ a -> x e. ( _M ` a ) ) <-> A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) )
15 sseq2 
 |-  ( a = A -> ( ( bday ` x ) C_ a <-> ( bday ` x ) C_ A ) )
16 fveq2 
 |-  ( a = A -> ( _M ` a ) = ( _M ` A ) )
17 16 eleq2d 
 |-  ( a = A -> ( x e. ( _M ` a ) <-> x e. ( _M ` A ) ) )
18 15 17 imbi12d 
 |-  ( a = A -> ( ( ( bday ` x ) C_ a -> x e. ( _M ` a ) ) <-> ( ( bday ` x ) C_ A -> x e. ( _M ` A ) ) ) )
19 18 ralbidv 
 |-  ( a = A -> ( A. x e. No ( ( bday ` x ) C_ a -> x e. ( _M ` a ) ) <-> A. x e. No ( ( bday ` x ) C_ A -> x e. ( _M ` A ) ) ) )
20 bdayelon 
 |-  ( bday ` x ) e. On
21 onsseleq 
 |-  ( ( ( bday ` x ) e. On /\ a e. On ) -> ( ( bday ` x ) C_ a <-> ( ( bday ` x ) e. a \/ ( bday ` x ) = a ) ) )
22 20 21 mpan 
 |-  ( a e. On -> ( ( bday ` x ) C_ a <-> ( ( bday ` x ) e. a \/ ( bday ` x ) = a ) ) )
23 22 ad2antrr 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) C_ a <-> ( ( bday ` x ) e. a \/ ( bday ` x ) = a ) ) )
24 simpll 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) -> a e. On )
25 onelss 
 |-  ( a e. On -> ( ( bday ` x ) e. a -> ( bday ` x ) C_ a ) )
26 25 ad2antrr 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) e. a -> ( bday ` x ) C_ a ) )
27 26 imp 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( bday ` x ) C_ a )
28 madess 
 |-  ( ( ( bday ` x ) e. On /\ a e. On /\ ( bday ` x ) C_ a ) -> ( _M ` ( bday ` x ) ) C_ ( _M ` a ) )
29 20 24 27 28 mp3an2ani 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( _M ` ( bday ` x ) ) C_ ( _M ` a ) )
30 ssid 
 |-  ( bday ` x ) C_ ( bday ` x )
31 simpr 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( bday ` x ) e. a )
32 simplr 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> x e. No )
33 31 32 jca 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( ( bday ` x ) e. a /\ x e. No ) )
34 simpllr 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) )
35 sseq2 
 |-  ( b = ( bday ` x ) -> ( ( bday ` y ) C_ b <-> ( bday ` y ) C_ ( bday ` x ) ) )
36 fveq2 
 |-  ( b = ( bday ` x ) -> ( _M ` b ) = ( _M ` ( bday ` x ) ) )
37 36 eleq2d 
 |-  ( b = ( bday ` x ) -> ( y e. ( _M ` b ) <-> y e. ( _M ` ( bday ` x ) ) ) )
38 35 37 imbi12d 
 |-  ( b = ( bday ` x ) -> ( ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) <-> ( ( bday ` y ) C_ ( bday ` x ) -> y e. ( _M ` ( bday ` x ) ) ) ) )
39 fveq2 
 |-  ( y = x -> ( bday ` y ) = ( bday ` x ) )
40 39 sseq1d 
 |-  ( y = x -> ( ( bday ` y ) C_ ( bday ` x ) <-> ( bday ` x ) C_ ( bday ` x ) ) )
41 eleq1 
 |-  ( y = x -> ( y e. ( _M ` ( bday ` x ) ) <-> x e. ( _M ` ( bday ` x ) ) ) )
42 40 41 imbi12d 
 |-  ( y = x -> ( ( ( bday ` y ) C_ ( bday ` x ) -> y e. ( _M ` ( bday ` x ) ) ) <-> ( ( bday ` x ) C_ ( bday ` x ) -> x e. ( _M ` ( bday ` x ) ) ) ) )
43 38 42 rspc2v 
 |-  ( ( ( bday ` x ) e. a /\ x e. No ) -> ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) -> ( ( bday ` x ) C_ ( bday ` x ) -> x e. ( _M ` ( bday ` x ) ) ) ) )
44 33 34 43 sylc 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( ( bday ` x ) C_ ( bday ` x ) -> x e. ( _M ` ( bday ` x ) ) ) )
45 30 44 mpi 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> x e. ( _M ` ( bday ` x ) ) )
46 29 45 sseldd 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> x e. ( _M ` a ) )
47 46 ex 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) e. a -> x e. ( _M ` a ) ) )
48 madebdaylemlrcut 
 |-  ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ x e. No ) -> ( ( _L ` x ) |s ( _R ` x ) ) = x )
49 20 a1i 
 |-  ( x e. No -> ( bday ` x ) e. On )
50 lltropt 
 |-  ( x e. No -> ( _L ` x ) <
51 leftssold 
 |-  ( x e. No -> ( _L ` x ) C_ ( _Old ` ( bday ` x ) ) )
52 rightssold 
 |-  ( x e. No -> ( _R ` x ) C_ ( _Old ` ( bday ` x ) ) )
53 madecut 
 |-  ( ( ( ( bday ` x ) e. On /\ ( _L ` x ) < ( ( _L ` x ) |s ( _R ` x ) ) e. ( _M ` ( bday ` x ) ) )
54 49 50 51 52 53 syl22anc 
 |-  ( x e. No -> ( ( _L ` x ) |s ( _R ` x ) ) e. ( _M ` ( bday ` x ) ) )
55 54 adantl 
 |-  ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ x e. No ) -> ( ( _L ` x ) |s ( _R ` x ) ) e. ( _M ` ( bday ` x ) ) )
56 48 55 eqeltrrd 
 |-  ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ x e. No ) -> x e. ( _M ` ( bday ` x ) ) )
57 raleq 
 |-  ( ( bday ` x ) = a -> ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) <-> A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) )
58 57 anbi1d 
 |-  ( ( bday ` x ) = a -> ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ x e. No ) <-> ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ x e. No ) ) )
59 fveq2 
 |-  ( ( bday ` x ) = a -> ( _M ` ( bday ` x ) ) = ( _M ` a ) )
60 59 eleq2d 
 |-  ( ( bday ` x ) = a -> ( x e. ( _M ` ( bday ` x ) ) <-> x e. ( _M ` a ) ) )
61 58 60 imbi12d 
 |-  ( ( bday ` x ) = a -> ( ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ x e. No ) -> x e. ( _M ` ( bday ` x ) ) ) <-> ( ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ x e. No ) -> x e. ( _M ` a ) ) ) )
62 56 61 mpbii 
 |-  ( ( bday ` x ) = a -> ( ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ x e. No ) -> x e. ( _M ` a ) ) )
63 62 com12 
 |-  ( ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) /\ x e. No ) -> ( ( bday ` x ) = a -> x e. ( _M ` a ) ) )
64 63 adantll 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) = a -> x e. ( _M ` a ) ) )
65 47 64 jaod 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) -> ( ( ( bday ` x ) e. a \/ ( bday ` x ) = a ) -> x e. ( _M ` a ) ) )
66 23 65 sylbid 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) C_ a -> x e. ( _M ` a ) ) )
67 66 ralrimiva 
 |-  ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) -> A. x e. No ( ( bday ` x ) C_ a -> x e. ( _M ` a ) ) )
68 67 ex 
 |-  ( a e. On -> ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) -> A. x e. No ( ( bday ` x ) C_ a -> x e. ( _M ` a ) ) ) )
69 14 19 68 tfis3 
 |-  ( A e. On -> A. x e. No ( ( bday ` x ) C_ A -> x e. ( _M ` A ) ) )
70 fveq2 
 |-  ( x = X -> ( bday ` x ) = ( bday ` X ) )
71 70 sseq1d 
 |-  ( x = X -> ( ( bday ` x ) C_ A <-> ( bday ` X ) C_ A ) )
72 eleq1 
 |-  ( x = X -> ( x e. ( _M ` A ) <-> X e. ( _M ` A ) ) )
73 71 72 imbi12d 
 |-  ( x = X -> ( ( ( bday ` x ) C_ A -> x e. ( _M ` A ) ) <-> ( ( bday ` X ) C_ A -> X e. ( _M ` A ) ) ) )
74 73 rspccva 
 |-  ( ( A. x e. No ( ( bday ` x ) C_ A -> x e. ( _M ` A ) ) /\ X e. No ) -> ( ( bday ` X ) C_ A -> X e. ( _M ` A ) ) )
75 69 74 sylan 
 |-  ( ( A e. On /\ X e. No ) -> ( ( bday ` X ) C_ A -> X e. ( _M ` A ) ) )
76 3 75 impbid 
 |-  ( ( A e. On /\ X e. No ) -> ( X e. ( _M ` A ) <-> ( bday ` X ) C_ A ) )