Theorem dssmapnvod

Description: For any base set B the duality operator for self-mappings of subsets of that base set is its own inverse, an involution. (Contributed by RP, 20-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		dssmapfvd.o	⊢ 𝑂 = ( 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ↦ ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) ) )
2		dssmapfvd.d	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3		dssmapfvd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4		simpr	⊢ ( ( 𝜑 ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) → 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
5		difeq2	⊢ ( 𝑠 = 𝑡 → ( 𝐵 ∖ 𝑠 ) = ( 𝐵 ∖ 𝑡 ) )
6	5	fveq2d	⊢ ( 𝑠 = 𝑡 → ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) = ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) )
7	6	difeq2d	⊢ ( 𝑠 = 𝑡 → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) = ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
8	7	cbvmptv	⊢ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) = ( 𝑡 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
9	4 8	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) → 𝑔 = ( 𝑡 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) )
10		ssun1	⊢ 𝐵 ⊆ ( 𝐵 ∪ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) )
11	10	sspwi	⊢ 𝒫 𝐵 ⊆ 𝒫 ( 𝐵 ∪ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) )
12		pwidg	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ 𝒫 𝐵 )
13	3 12	syl	⊢ ( 𝜑 → 𝐵 ∈ 𝒫 𝐵 )
14	11 13	sselid	⊢ ( 𝜑 → 𝐵 ∈ 𝒫 ( 𝐵 ∪ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
15		fvex	⊢ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ∈ V
16	15	elpwun	⊢ ( 𝐵 ∈ 𝒫 ( 𝐵 ∪ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ↔ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ∈ 𝒫 𝐵 )
17	14 16	sylib	⊢ ( 𝜑 → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ∈ 𝒫 𝐵 )
18	17	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ∈ 𝒫 𝐵 )
19	9 18	fmpt3d	⊢ ( ( 𝜑 ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) → 𝑔 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
20	3	pwexd	⊢ ( 𝜑 → 𝒫 𝐵 ∈ V )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) → 𝒫 𝐵 ∈ V )
22	21 21	elmapd	⊢ ( ( 𝜑 ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) → ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↔ 𝑔 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ) )
23	19 22	mpbird	⊢ ( ( 𝜑 ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) → 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
24	23	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ) → 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
25		simplr	⊢ ( ( ( 𝜑 ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
26		difeq2	⊢ ( 𝑠 = 𝑢 → ( 𝐵 ∖ 𝑠 ) = ( 𝐵 ∖ 𝑢 ) )
27	26	fveq2d	⊢ ( 𝑠 = 𝑢 → ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) = ( 𝑓 ‘ ( 𝐵 ∖ 𝑢 ) ) )
28	27	difeq2d	⊢ ( 𝑠 = 𝑢 → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) = ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑢 ) ) ) )
29	28	cbvmptv	⊢ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) = ( 𝑢 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑢 ) ) ) )
30	25 29	eqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑔 = ( 𝑢 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑢 ) ) ) ) )
31		difeq2	⊢ ( 𝑢 = ( 𝐵 ∖ 𝑡 ) → ( 𝐵 ∖ 𝑢 ) = ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) )
32	31	fveq2d	⊢ ( 𝑢 = ( 𝐵 ∖ 𝑡 ) → ( 𝑓 ‘ ( 𝐵 ∖ 𝑢 ) ) = ( 𝑓 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) )
33	32	difeq2d	⊢ ( 𝑢 = ( 𝐵 ∖ 𝑡 ) → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑢 ) ) ) = ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) )
34	33	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑢 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑢 ) ) ) = ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) )
35		ssun1	⊢ 𝐵 ⊆ ( 𝐵 ∪ 𝑡 )
36	35	sspwi	⊢ 𝒫 𝐵 ⊆ 𝒫 ( 𝐵 ∪ 𝑡 )
37	36 13	sselid	⊢ ( 𝜑 → 𝐵 ∈ 𝒫 ( 𝐵 ∪ 𝑡 ) )
38		vex	⊢ 𝑡 ∈ V
39	38	elpwun	⊢ ( 𝐵 ∈ 𝒫 ( 𝐵 ∪ 𝑡 ) ↔ ( 𝐵 ∖ 𝑡 ) ∈ 𝒫 𝐵 )
40	37 39	sylib	⊢ ( 𝜑 → ( 𝐵 ∖ 𝑡 ) ∈ 𝒫 𝐵 )
41	40	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑡 ) ∈ 𝒫 𝐵 )
42	3	difexd	⊢ ( 𝜑 → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) ∈ V )
43	42	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) ∈ V )
44	30 34 41 43	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) = ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) )
45	44	difeq2d	⊢ ( ( ( 𝜑 ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) ) )
46	45	adantlrl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) ) )
47		elpwi	⊢ ( 𝑡 ∈ 𝒫 𝐵 → 𝑡 ⊆ 𝐵 )
48		dfss4	⊢ ( 𝑡 ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) = 𝑡 )
49	47 48	sylib	⊢ ( 𝑡 ∈ 𝒫 𝐵 → ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) = 𝑡 )
50	49	fveq2d	⊢ ( 𝑡 ∈ 𝒫 𝐵 → ( 𝑓 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) = ( 𝑓 ‘ 𝑡 ) )
51	50	difeq2d	⊢ ( 𝑡 ∈ 𝒫 𝐵 → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) = ( 𝐵 ∖ ( 𝑓 ‘ 𝑡 ) ) )
52	51	difeq2d	⊢ ( 𝑡 ∈ 𝒫 𝐵 → ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) ) = ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑓 ‘ 𝑡 ) ) ) )
53	52	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) ) = ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑓 ‘ 𝑡 ) ) ) )
54	20 20	elmapd	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↔ 𝑓 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ) )
55	54	biimpa	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → 𝑓 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
56	55	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑓 ‘ 𝑡 ) ∈ 𝒫 𝐵 )
57	56	elpwid	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑓 ‘ 𝑡 ) ⊆ 𝐵 )
58		dfss4	⊢ ( ( 𝑓 ‘ 𝑡 ) ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑓 ‘ 𝑡 ) ) ) = ( 𝑓 ‘ 𝑡 ) )
59	57 58	sylib	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑓 ‘ 𝑡 ) ) ) = ( 𝑓 ‘ 𝑡 ) )
60	59	adantlrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑓 ‘ 𝑡 ) ) ) = ( 𝑓 ‘ 𝑡 ) )
61	46 53 60	3eqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑓 ‘ 𝑡 ) = ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
62	61	ralrimiva	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ) → ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑓 ‘ 𝑡 ) = ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
63		elmapfn	⊢ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝑓 Fn 𝒫 𝐵 )
64	63	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ) → 𝑓 Fn 𝒫 𝐵 )
65		difeq2	⊢ ( 𝑡 = 𝑧 → ( 𝐵 ∖ 𝑡 ) = ( 𝐵 ∖ 𝑧 ) )
66	65	fveq2d	⊢ ( 𝑡 = 𝑧 → ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) = ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) )
67	66	difeq2d	⊢ ( 𝑡 = 𝑧 → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) )
68	3	difexd	⊢ ( 𝜑 → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ∈ V )
69	68	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ∈ V )
70	3	difexd	⊢ ( 𝜑 → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ∈ V )
71	70	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ) ∧ 𝑧 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ∈ V )
72	64 67 69 71	fnmptfvd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ) → ( 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑓 ‘ 𝑡 ) = ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) )
73	62 72	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ) → 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) )
74	24 73	jca	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ) → ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) )
75		simpr	⊢ ( ( 𝜑 ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) → 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) )
76		difeq2	⊢ ( 𝑧 = 𝑡 → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ 𝑡 ) )
77	76	fveq2d	⊢ ( 𝑧 = 𝑡 → ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) = ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) )
78	77	difeq2d	⊢ ( 𝑧 = 𝑡 → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) = ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
79	78	cbvmptv	⊢ ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) = ( 𝑡 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
80	75 79	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) → 𝑓 = ( 𝑡 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) )
81		ssun1	⊢ 𝐵 ⊆ ( 𝐵 ∪ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) )
82	81	sspwi	⊢ 𝒫 𝐵 ⊆ 𝒫 ( 𝐵 ∪ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) )
83	82 13	sselid	⊢ ( 𝜑 → 𝐵 ∈ 𝒫 ( 𝐵 ∪ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
84		fvex	⊢ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ∈ V
85	84	elpwun	⊢ ( 𝐵 ∈ 𝒫 ( 𝐵 ∪ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ↔ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ∈ 𝒫 𝐵 )
86	83 85	sylib	⊢ ( 𝜑 → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ∈ 𝒫 𝐵 )
87	86	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ∈ 𝒫 𝐵 )
88	80 87	fmpt3d	⊢ ( ( 𝜑 ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) → 𝑓 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
89	20	adantr	⊢ ( ( 𝜑 ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) → 𝒫 𝐵 ∈ V )
90	89 89	elmapd	⊢ ( ( 𝜑 ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) → ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↔ 𝑓 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ) )
91	88 90	mpbird	⊢ ( ( 𝜑 ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) → 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
92	91	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ) → 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
93		simplr	⊢ ( ( ( 𝜑 ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) )
94		difeq2	⊢ ( 𝑧 = 𝑢 → ( 𝐵 ∖ 𝑧 ) = ( 𝐵 ∖ 𝑢 ) )
95	94	fveq2d	⊢ ( 𝑧 = 𝑢 → ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) = ( 𝑔 ‘ ( 𝐵 ∖ 𝑢 ) ) )
96	95	difeq2d	⊢ ( 𝑧 = 𝑢 → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) = ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑢 ) ) ) )
97	96	cbvmptv	⊢ ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) = ( 𝑢 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑢 ) ) ) )
98	93 97	eqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑓 = ( 𝑢 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑢 ) ) ) ) )
99	31	fveq2d	⊢ ( 𝑢 = ( 𝐵 ∖ 𝑡 ) → ( 𝑔 ‘ ( 𝐵 ∖ 𝑢 ) ) = ( 𝑔 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) )
100	99	difeq2d	⊢ ( 𝑢 = ( 𝐵 ∖ 𝑡 ) → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑢 ) ) ) = ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) )
101	100	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑢 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑢 ) ) ) = ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) )
102	40	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑡 ) ∈ 𝒫 𝐵 )
103	3	difexd	⊢ ( 𝜑 → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) ∈ V )
104	103	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) ∈ V )
105	98 101 102 104	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) = ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) )
106	105	difeq2d	⊢ ( ( ( 𝜑 ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) ) )
107	106	adantlrl	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) ) )
108	49	fveq2d	⊢ ( 𝑡 ∈ 𝒫 𝐵 → ( 𝑔 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) = ( 𝑔 ‘ 𝑡 ) )
109	108	difeq2d	⊢ ( 𝑡 ∈ 𝒫 𝐵 → ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) = ( 𝐵 ∖ ( 𝑔 ‘ 𝑡 ) ) )
110	109	difeq2d	⊢ ( 𝑡 ∈ 𝒫 𝐵 → ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) ) = ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑔 ‘ 𝑡 ) ) ) )
111	110	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) ) ) = ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑔 ‘ 𝑡 ) ) ) )
112	20 20	elmapd	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↔ 𝑔 : 𝒫 𝐵 ⟶ 𝒫 𝐵 ) )
113	112	biimpa	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → 𝑔 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
114	113	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑔 ‘ 𝑡 ) ∈ 𝒫 𝐵 )
115	114	elpwid	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑔 ‘ 𝑡 ) ⊆ 𝐵 )
116		dfss4	⊢ ( ( 𝑔 ‘ 𝑡 ) ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑔 ‘ 𝑡 ) )
117	115 116	sylib	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑔 ‘ 𝑡 ) )
118	117	adantlrr	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝐵 ∖ ( 𝑔 ‘ 𝑡 ) ) ) = ( 𝑔 ‘ 𝑡 ) )
119	107 111 118	3eqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑔 ‘ 𝑡 ) = ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
120	119	ralrimiva	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ) → ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑔 ‘ 𝑡 ) = ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) )
121		elmapfn	⊢ ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝑔 Fn 𝒫 𝐵 )
122	121	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ) → 𝑔 Fn 𝒫 𝐵 )
123		difeq2	⊢ ( 𝑡 = 𝑠 → ( 𝐵 ∖ 𝑡 ) = ( 𝐵 ∖ 𝑠 ) )
124	123	fveq2d	⊢ ( 𝑡 = 𝑠 → ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) = ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) )
125	124	difeq2d	⊢ ( 𝑡 = 𝑠 → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) = ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
126	3	difexd	⊢ ( 𝜑 → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ∈ V )
127	126	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ∈ V )
128	3	difexd	⊢ ( 𝜑 → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∈ V )
129	128	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ) ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∈ V )
130	122 125 127 129	fnmptfvd	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ) → ( 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑔 ‘ 𝑡 ) = ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑡 ) ) ) ) )
131	120 130	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ) → 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
132	92 131	jca	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ) → ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) )
133	74 132	impbida	⊢ ( 𝜑 → ( ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑔 = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) ↔ ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝑓 = ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) ) )
134	133	mptcnv	⊢ ( 𝜑 → ◡ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) = ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) )
135	1 2 3	dssmapfvd	⊢ ( 𝜑 → 𝐷 = ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) )
136	135	cnveqd	⊢ ( 𝜑 → ◡ 𝐷 = ◡ ( 𝑓 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑓 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) ) )
137		fveq1	⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) = ( 𝑔 ‘ ( 𝑏 ∖ 𝑠 ) ) )
138	137	difeq2d	⊢ ( 𝑓 = 𝑔 → ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) = ( 𝑏 ∖ ( 𝑔 ‘ ( 𝑏 ∖ 𝑠 ) ) ) )
139	138	mpteq2dv	⊢ ( 𝑓 = 𝑔 → ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) = ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑔 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) )
140		difeq2	⊢ ( 𝑠 = 𝑧 → ( 𝑏 ∖ 𝑠 ) = ( 𝑏 ∖ 𝑧 ) )
141	140	fveq2d	⊢ ( 𝑠 = 𝑧 → ( 𝑔 ‘ ( 𝑏 ∖ 𝑠 ) ) = ( 𝑔 ‘ ( 𝑏 ∖ 𝑧 ) ) )
142	141	difeq2d	⊢ ( 𝑠 = 𝑧 → ( 𝑏 ∖ ( 𝑔 ‘ ( 𝑏 ∖ 𝑠 ) ) ) = ( 𝑏 ∖ ( 𝑔 ‘ ( 𝑏 ∖ 𝑧 ) ) ) )
143	142	cbvmptv	⊢ ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑔 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) = ( 𝑧 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑔 ‘ ( 𝑏 ∖ 𝑧 ) ) ) )
144	139 143	eqtrdi	⊢ ( 𝑓 = 𝑔 → ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) = ( 𝑧 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑔 ‘ ( 𝑏 ∖ 𝑧 ) ) ) ) )
145	144	cbvmptv	⊢ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ↦ ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) ) = ( 𝑔 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ↦ ( 𝑧 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑔 ‘ ( 𝑏 ∖ 𝑧 ) ) ) ) )
146	145	mpteq2i	⊢ ( 𝑏 ∈ V ↦ ( 𝑓 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ↦ ( 𝑠 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑓 ‘ ( 𝑏 ∖ 𝑠 ) ) ) ) ) ) = ( 𝑏 ∈ V ↦ ( 𝑔 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ↦ ( 𝑧 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑔 ‘ ( 𝑏 ∖ 𝑧 ) ) ) ) ) )
147	1 146	eqtri	⊢ 𝑂 = ( 𝑏 ∈ V ↦ ( 𝑔 ∈ ( 𝒫 𝑏 ↑m 𝒫 𝑏 ) ↦ ( 𝑧 ∈ 𝒫 𝑏 ↦ ( 𝑏 ∖ ( 𝑔 ‘ ( 𝑏 ∖ 𝑧 ) ) ) ) ) )
148	147 2 3	dssmapfvd	⊢ ( 𝜑 → 𝐷 = ( 𝑔 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ↦ ( 𝑧 ∈ 𝒫 𝐵 ↦ ( 𝐵 ∖ ( 𝑔 ‘ ( 𝐵 ∖ 𝑧 ) ) ) ) ) )
149	134 136 148	3eqtr4d	⊢ ( 𝜑 → ◡ 𝐷 = 𝐷 )