Theorem dssmap2d

Description: For any base set B the duality operator for self-mappings of subsets of that base set when composed with itself is the restricted identity operator. (Contributed by RP, 21-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		dssmapfvd.o	⊢ 𝑂 = ( 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ↦ ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) ) )
2		dssmapfvd.d	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3		dssmapfvd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4	1 2 3	dssmapnvod	⊢ ( 𝜑 → ◡ 𝐷 = 𝐷 )
5	4	coeq1d	⊢ ( 𝜑 → ( ◡ 𝐷 ∘ 𝐷 ) = ( 𝐷 ∘ 𝐷 ) )
6	1 2 3	dssmapf1od	⊢ ( 𝜑 → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
7		f1ococnv1	⊢ ( 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → ( ◡ 𝐷 ∘ 𝐷 ) = ( I ↾ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) )
8	6 7	syl	⊢ ( 𝜑 → ( ◡ 𝐷 ∘ 𝐷 ) = ( I ↾ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) )
9	5 8	eqtr3d	⊢ ( 𝜑 → ( 𝐷 ∘ 𝐷 ) = ( I ↾ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) )