Theorem dssmapfv3d

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

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

Proof

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