Theorem newf

Description: The new function is a function from ordinals to sets of surreals. (Contributed by Scott Fenton, 6-Aug-2024)

	Ref	Expression
Assertion	newf	⊢ N : On ⟶ 𝒫 No

Proof

Step	Hyp	Ref	Expression
1		df-new	⊢ N = ( 𝑥 ∈ On ↦ ( ( M ‘ 𝑥 ) ∖ ( O ‘ 𝑥 ) ) )
2		madef	⊢ M : On ⟶ 𝒫 No
3	2	ffvelcdmi	⊢ ( 𝑥 ∈ On → ( M ‘ 𝑥 ) ∈ 𝒫 No )
4	3	elpwid	⊢ ( 𝑥 ∈ On → ( M ‘ 𝑥 ) ⊆ No )
5	4	ssdifssd	⊢ ( 𝑥 ∈ On → ( ( M ‘ 𝑥 ) ∖ ( O ‘ 𝑥 ) ) ⊆ No )
6		fvex	⊢ ( M ‘ 𝑥 ) ∈ V
7	6	difexi	⊢ ( ( M ‘ 𝑥 ) ∖ ( O ‘ 𝑥 ) ) ∈ V
8	7	elpw	⊢ ( ( ( M ‘ 𝑥 ) ∖ ( O ‘ 𝑥 ) ) ∈ 𝒫 No ↔ ( ( M ‘ 𝑥 ) ∖ ( O ‘ 𝑥 ) ) ⊆ No )
9	5 8	sylibr	⊢ ( 𝑥 ∈ On → ( ( M ‘ 𝑥 ) ∖ ( O ‘ 𝑥 ) ) ∈ 𝒫 No )
10	1 9	fmpti	⊢ N : On ⟶ 𝒫 No