Theorem newval

Description: The value of the new options function. (Contributed by Scott Fenton, 9-Oct-2024)

	Ref	Expression
Assertion	newval	⊢ ( N ‘ 𝐴 ) = ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑥 = 𝐴 → ( M ‘ 𝑥 ) = ( M ‘ 𝐴 ) )
2		fveq2	⊢ ( 𝑥 = 𝐴 → ( O ‘ 𝑥 ) = ( O ‘ 𝐴 ) )
3	1 2	difeq12d	⊢ ( 𝑥 = 𝐴 → ( ( M ‘ 𝑥 ) ∖ ( O ‘ 𝑥 ) ) = ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) )
4		df-new	⊢ N = ( 𝑥 ∈ On ↦ ( ( M ‘ 𝑥 ) ∖ ( O ‘ 𝑥 ) ) )
5		fvex	⊢ ( M ‘ 𝐴 ) ∈ V
6	5	difexi	⊢ ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) ∈ V
7	3 4 6	fvmpt	⊢ ( 𝐴 ∈ On → ( N ‘ 𝐴 ) = ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) )
8	4	fvmptndm	⊢ ( ¬ 𝐴 ∈ On → ( N ‘ 𝐴 ) = ∅ )
9		df-made	⊢ M = recs ( ( 𝑓 ∈ V ↦ ( |s “ ( 𝒫 ∪ ran 𝑓 × 𝒫 ∪ ran 𝑓 ) ) ) )
10	9	tfr1	⊢ M Fn On
11	10	fndmi	⊢ dom M = On
12	11	eleq2i	⊢ ( 𝐴 ∈ dom M ↔ 𝐴 ∈ On )
13		ndmfv	⊢ ( ¬ 𝐴 ∈ dom M → ( M ‘ 𝐴 ) = ∅ )
14	12 13	sylnbir	⊢ ( ¬ 𝐴 ∈ On → ( M ‘ 𝐴 ) = ∅ )
15	14	difeq1d	⊢ ( ¬ 𝐴 ∈ On → ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) = ( ∅ ∖ ( O ‘ 𝐴 ) ) )
16		0dif	⊢ ( ∅ ∖ ( O ‘ 𝐴 ) ) = ∅
17	15 16	eqtrdi	⊢ ( ¬ 𝐴 ∈ On → ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) = ∅ )
18	8 17	eqtr4d	⊢ ( ¬ 𝐴 ∈ On → ( N ‘ 𝐴 ) = ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) ) )
19	7 18	pm2.61i	⊢ ( N ‘ 𝐴 ) = ( ( M ‘ 𝐴 ) ∖ ( O ‘ 𝐴 ) )