madeval

Description: The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021)

		Ref	Expression
	Assertion	madeval	$⊢ A \in On \to M (A) = \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]]$

Proof

Step	Hyp	Ref	Expression
1		df-made	$⊢ M = recs ((x \in V ⟼ \|_{s} [𝒫 ⋃ ran x \times 𝒫 ⋃ ran x]))$
2	1	tfr2	$⊢ A \in On \to M (A) = (x \in V ⟼ \|_{s} [𝒫 ⋃ ran x \times 𝒫 ⋃ ran x]) ({M ↾}_{A})$
3		eqid	$⊢ (x \in V ⟼ \|_{s} [𝒫 ⋃ ran x \times 𝒫 ⋃ ran x]) = (x \in V ⟼ \|_{s} [𝒫 ⋃ ran x \times 𝒫 ⋃ ran x])$
4		rneq	$⊢ x = {M ↾}_{A} \to ran x = ran ({M ↾}_{A})$
5		df-ima	$⊢ M [A] = ran ({M ↾}_{A})$
6	4 5	eqtr4di	$⊢ x = {M ↾}_{A} \to ran x = M [A]$
7	6	unieqd	$⊢ x = {M ↾}_{A} \to ⋃ ran x = ⋃ M [A]$
8	7	pweqd	$⊢ x = {M ↾}_{A} \to 𝒫 ⋃ ran x = 𝒫 ⋃ M [A]$
9	8	sqxpeqd	$⊢ x = {M ↾}_{A} \to 𝒫 ⋃ ran x \times 𝒫 ⋃ ran x = 𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]$
10	9	imaeq2d	$⊢ x = {M ↾}_{A} \to \|_{s} [𝒫 ⋃ ran x \times 𝒫 ⋃ ran x] = \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]]$
11	1	tfr1	$⊢ M Fn On$
12		fnfun	$⊢ M Fn On \to Fun M$
13	11 12	ax-mp	$⊢ Fun M$
14		resfunexg	$⊢ (Fun M \land A \in On) \to {M ↾}_{A} \in V$
15	13 14	mpan	$⊢ A \in On \to {M ↾}_{A} \in V$
16		scutf	$⊢ \|_{s} : ≪_{s} ⟶ No$
17		ffun	$⊢ \|_{s} : ≪_{s} ⟶ No \to Fun \|_{s}$
18	16 17	ax-mp	$⊢ Fun \|_{s}$
19		funimaexg	$⊢ (Fun M \land A \in On) \to M [A] \in V$
20	13 19	mpan	$⊢ A \in On \to M [A] \in V$
21		uniexg	$⊢ M [A] \in V \to ⋃ M [A] \in V$
22		pwexg	$⊢ ⋃ M [A] \in V \to 𝒫 ⋃ M [A] \in V$
23	20 21 22	3syl	$⊢ A \in On \to 𝒫 ⋃ M [A] \in V$
24	23 23	xpexd	$⊢ A \in On \to 𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A] \in V$
25		funimaexg	$⊢ (Fun \|_{s} \land 𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A] \in V) \to \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]] \in V$
26	18 24 25	sylancr	$⊢ A \in On \to \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]] \in V$
27	3 10 15 26	fvmptd3	$⊢ A \in On \to (x \in V ⟼ \|_{s} [𝒫 ⋃ ran x \times 𝒫 ⋃ ran x]) ({M ↾}_{A}) = \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]]$
28	2 27	eqtrd	$⊢ A \in On \to M (A) = \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]]$

Metamath Proof Explorer

Theorem madeval

Proof