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	$⊢ O = (b \in V ⟼ (f \in ({𝒫 b}^{𝒫 b}) ⟼ (s \in 𝒫 b ⟼ b ∖ f (b ∖ s))))$
	dssmapfvd.d	$⊢ D = O (B)$
	dssmapfvd.b	$⊢ φ \to B \in V$
Assertion	dssmapnvod	$⊢ φ \to D^{-1} = D$

Proof

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

Metamath Proof Explorer

Theorem dssmapnvod

Proof