Theorem oldbday

Description: A surreal is part of the set older than ordinal A iff its birthday is less than A . Remark in Conway p. 29. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Assertion	oldbday	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( O ‘ 𝐴 ) ↔ ( bday ‘ 𝑋 ) ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		oldbdayim	⊢ ( 𝑋 ∈ ( O ‘ 𝐴 ) → ( bday ‘ 𝑋 ) ∈ 𝐴 )
2		simpl	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → 𝐴 ∈ On )
3		onelon	⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ∈ On )
4		madebday	⊢ ( ( 𝑏 ∈ On ∧ 𝑦 ∈ No ) → ( 𝑦 ∈ ( M ‘ 𝑏 ) ↔ ( bday ‘ 𝑦 ) ⊆ 𝑏 ) )
5	4	biimprd	⊢ ( ( 𝑏 ∈ On ∧ 𝑦 ∈ No ) → ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) )
6	3 5	sylan	⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑦 ∈ No ) → ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) )
7	6	anasss	⊢ ( ( 𝐴 ∈ On ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑦 ∈ No ) ) → ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) )
8	7	ralrimivva	⊢ ( 𝐴 ∈ On → ∀ 𝑏 ∈ 𝐴 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) )
9	8	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ∀ 𝑏 ∈ 𝐴 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) )
10		simpr	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → 𝑋 ∈ No )
11		madebdaylemold	⊢ ( ( 𝐴 ∈ On ∧ ∀ 𝑏 ∈ 𝐴 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( ( bday ‘ 𝑋 ) ∈ 𝐴 → 𝑋 ∈ ( O ‘ 𝐴 ) ) )
12	2 9 10 11	syl3anc	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( ( bday ‘ 𝑋 ) ∈ 𝐴 → 𝑋 ∈ ( O ‘ 𝐴 ) ) )
13	1 12	impbid2	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( O ‘ 𝐴 ) ↔ ( bday ‘ 𝑋 ) ∈ 𝐴 ) )