oldval

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

		Ref	Expression
	Assertion	oldval	$⊢ A \in On \to Old (A) = ⋃ M [A]$

Step	Hyp	Ref	Expression
1		df-made	$⊢ M = recs ((x \in V ⟼ \|_{s} [𝒫 ⋃ ran x \times 𝒫 ⋃ ran x]))$
2		recsfnon	$⊢ recs ((x \in V ⟼ \|_{s} [𝒫 ⋃ ran x \times 𝒫 ⋃ ran x])) Fn On$
3		fnfun	$⊢ recs ((x \in V ⟼ \|_{s} [𝒫 ⋃ ran x \times 𝒫 ⋃ ran x])) Fn On \to Fun recs ((x \in V ⟼ \|_{s} [𝒫 ⋃ ran x \times 𝒫 ⋃ ran x]))$
4	2 3	ax-mp	$⊢ Fun recs ((x \in V ⟼ \|_{s} [𝒫 ⋃ ran x \times 𝒫 ⋃ ran x]))$
5		funeq	$⊢ M = recs ((x \in V ⟼ \|_{s} [𝒫 ⋃ ran x \times 𝒫 ⋃ ran x])) \to (Fun M \leftrightarrow Fun recs ((x \in V ⟼ \|_{s} [𝒫 ⋃ ran x \times 𝒫 ⋃ ran x])))$
6	4 5	mpbiri	$⊢ M = recs ((x \in V ⟼ \|_{s} [𝒫 ⋃ ran x \times 𝒫 ⋃ ran x])) \to Fun M$
7	1 6	ax-mp	$⊢ Fun M$
8		funimaexg	$⊢ (Fun M \land A \in On) \to M [A] \in V$
9	7 8	mpan	$⊢ A \in On \to M [A] \in V$
10	9	uniexd	$⊢ A \in On \to ⋃ M [A] \in V$
11		imaeq2	$⊢ x = A \to M [x] = M [A]$
12	11	unieqd	$⊢ x = A \to ⋃ M [x] = ⋃ M [A]$
13		df-old	$⊢ Old = (x \in On ⟼ ⋃ M [x])$
14	12 13	fvmptg	$⊢ (A \in On \land ⋃ M [A] \in V) \to Old (A) = ⋃ M [A]$
15	10 14	mpdan	$⊢ A \in On \to Old (A) = ⋃ M [A]$

Metamath Proof Explorer