Theorem dssmapf1od

Description: For any base set B the duality operator for self-mappings of subsets of that base set is one-to-one and onto. (Contributed by RP, 21-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		dssmapfvd.o	⊢ 𝑂 = ( 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ↦ ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) ) )
2		dssmapfvd.d	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3		dssmapfvd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4	1 2 3	dssmapfvd	⊢ ( 𝜑 → 𝐷 = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) )
5	3	pwexd	⊢ ( 𝜑 → 𝒫 𝐵 ∈ V )
6	5	mptexd	⊢ ( 𝜑 → ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ∈ V )
7	6	ralrimivw	⊢ ( 𝜑 → ∀ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ∈ V )
8		nfcv	⊢ Ⅎ 𝑓 ( 𝒫 𝐵 ↑m 𝒫 𝐵 )
9	8	fnmptf	⊢ ( ∀ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ∈ V → ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
10	7 9	syl	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
11		fneq1	⊢ ( 𝐷 = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) → ( 𝐷 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↔ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) )
12	11	biimprd	⊢ ( 𝐷 = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) → ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐷 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) )
13	4 10 12	sylc	⊢ ( 𝜑 → 𝐷 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
14	1 2 3	dssmapnvod	⊢ ( 𝜑 → ◡ 𝐷 = 𝐷 )
15		nvof1o	⊢ ( ( 𝐷 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ ◡ 𝐷 = 𝐷 ) → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
16	13 14 15	syl2anc	⊢ ( 𝜑 → 𝐷 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )