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	⊢ ( 𝐴 ∈ Ons → ( bday ‘ 𝐴 ) = ( bday “ { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ) )

Proof

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