Metamath Proof Explorer

Theorem oldval

Description: The value of the old options function. (Contributed by Scott Fenton, 6-Aug-2024)

Ref Expression
Assertion oldval ( 𝐴 ∈ On → ( O ‘ 𝐴 ) = ∪ ( M “ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 df-made ⊢ M = recs ( ( 𝑥 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) ) ) )
2 recsfnon ⊢ recs ( ( 𝑥 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) ) ) ) Fn On
3 fnfun ⊢ ( recs ( ( 𝑥 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) ) ) ) Fn On → Fun recs ( ( 𝑥 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) ) ) ) )
4 2 3 ax-mp ⊢ Fun recs ( ( 𝑥 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) ) ) )
5 funeq ⊢ ( M = recs ( ( 𝑥 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) ) ) ) → ( Fun M ↔ Fun recs ( ( 𝑥 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) ) ) ) ) )
6 4 5 mpbiri ⊢ ( M = recs ( ( 𝑥 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) ) ) ) → Fun M )
7 1 6 ax-mp ⊢ Fun M
8 funimaexg ⊢ ( ( Fun M ∧ 𝐴 ∈ On ) → ( M “ 𝐴 ) ∈ V )
9 7 8 mpan ⊢ ( 𝐴 ∈ On → ( M “ 𝐴 ) ∈ V )
10 9 uniexd ⊢ ( 𝐴 ∈ On → ∪ ( M “ 𝐴 ) ∈ V )
11 imaeq2 ⊢ ( 𝑥 = 𝐴 → ( M “ 𝑥 ) = ( M “ 𝐴 ) )
12 11 unieqd ⊢ ( 𝑥 = 𝐴 → ∪ ( M “ 𝑥 ) = ∪ ( M “ 𝐴 ) )
13 df-old ⊢ O = ( 𝑥 ∈ On ↦ ∪ ( M “ 𝑥 ) )
14 12 13 fvmptg ⊢ ( ( 𝐴 ∈ On ∧ ∪ ( M “ 𝐴 ) ∈ V ) → ( O ‘ 𝐴 ) = ∪ ( M “ 𝐴 ) )
15 10 14 mpdan ⊢ ( 𝐴 ∈ On → ( O ‘ 𝐴 ) = ∪ ( M “ 𝐴 ) )