Metamath Proof Explorer

Theorem madef

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

Ref Expression
Assertion madef ⊢ M : On ⟶ 𝒫 No

Proof

Step Hyp Ref Expression
1 df-made ⊢ M = recs ⁡ x ∈ V ⟼ | s 𝒫 ⋃ ran ⁡ x × 𝒫 ⋃ ran ⁡ x
2 1 tfr1 ⊢ M Fn On
3 madeval2 ⊢ x ∈ On → M ⁡ x = y ∈ No | ∃ z ∈ 𝒫 ⋃ M x ∃ w ∈ 𝒫 ⋃ M x z ≪ s w ∧ z | s w = y
4 ssrab2 ⊢ y ∈ No | ∃ z ∈ 𝒫 ⋃ M x ∃ w ∈ 𝒫 ⋃ M x z ≪ s w ∧ z | s w = y ⊆ No
5 3 4 eqsstrdi ⊢ x ∈ On → M ⁡ x ⊆ No
6 sseq1 ⊢ y = M ⁡ x → y ⊆ No ↔ M ⁡ x ⊆ No
7 5 6 syl5ibrcom ⊢ x ∈ On → y = M ⁡ x → y ⊆ No
8 7 rexlimiv ⊢ ∃ x ∈ On y = M ⁡ x → y ⊆ No
9 vex ⊢ y ∈ V
10 eqeq1 ⊢ z = y → z = M ⁡ x ↔ y = M ⁡ x
11 10 rexbidv ⊢ z = y → ∃ x ∈ On z = M ⁡ x ↔ ∃ x ∈ On y = M ⁡ x
12 fnrnfv ⊢ M Fn On → ran ⁡ M = z | ∃ x ∈ On z = M ⁡ x
13 2 12 ax-mp ⊢ ran ⁡ M = z | ∃ x ∈ On z = M ⁡ x
14 9 11 13 elab2 ⊢ y ∈ ran ⁡ M ↔ ∃ x ∈ On y = M ⁡ x
15 velpw ⊢ y ∈ 𝒫 No ↔ y ⊆ No
16 8 14 15 3imtr4i ⊢ y ∈ ran ⁡ M → y ∈ 𝒫 No
17 16 ssriv ⊢ ran ⁡ M ⊆ 𝒫 No
18 df-f ⊢ M : On ⟶ 𝒫 No ↔ M Fn On ∧ ran ⁡ M ⊆ 𝒫 No
19 2 17 18 mpbir2an ⊢ M : On ⟶ 𝒫 No