Theorem madeval

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

	Ref	Expression
Assertion	madeval	⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = ( |s “ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-made	⊢ M = recs ( ( 𝑥 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) ) ) )
2	1	tfr2	⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = ( ( 𝑥 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) ) ) ‘ ( M ↾ 𝐴 ) ) )
3		eqid	⊢ ( 𝑥 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) ) ) = ( 𝑥 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) ) )
4		rneq	⊢ ( 𝑥 = ( M ↾ 𝐴 ) → ran 𝑥 = ran ( M ↾ 𝐴 ) )
5		df-ima	⊢ ( M “ 𝐴 ) = ran ( M ↾ 𝐴 )
6	4 5	eqtr4di	⊢ ( 𝑥 = ( M ↾ 𝐴 ) → ran 𝑥 = ( M “ 𝐴 ) )
7	6	unieqd	⊢ ( 𝑥 = ( M ↾ 𝐴 ) → ∪ ran 𝑥 = ∪ ( M “ 𝐴 ) )
8	7	pweqd	⊢ ( 𝑥 = ( M ↾ 𝐴 ) → 𝒫 ∪ ran 𝑥 = 𝒫 ∪ ( M “ 𝐴 ) )
9	8	sqxpeqd	⊢ ( 𝑥 = ( M ↾ 𝐴 ) → ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) = ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) )
10	9	imaeq2d	⊢ ( 𝑥 = ( M ↾ 𝐴 ) → ( |s “ ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) ) = ( |s “ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ) )
11	1	tfr1	⊢ M Fn On
12		fnfun	⊢ ( M Fn On → Fun M )
13	11 12	ax-mp	⊢ Fun M
14		resfunexg	⊢ ( ( Fun M ∧ 𝐴 ∈ On ) → ( M ↾ 𝐴 ) ∈ V )
15	13 14	mpan	⊢ ( 𝐴 ∈ On → ( M ↾ 𝐴 ) ∈ V )
16		scutf	⊢ |s : <<s ⟶ No
17		ffun	⊢ ( |s : <<s ⟶ No → Fun |s )
18	16 17	ax-mp	⊢ Fun |s
19		funimaexg	⊢ ( ( Fun M ∧ 𝐴 ∈ On ) → ( M “ 𝐴 ) ∈ V )
20	13 19	mpan	⊢ ( 𝐴 ∈ On → ( M “ 𝐴 ) ∈ V )
21		uniexg	⊢ ( ( M “ 𝐴 ) ∈ V → ∪ ( M “ 𝐴 ) ∈ V )
22		pwexg	⊢ ( ∪ ( M “ 𝐴 ) ∈ V → 𝒫 ∪ ( M “ 𝐴 ) ∈ V )
23	20 21 22	3syl	⊢ ( 𝐴 ∈ On → 𝒫 ∪ ( M “ 𝐴 ) ∈ V )
24	23 23	xpexd	⊢ ( 𝐴 ∈ On → ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∈ V )
25		funimaexg	⊢ ( ( Fun |s ∧ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∈ V ) → ( |s “ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ) ∈ V )
26	18 24 25	sylancr	⊢ ( 𝐴 ∈ On → ( |s “ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ) ∈ V )
27	3 10 15 26	fvmptd3	⊢ ( 𝐴 ∈ On → ( ( 𝑥 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑥 × 𝒫 ∪ ran 𝑥 ) ) ) ‘ ( M ↾ 𝐴 ) ) = ( |s “ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ) )
28	2 27	eqtrd	⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = ( |s “ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ) )