Metamath Proof Explorer

Theorem bdayon

Description: The birthday of a surreal ordinal is the set of all previous ordinal birthdays. (Contributed by Scott Fenton, 7-Nov-2025)

Ref Expression
Assertion bdayon 
|- ( A e. On_s -> ( bday ` A ) = ( bday " { x e. On_s | x

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( a = b -> ( bday ` a ) = ( bday ` b ) )
2 breq2 
 |-  ( a = b -> ( x  x
3 2 rabbidv 
 |-  ( a = b -> { x e. On_s | x
4 breq1 
 |-  ( x = y -> ( x  y
5 4 cbvrabv 
 |-  { x e. On_s | x
6 3 5 eqtrdi 
 |-  ( a = b -> { x e. On_s | x
7 6 imaeq2d 
 |-  ( a = b -> ( bday " { x e. On_s | x
8 1 7 eqeq12d 
 |-  ( a = b -> ( ( bday ` a ) = ( bday " { x e. On_s | x  ( bday ` b ) = ( bday " { y e. On_s | y
9 fveq2 
 |-  ( a = A -> ( bday ` a ) = ( bday ` A ) )
10 breq2 
 |-  ( a = A -> ( x  x
11 10 rabbidv 
 |-  ( a = A -> { x e. On_s | x
12 11 imaeq2d 
 |-  ( a = A -> ( bday " { x e. On_s | x
13 9 12 eqeq12d 
 |-  ( a = A -> ( ( bday ` a ) = ( bday " { x e. On_s | x  ( bday ` A ) = ( bday " { x e. On_s | x
14 onscutlt 
 |-  ( a e. On_s -> a = ( { x e. On_s | x
15 14 adantr 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  a = ( { x e. On_s | x
16 15 fveq2d 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( bday ` a ) = ( bday ` ( { x e. On_s | x
17 onsno 
 |-  ( a e. On_s -> a e. No )
18 sltonex 
 |-  ( a e. No -> { x e. On_s | x
19 17 18 syl 
 |-  ( a e. On_s -> { x e. On_s | x
20 19 adantr 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  { x e. On_s | x
21 ssrab2 
 |-  { x e. On_s | x
22 onssno 
 |-  On_s C_ No
23 21 22 sstri 
 |-  { x e. On_s | x
24 23 a1i 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  { x e. On_s | x
25 20 24 elpwd 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  { x e. On_s | x
26 nulssgt 
 |-  ( { x e. On_s | x  { x e. On_s | x
27 25 26 syl 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  { x e. On_s | x
28 bdayfn 
 |-  bday Fn No
29 fvelimab 
 |-  ( ( bday Fn No /\ { x e. On_s | x  ( q e. ( bday " { x e. On_s | x  E. z e. { x e. On_s | x
30 28 23 29 mp2an 
 |-  ( q e. ( bday " { x e. On_s | x  E. z e. { x e. On_s | x
31 breq1 
 |-  ( x = z -> ( x  z
32 31 rexrab 
 |-  ( E. z e. { x e. On_s | x  E. z e. On_s ( z
33 30 32 bitri 
 |-  ( q e. ( bday " { x e. On_s | x  E. z e. On_s ( z
34 breq1 
 |-  ( b = z -> ( b  z
35 fveq2 
 |-  ( b = z -> ( bday ` b ) = ( bday ` z ) )
36 breq2 
 |-  ( b = z -> ( y  y
37 36 rabbidv 
 |-  ( b = z -> { y e. On_s | y
38 breq1 
 |-  ( x = y -> ( x  y
39 38 cbvrabv 
 |-  { x e. On_s | x
40 37 39 eqtr4di 
 |-  ( b = z -> { y e. On_s | y
41 40 imaeq2d 
 |-  ( b = z -> ( bday " { y e. On_s | y
42 35 41 eqeq12d 
 |-  ( b = z -> ( ( bday ` b ) = ( bday " { y e. On_s | y  ( bday ` z ) = ( bday " { x e. On_s | x
43 34 42 imbi12d 
 |-  ( b = z -> ( ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( z  ( bday ` z ) = ( bday " { x e. On_s | x
44 43 rspccv 
 |-  ( A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( z e. On_s -> ( z  ( bday ` z ) = ( bday " { x e. On_s | x
45 44 imp 
 |-  ( ( A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( z  ( bday ` z ) = ( bday " { x e. On_s | x
46 45 adantll 
 |-  ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( z  ( bday ` z ) = ( bday " { x e. On_s | x
47 46 impr 
 |-  ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( bday ` z ) = ( bday " { x e. On_s | x
48 simplrr 
 |-  ( ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  z
49 onsno 
 |-  ( x e. On_s -> x e. No )
50 49 adantl 
 |-  ( ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  x e. No )
51 simplrl 
 |-  ( ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  z e. On_s )
52 onsno 
 |-  ( z e. On_s -> z e. No )
53 51 52 syl 
 |-  ( ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  z e. No )
54 simplll 
 |-  ( ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  a e. On_s )
55 54 17 syl 
 |-  ( ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  a e. No )
56 slttr 
 |-  ( ( x e. No /\ z e. No /\ a e. No ) -> ( ( x  x
57 50 53 55 56 syl3anc 
 |-  ( ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( ( x  x
58 48 57 mpan2d 
 |-  ( ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( x  x
59 58 ss2rabdv 
 |-  ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  { x e. On_s | x
60 imass2 
 |-  ( { x e. On_s | x  ( bday " { x e. On_s | x
61 59 60 syl 
 |-  ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( bday " { x e. On_s | x
62 47 61 eqsstrd 
 |-  ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( bday ` z ) C_ ( bday " { x e. On_s | x
63 62 sseld 
 |-  ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( p e. ( bday ` z ) -> p e. ( bday " { x e. On_s | x
64 eleq2 
 |-  ( ( bday ` z ) = q -> ( p e. ( bday ` z ) <-> p e. q ) )
65 64 imbi1d 
 |-  ( ( bday ` z ) = q -> ( ( p e. ( bday ` z ) -> p e. ( bday " { x e. On_s | x  ( p e. q -> p e. ( bday " { x e. On_s | x
66 65 bicomd 
 |-  ( ( bday ` z ) = q -> ( ( p e. q -> p e. ( bday " { x e. On_s | x  ( p e. ( bday ` z ) -> p e. ( bday " { x e. On_s | x
67 63 66 syl5ibrcom 
 |-  ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( ( bday ` z ) = q -> ( p e. q -> p e. ( bday " { x e. On_s | x
68 67 expr 
 |-  ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( z  ( ( bday ` z ) = q -> ( p e. q -> p e. ( bday " { x e. On_s | x
69 68 impd 
 |-  ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( ( z  ( p e. q -> p e. ( bday " { x e. On_s | x
70 69 rexlimdva 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( E. z e. On_s ( z  ( p e. q -> p e. ( bday " { x e. On_s | x
71 33 70 biimtrid 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( q e. ( bday " { x e. On_s | x  ( p e. q -> p e. ( bday " { x e. On_s | x
72 71 impcomd 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( ( p e. q /\ q e. ( bday " { x e. On_s | x  p e. ( bday " { x e. On_s | x
73 72 alrimivv 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  A. p A. q ( ( p e. q /\ q e. ( bday " { x e. On_s | x  p e. ( bday " { x e. On_s | x
74 imassrn 
 |-  ( bday " { x e. On_s | x
75 bdayrn 
 |-  ran bday = On
76 74 75 sseqtri 
 |-  ( bday " { x e. On_s | x
77 dford5 
 |-  ( Ord ( bday " { x e. On_s | x  ( ( bday " { x e. On_s | x
78 76 77 mpbiran 
 |-  ( Ord ( bday " { x e. On_s | x  Tr ( bday " { x e. On_s | x
79 dftr2 
 |-  ( Tr ( bday " { x e. On_s | x  A. p A. q ( ( p e. q /\ q e. ( bday " { x e. On_s | x  p e. ( bday " { x e. On_s | x
80 78 79 bitri 
 |-  ( Ord ( bday " { x e. On_s | x  A. p A. q ( ( p e. q /\ q e. ( bday " { x e. On_s | x  p e. ( bday " { x e. On_s | x
81 73 80 sylibr 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  Ord ( bday " { x e. On_s | x
82 bdayfun 
 |-  Fun bday
83 funimaexg 
 |-  ( ( Fun bday /\ { x e. On_s | x  ( bday " { x e. On_s | x
84 82 20 83 sylancr 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( bday " { x e. On_s | x
85 elon2 
 |-  ( ( bday " { x e. On_s | x  ( Ord ( bday " { x e. On_s | x
86 81 84 85 sylanbrc 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( bday " { x e. On_s | x
87 un0 
 |-  ( { x e. On_s | x
88 87 imaeq2i 
 |-  ( bday " ( { x e. On_s | x
89 88 eqimssi 
 |-  ( bday " ( { x e. On_s | x
90 scutbdaybnd 
 |-  ( ( { x e. On_s | x  ( bday ` ( { x e. On_s | x
91 89 90 mp3an3 
 |-  ( ( { x e. On_s | x  ( bday ` ( { x e. On_s | x
92 27 86 91 syl2anc 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( bday ` ( { x e. On_s | x
93 16 92 eqsstrd 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( bday ` a ) C_ ( bday " { x e. On_s | x
94 simpr 
 |-  ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  z e. On_s )
95 simpll 
 |-  ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  a e. On_s )
96 onslt 
 |-  ( ( z e. On_s /\ a e. On_s ) -> ( z  ( bday ` z ) e. ( bday ` a ) ) )
97 94 95 96 syl2anc 
 |-  ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( z  ( bday ` z ) e. ( bday ` a ) ) )
98 97 biimpd 
 |-  ( ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( z  ( bday ` z ) e. ( bday ` a ) ) )
99 98 ralrimiva 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  A. z e. On_s ( z  ( bday ` z ) e. ( bday ` a ) ) )
100 bdaydm 
 |-  dom bday = No
101 23 100 sseqtrri 
 |-  { x e. On_s | x
102 funimass4 
 |-  ( ( Fun bday /\ { x e. On_s | x  ( ( bday " { x e. On_s | x  A. z e. { x e. On_s | x
103 82 101 102 mp2an 
 |-  ( ( bday " { x e. On_s | x  A. z e. { x e. On_s | x
104 31 ralrab 
 |-  ( A. z e. { x e. On_s | x  A. z e. On_s ( z  ( bday ` z ) e. ( bday ` a ) ) )
105 103 104 bitri 
 |-  ( ( bday " { x e. On_s | x  A. z e. On_s ( z  ( bday ` z ) e. ( bday ` a ) ) )
106 99 105 sylibr 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( bday " { x e. On_s | x
107 93 106 eqssd 
 |-  ( ( a e. On_s /\ A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( bday ` a ) = ( bday " { x e. On_s | x
108 107 ex 
 |-  ( a e. On_s -> ( A. b e. On_s ( b  ( bday ` b ) = ( bday " { y e. On_s | y  ( bday ` a ) = ( bday " { x e. On_s | x
109 8 13 108 onsis 
 |-  ( A e. On_s -> ( bday ` A ) = ( bday " { x e. On_s | x