Theorem oldf

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

	Ref	Expression
Assertion	oldf	⊢ O : On ⟶ 𝒫 No

Proof

Step	Hyp	Ref	Expression
1		df-old	⊢ O = ( 𝑥 ∈ On ↦ ∪ ( M “ 𝑥 ) )
2		imassrn	⊢ ( M “ 𝑥 ) ⊆ ran M
3		madef	⊢ M : On ⟶ 𝒫 No
4		frn	⊢ ( M : On ⟶ 𝒫 No → ran M ⊆ 𝒫 No )
5	3 4	ax-mp	⊢ ran M ⊆ 𝒫 No
6	2 5	sstri	⊢ ( M “ 𝑥 ) ⊆ 𝒫 No
7	6	sseli	⊢ ( 𝑦 ∈ ( M “ 𝑥 ) → 𝑦 ∈ 𝒫 No )
8	7	elpwid	⊢ ( 𝑦 ∈ ( M “ 𝑥 ) → 𝑦 ⊆ No )
9	8	rgen	⊢ ∀ 𝑦 ∈ ( M “ 𝑥 ) 𝑦 ⊆ No
10	9	a1i	⊢ ( 𝑥 ∈ On → ∀ 𝑦 ∈ ( M “ 𝑥 ) 𝑦 ⊆ No )
11		ffun	⊢ ( M : On ⟶ 𝒫 No → Fun M )
12	3 11	ax-mp	⊢ Fun M
13		vex	⊢ 𝑥 ∈ V
14	13	funimaex	⊢ ( Fun M → ( M “ 𝑥 ) ∈ V )
15	12 14	ax-mp	⊢ ( M “ 𝑥 ) ∈ V
16	15	uniex	⊢ ∪ ( M “ 𝑥 ) ∈ V
17	16	elpw	⊢ ( ∪ ( M “ 𝑥 ) ∈ 𝒫 No ↔ ∪ ( M “ 𝑥 ) ⊆ No )
18		unissb	⊢ ( ∪ ( M “ 𝑥 ) ⊆ No ↔ ∀ 𝑦 ∈ ( M “ 𝑥 ) 𝑦 ⊆ No )
19	17 18	bitri	⊢ ( ∪ ( M “ 𝑥 ) ∈ 𝒫 No ↔ ∀ 𝑦 ∈ ( M “ 𝑥 ) 𝑦 ⊆ No )
20	10 19	sylibr	⊢ ( 𝑥 ∈ On → ∪ ( M “ 𝑥 ) ∈ 𝒫 No )
21	1 20	fmpti	⊢ O : On ⟶ 𝒫 No