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. ( _Made ` A ) <-> ( bday ` X ) C_ A ) )

Proof

Step Hyp Ref Expression
1 madebdayim 
 |-  ( X e. ( _Made ` A ) -> ( bday ` X ) C_ A )
2 sseq2 
 |-  ( a = b -> ( ( bday ` x ) C_ a <-> ( bday ` x ) C_ b ) )
3 fveq2 
 |-  ( a = b -> ( _Made ` a ) = ( _Made ` b ) )
4 3 eleq2d 
 |-  ( a = b -> ( x e. ( _Made ` a ) <-> x e. ( _Made ` b ) ) )
5 2 4 imbi12d 
 |-  ( a = b -> ( ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) <-> ( ( bday ` x ) C_ b -> x e. ( _Made ` b ) ) ) )
6 5 ralbidv 
 |-  ( a = b -> ( A. x e. No ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) <-> A. x e. No ( ( bday ` x ) C_ b -> x e. ( _Made ` 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. ( _Made ` b ) <-> y e. ( _Made ` b ) ) )
10 8 9 imbi12d 
 |-  ( x = y -> ( ( ( bday ` x ) C_ b -> x e. ( _Made ` b ) ) <-> ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) )
11 10 cbvralvw 
 |-  ( A. x e. No ( ( bday ` x ) C_ b -> x e. ( _Made ` b ) ) <-> A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) )
12 6 11 bitrdi 
 |-  ( a = b -> ( A. x e. No ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) <-> A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) )
13 sseq2 
 |-  ( a = A -> ( ( bday ` x ) C_ a <-> ( bday ` x ) C_ A ) )
14 fveq2 
 |-  ( a = A -> ( _Made ` a ) = ( _Made ` A ) )
15 14 eleq2d 
 |-  ( a = A -> ( x e. ( _Made ` a ) <-> x e. ( _Made ` A ) ) )
16 13 15 imbi12d 
 |-  ( a = A -> ( ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) <-> ( ( bday ` x ) C_ A -> x e. ( _Made ` A ) ) ) )
17 16 ralbidv 
 |-  ( a = A -> ( A. x e. No ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) <-> A. x e. No ( ( bday ` x ) C_ A -> x e. ( _Made ` 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. ( _Made ` 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. ( _Made ` 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. ( _Made ` 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. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( bday ` x ) C_ a )
26 madess 
 |-  ( ( a e. On /\ ( bday ` x ) C_ a ) -> ( _Made ` ( bday ` x ) ) C_ ( _Made ` a ) )
27 22 25 26 syl2an2r 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( _Made ` ( bday ` x ) ) C_ ( _Made ` 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. ( _Made ` 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. ( _Made ` 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. ( _Made ` 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. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) )
33 sseq2 
 |-  ( b = ( bday ` x ) -> ( ( bday ` y ) C_ b <-> ( bday ` y ) C_ ( bday ` x ) ) )
34 fveq2 
 |-  ( b = ( bday ` x ) -> ( _Made ` b ) = ( _Made ` ( bday ` x ) ) )
35 34 eleq2d 
 |-  ( b = ( bday ` x ) -> ( y e. ( _Made ` b ) <-> y e. ( _Made ` ( bday ` x ) ) ) )
36 33 35 imbi12d 
 |-  ( b = ( bday ` x ) -> ( ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) <-> ( ( bday ` y ) C_ ( bday ` x ) -> y e. ( _Made ` ( 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. ( _Made ` ( bday ` x ) ) <-> x e. ( _Made ` ( bday ` x ) ) ) )
40 38 39 imbi12d 
 |-  ( y = x -> ( ( ( bday ` y ) C_ ( bday ` x ) -> y e. ( _Made ` ( bday ` x ) ) ) <-> ( ( bday ` x ) C_ ( bday ` x ) -> x e. ( _Made ` ( 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. ( _Made ` b ) ) -> ( ( bday ` x ) C_ ( bday ` x ) -> x e. ( _Made ` ( bday ` x ) ) ) ) )
42 31 32 41 sylc 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( ( bday ` x ) C_ ( bday ` x ) -> x e. ( _Made ` ( bday ` x ) ) ) )
43 28 42 mpi 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> x e. ( _Made ` ( bday ` x ) ) )
44 27 43 sseldd 
 |-  ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> x e. ( _Made ` a ) )
45 44 ex 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) e. a -> x e. ( _Made ` a ) ) )
46 madebdaylemlrcut 
 |-  ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x )
