Theorem dssmapfvd

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

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

Proof

Step	Hyp	Ref	Expression
1		dssmapfvd.o	⊢ 𝑂 = ( 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ↦ ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) ) )
2		dssmapfvd.d	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3		dssmapfvd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4		pweq	⊢ ( 𝑏 = 𝐵 → 𝒫 𝑏 = 𝒫 𝐵 )
5	4 4	oveq12d	⊢ ( 𝑏 = 𝐵 → ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) = ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
6		id	⊢ ( 𝑏 = 𝐵 → 𝑏 = 𝐵 )
7		difeq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 ∖ 𝑠 ) = ( 𝐵 ∖ 𝑠 ) )
8	7	fveq2d	⊢ ( 𝑏 = 𝐵 → ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) = ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) )
9	6 8	difeq12d	⊢ ( 𝑏 = 𝐵 → ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) = ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
10	4 9	mpteq12dv	⊢ ( 𝑏 = 𝐵 → ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
11	5 10	mpteq12dv	⊢ ( 𝑏 = 𝐵 → ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ↦ ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) ) = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) )
12	3	elexd	⊢ ( 𝜑 → 𝐵 ∈ V )
13		ovex	⊢ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∈ V
14		mptexg	⊢ ( ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∈ V → ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ∈ V )
15	13 14	mp1i	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ∈ V )
16	1 11 12 15	fvmptd3	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐵 ) = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) )
17	2 16	syl5eq	⊢ ( 𝜑 → 𝐷 = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) )