Theorem dssmapfv2d

Description: Value of the duality operator for self-mappings of subsets of a base set, B when applied to function F . (Contributed by RP, 19-Apr-2021)

	Ref	Expression
Hypotheses	dssmapfvd.o	⊢ 𝑂 = ( 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ↦ ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) ) )
	dssmapfvd.d	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
	dssmapfvd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	dssmapfv2d.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
	dssmapfv2d.g	⊢ 𝐺 = ( 𝐷 ‘ 𝐹 )
Assertion	dssmapfv2d	⊢ ( 𝜑 → 𝐺 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝐹 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dssmapfvd.o	⊢ 𝑂 = ( 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ↦ ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) ) )
2		dssmapfvd.d	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3		dssmapfvd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4		dssmapfv2d.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
5		dssmapfv2d.g	⊢ 𝐺 = ( 𝐷 ‘ 𝐹 )
6	1 2 3	dssmapfvd	⊢ ( 𝜑 → 𝐷 = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) )
7		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) = ( 𝐹 ‘ ( 𝐵 ∖ 𝑠 ) ) )
8	7	difeq2d	⊢ ( 𝑓 = 𝐹 → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) = ( 𝐵 ∖ ( 𝐹 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
9	8	mpteq2dv	⊢ ( 𝑓 = 𝐹 → ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝐹 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝐹 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
11		pwexg	⊢ ( 𝐵 ∈ 𝑉 → 𝒫 𝐵 ∈ V )
12		mptexg	⊢ ( 𝒫 𝐵 ∈ V → ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝐹 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ∈ V )
13	3 11 12	3syl	⊢ ( 𝜑 → ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝐹 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ∈ V )
14	6 10 4 13	fvmptd	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐹 ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝐹 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
15	5 14	syl5eq	⊢ ( 𝜑 → 𝐺 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝐹 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )