Theorem lrcut

Description: A surreal is equal to the cut of its left and right sets. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Assertion	lrcut	⊢ ( 𝑋 ∈ No → ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		bdayelon	⊢ ( bday ‘ 𝑋 ) ∈ On
2	1	oneli	⊢ ( 𝑏 ∈ ( bday ‘ 𝑋 ) → 𝑏 ∈ On )
3		madebday	⊢ ( ( 𝑏 ∈ On ∧ 𝑦 ∈ No ) → ( 𝑦 ∈ ( M ‘ 𝑏 ) ↔ ( bday ‘ 𝑦 ) ⊆ 𝑏 ) )
4	3	biimprd	⊢ ( ( 𝑏 ∈ On ∧ 𝑦 ∈ No ) → ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) )
5	2 4	sylan	⊢ ( ( 𝑏 ∈ ( bday ‘ 𝑋 ) ∧ 𝑦 ∈ No ) → ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) )
6	5	rgen2	⊢ ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) )
7		madebdaylemlrcut	⊢ ( ( ∀ 𝑏 ∈ ( bday ‘ 𝑋 ) ∀ 𝑦 ∈ No ( ( bday ‘ 𝑦 ) ⊆ 𝑏 → 𝑦 ∈ ( M ‘ 𝑏 ) ) ∧ 𝑋 ∈ No ) → ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = 𝑋 )
8	6 7	mpan	⊢ ( 𝑋 ∈ No → ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = 𝑋 )