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 
 |-  ( X e. ( _M ` A ) -> ( bday ` X ) C_ A )
2 sseq2 
 |-  ( a = b -> ( ( bday ` x ) C_ a <-> ( bday ` x ) C_ b ) )
3 fveq2 
 |-  ( a = b -> ( _M ` a ) = ( _M ` b ) )
4 3 eleq2d 
 |-  ( a = b -> ( x e. ( _M ` a ) <-> x e. ( _M ` b ) ) )
5 2 4 imbi12d 
 |-  ( a = b -> ( ( ( bday ` x ) C_ a -> x e. ( _M ` a ) ) <-> ( ( bday ` x ) C_ b -> x e. ( _M ` b ) ) ) )
6 5 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 ) ) ) )
7 fveq2 
 |-  ( x = y -> ( bday ` x ) = ( bday ` y ) )
8 7 sseq1d 
 |-  ( x = y -> ( ( bday ` x ) C_ b <-> ( bday ` y ) C_ b ) )
9 eleq1 
 |-  ( x = y -> ( x e. ( _M ` b ) <-> y e. ( _M ` b ) ) )
10 8 9 imbi12d 
 |-  ( x = y -> ( ( ( bday ` x ) C_ b -> x e. ( _M ` b ) ) <-> ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) ) )
11 10 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 ) ) )
12 6 11 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 ) ) ) )
13 sseq2 
 |-  ( a = A -> ( ( bday ` x ) C_ a <-> ( bday ` x ) C_ A ) )
14 fveq2 
 |-  ( a = A -> ( _M ` a ) = ( _M ` A ) )
15 14 eleq2d 
 |-  ( a = A -> ( x e. ( _M ` a ) <-> x e. ( _M ` A ) ) )
16 13 15 imbi12d 
 |-  ( a = A -> ( ( ( bday ` x ) C_ a -> x e. ( _M ` a ) ) <-> ( ( bday ` x ) C_ A -> x e. ( _M ` A ) ) ) )
17 16 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 ) ) ) )
18 bdayelon 
 |-  ( bday ` x ) e. On
19 onsseleq 
 |-  ( ( ( bday ` x ) e. On /\ a e. On ) -> ( ( bday ` x ) C_ a <-> ( ( bday ` x ) e. a \/ ( bday ` x ) = a ) ) )
20 18 19 mpan 
 |-  ( a e. On -> ( ( bday ` x ) C_ a <-> ( ( bday ` x ) e. a \/ ( bday ` x ) = a ) ) )
21 20 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 ) ) )
22 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 )
23 onelss 
 |-  ( a e. On -> ( ( bday ` x ) e. a -> ( bday ` x ) C_ a ) )
24 23 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 ) )
25 24 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 )
26 madess 
 |-  ( ( a e. On /\ ( bday ` x ) C_ a ) -> ( _M ` ( bday ` x ) ) C_ ( _M ` a ) )
27 22 25 26 syl2an2r 
 |-  ( ( ( ( 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 ) )
28 ssid 
 |-  ( bday ` x ) C_ ( bday ` x )
29 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 )
30 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 )
31 29 30 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 ) )
32 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 ) ) )
33 sseq2 
 |-  ( b = ( bday ` x ) -> ( ( bday ` y ) C_ b <-> ( bday ` y ) C_ ( bday ` x ) ) )
34 fveq2 
 |-  ( b = ( bday ` x ) -> ( _M ` b ) = ( _M ` ( bday ` x ) ) )
35 34 eleq2d 
 |-  ( b = ( bday ` x ) -> ( y e. ( _M ` b ) <-> y e. ( _M ` ( bday ` x ) ) ) )
36 33 35 imbi12d 
 |-  ( b = ( bday ` x ) -> ( ( ( bday ` y ) C_ b -> y e. ( _M ` b ) ) <-> ( ( bday ` y ) C_ ( bday ` x ) -> y e. ( _M ` ( bday ` x ) ) ) ) )
37 fveq2 
 |-  ( y = x -> ( bday ` y ) = ( bday ` x ) )
38 37 sseq1d 
 |-  ( y = x -> ( ( bday ` y ) C_ ( bday ` x ) <-> ( bday ` x ) C_ ( bday ` x ) ) )
39 eleq1 
 |-  ( y = x -> ( y e. ( _M ` ( bday ` x ) ) <-> x e. ( _M ` ( bday ` x ) ) ) )
40 38 39 imbi12d 
 |-  ( y = x -> ( ( ( bday ` y ) C_ ( bday ` x ) -> y e. ( _M ` ( bday ` x ) ) ) <-> ( ( bday ` x ) C_ ( bday ` x ) -> x e. ( _M ` ( bday ` x ) ) ) ) )
41 36 40 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 ) ) ) ) )
42 31 32 41 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 ) ) ) )
43 28 42 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 ) ) )
44 27 43 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 ) )
45 44 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 ) ) )
46 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 )
47 18 a1i 
 |-  ( x e. No -> ( bday ` x ) e. On )
48 lltropt 
 |-  ( x e. No -> ( _L ` x ) <
49 leftssold 
 |-  ( _L ` x ) C_ ( _Old ` ( bday ` x ) )
50 49 a1i 
 |-  ( x e. No -> ( _L ` x ) C_ ( _Old ` ( bday ` x ) ) )
51 rightssold 
 |-  ( _R ` x ) C_ ( _Old ` ( bday ` x ) )
52 51 a1i 
 |-  ( 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 47 48 50 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 46 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 45 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 21 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 12 17 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 1 75 impbid2 
 |-  ( ( A e. On /\ X e. No ) -> ( X e. ( _M ` A ) <-> ( bday ` X ) C_ A ) )