Metamath Proof Explorer

Theorem bdayons

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 bdayons ⊢ A ∈ On s → bday ⁡ A = bday x ∈ On s | x < s A

Proof

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