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	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ ( O ‘ 𝐴 ) ) → ( bday ‘ 𝑋 ) ∈ 𝐴 )
2	1	ex	⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( O ‘ 𝐴 ) → ( bday ‘ 𝑋 ) ∈ 𝐴 ) )
3	2	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( O ‘ 𝐴 ) → ( bday ‘ 𝑋 ) ∈ 𝐴 ) )
4		simpl	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → 𝐴 ∈ On )
5		onelon	⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ∈ On )
6		madebday	⊢ ( ( 𝑏 ∈ On ∧ 𝑦 ∈ No ) → ( 𝑦 ∈ ( M ‘ 𝑏 ) ↔ ( bday ‘ 𝑦 ) ⊆ 𝑏 ) )
7	6	biimprd	⊢ ( ( 𝑏 ∈ On ∧ 𝑦 ∈ No ) → ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) )
8	5 7	sylan	⊢ ( ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑦 ∈ No ) → ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) )
9	8	anasss	⊢ ( ( 𝐴 ∈ On ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑦 ∈ No ) ) → ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) )
10	9	ralrimivva	⊢ ( 𝐴 ∈ On → ∀ 𝑏 ∈ 𝐴 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) )
11	10	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ∀ 𝑏 ∈ 𝐴 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) )
12		simpr	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → 𝑋 ∈ No )
13		madebdaylemold	⊢ ( ( 𝐴 ∈ On ∧ ∀ 𝑏 ∈ 𝐴 ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( ( bday ‘ 𝑋 ) ∈ 𝐴 → 𝑋 ∈ ( O ‘ 𝐴 ) ) )
14	4 11 12 13	syl3anc	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( ( bday ‘ 𝑋 ) ∈ 𝐴 → 𝑋 ∈ ( O ‘ 𝐴 ) ) )
15	3 14	impbid	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ No ) → ( 𝑋 ∈ ( O ‘ 𝐴 ) ↔ ( bday ‘ 𝑋 ) ∈ 𝐴 ) )