47 18 a1i 
 |-  ( x e. No -> ( bday ` x ) e. On )
48 lltropt 
 |-  ( _Left ` x ) <
49 48 a1i 
 |-  ( x e. No -> ( _Left ` x ) <
50 leftssold 
 |-  ( _Left ` x ) C_ ( _Old ` ( bday ` x ) )
51 50 a1i 
 |-  ( x e. No -> ( _Left ` x ) C_ ( _Old ` ( bday ` x ) ) )
52 rightssold 
 |-  ( _Right ` x ) C_ ( _Old ` ( bday ` x ) )
53 52 a1i 
 |-  ( x e. No -> ( _Right ` x ) C_ ( _Old ` ( bday ` x ) ) )
54 madecut 
 |-  ( ( ( ( bday ` x ) e. On /\ ( _Left ` x ) < ( ( _Left ` x ) |s ( _Right ` x ) ) e. ( _Made ` ( bday ` x ) ) )
55 47 49 51 53 54 syl22anc 
 |-  ( x e. No -> ( ( _Left ` x ) |s ( _Right ` x ) ) e. ( _Made ` ( bday ` x ) ) )
56 55 adantl 
 |-  ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) e. ( _Made ` ( bday ` x ) ) )
57 46 56 eqeltrrd 
 |-  ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> x e. ( _Made ` ( bday ` x ) ) )
58 raleq 
 |-  ( ( bday ` x ) = a -> ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) <-> A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) )
59 58 anbi1d 
 |-  ( ( bday ` x ) = a -> ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) <-> ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) ) )
60 fveq2 
 |-  ( ( bday ` x ) = a -> ( _Made ` ( bday ` x ) ) = ( _Made ` a ) )
61 60 eleq2d 
 |-  ( ( bday ` x ) = a -> ( x e. ( _Made ` ( bday ` x ) ) <-> x e. ( _Made ` a ) ) )
62 59 61 imbi12d 
 |-  ( ( bday ` x ) = a -> ( ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> x e. ( _Made ` ( bday ` x ) ) ) <-> ( ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> x e. ( _Made ` a ) ) ) )
63 57 62 mpbii 
 |-  ( ( bday ` x ) = a -> ( ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> x e. ( _Made ` a ) ) )
64 63 com12 
 |-  ( ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> ( ( bday ` x ) = a -> x e. ( _Made ` a ) ) )
65 64 adantll 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) = a -> x e. ( _Made ` a ) ) )
66 45 65 jaod 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( ( bday ` x ) e. a \/ ( bday ` x ) = a ) -> x e. ( _Made ` a ) ) )
67 21 66 sylbid 
 |-  ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) )
68 67 ralrimiva 
 |-  ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) -> A. x e. No ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) )
69 68 ex 
 |-  ( a e. On -> ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) -> A. x e. No ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) ) )
70 12 17 69 tfis3 
 |-  ( A e. On -> A. x e. No ( ( bday ` x ) C_ A -> x e. ( _Made ` A ) ) )
71 fveq2 
 |-  ( x = X -> ( bday ` x ) = ( bday ` X ) )
72 71 sseq1d 
 |-  ( x = X -> ( ( bday ` x ) C_ A <-> ( bday ` X ) C_ A ) )
73 eleq1 
 |-  ( x = X -> ( x e. ( _Made ` A ) <-> X e. ( _Made ` A ) ) )
74 72 73 imbi12d 
 |-  ( x = X -> ( ( ( bday ` x ) C_ A -> x e. ( _Made ` A ) ) <-> ( ( bday ` X ) C_ A -> X e. ( _Made ` A ) ) ) )
75 74 rspccva 
 |-  ( ( A. x e. No ( ( bday ` x ) C_ A -> x e. ( _Made ` A ) ) /\ X e. No ) -> ( ( bday ` X ) C_ A -> X e. ( _Made ` A ) ) )
76 70 75 sylan 
 |-  ( ( A e. On /\ X e. No ) -> ( ( bday ` X ) C_ A -> X e. ( _Made ` A ) ) )
77 1 76 impbid2 
 |-  ( ( A e. On /\ X e. No ) -> ( X e. ( _Made ` A ) <-> ( bday ` X ) C_ A ) )