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	sseldi	$⊢ φ \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	sseldi	$⊢ φ \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		difexg	$⊢ B \in V \to B ∖ f (B ∖ (B ∖ t)) \in V$
43	3 42	syl	$⊢ φ \to B ∖ f (B ∖ (B ∖ t)) \in V$
44	43	ad2antrr	$⊢ ((φ \land g = (s \in 𝒫 B ⟼ B ∖ f (B ∖ s))) \land t \in 𝒫 B) \to B ∖ f (B ∖ (B ∖ t)) \in V$
45	30 34 41 44	fvmptd	$⊢ ((φ \land g = (s \in 𝒫 B ⟼ B ∖ f (B ∖ s))) \land t \in 𝒫 B) \to g (B ∖ t) = B ∖ f (B ∖ (B ∖ t))$
46	45	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)))$
47	46	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)))$
48		elpwi	$⊢ t \in 𝒫 B \to t \subseteq B$
49		dfss4	$⊢ t \subseteq B \leftrightarrow B ∖ (B ∖ t) = t$
50	48 49	sylib	$⊢ t \in 𝒫 B \to B ∖ (B ∖ t) = t$
51	50	fveq2d	$⊢ t \in 𝒫 B \to f (B ∖ (B ∖ t)) = f (t)$
52	51	difeq2d	$⊢ t \in 𝒫 B \to B ∖ f (B ∖ (B ∖ t)) = B ∖ f (t)$
53	52	difeq2d	$⊢ t \in 𝒫 B \to B ∖ (B ∖ f (B ∖ (B ∖ t))) = B ∖ (B ∖ f (t))$
54	53	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))$
55	20 20	elmapd	$⊢ φ \to (f \in ({𝒫 B}^{𝒫 B}) \leftrightarrow f : 𝒫 B ⟶ 𝒫 B)$
56	55	biimpa	$⊢ (φ \land f \in ({𝒫 B}^{𝒫 B})) \to f : 𝒫 B ⟶ 𝒫 B$
57	56	ffvelrnda	$⊢ ((φ \land f \in ({𝒫 B}^{𝒫 B})) \land t \in 𝒫 B) \to f (t) \in 𝒫 B$
58	57	elpwid	$⊢ ((φ \land f \in ({𝒫 B}^{𝒫 B})) \land t \in 𝒫 B) \to f (t) \subseteq B$
59		dfss4	$⊢ f (t) \subseteq B \leftrightarrow B ∖ (B ∖ f (t)) = f (t)$
60	58 59	sylib	$⊢ ((φ \land f \in ({𝒫 B}^{𝒫 B})) \land t \in 𝒫 B) \to B ∖ (B ∖ f (t)) = f (t)$
61	60	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)$
62	47 54 61	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)$
63	62	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)$
64		elmapfn	$⊢ f \in ({𝒫 B}^{𝒫 B}) \to f Fn 𝒫 B$
65	64	ad2antrl	$⊢ (φ \land (f \in ({𝒫 B}^{𝒫 B}) \land g = (s \in 𝒫 B ⟼ B ∖ f (B ∖ s)))) \to f Fn 𝒫 B$
66		difeq2	$⊢ t = z \to B ∖ t = B ∖ z$
67	66	fveq2d	$⊢ t = z \to g (B ∖ t) = g (B ∖ z)$
68	67	difeq2d	$⊢ t = z \to B ∖ g (B ∖ t) = B ∖ g (B ∖ z)$
69		difexg	$⊢ B \in V \to B ∖ g (B ∖ t) \in V$
70	3 69	syl	$⊢ φ \to B ∖ g (B ∖ t) \in V$
71	70	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$
72		difexg	$⊢ B \in V \to B ∖ g (B ∖ z) \in V$
73	3 72	syl	$⊢ φ \to B ∖ g (B ∖ z) \in V$
74	73	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$
75	65 68 71 74	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))$
76	63 75	mpbird	$⊢ (φ \land (f \in ({𝒫 B}^{𝒫 B}) \land g = (s \in 𝒫 B ⟼ B ∖ f (B ∖ s)))) \to f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z))$
77	24 76	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)))$
78		simpr	$⊢ (φ \land f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z))) \to f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z))$
79		difeq2	$⊢ z = t \to B ∖ z = B ∖ t$
80	79	fveq2d	$⊢ z = t \to g (B ∖ z) = g (B ∖ t)$
81	80	difeq2d	$⊢ z = t \to B ∖ g (B ∖ z) = B ∖ g (B ∖ t)$
82	81	cbvmptv	$⊢ (z \in 𝒫 B ⟼ B ∖ g (B ∖ z)) = (t \in 𝒫 B ⟼ B ∖ g (B ∖ t))$
83	78 82	eqtrdi	$⊢ (φ \land f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z))) \to f = (t \in 𝒫 B ⟼ B ∖ g (B ∖ t))$
84		ssun1	$⊢ B \subseteq B \cup g (B ∖ t)$
85	84	sspwi	$⊢ 𝒫 B \subseteq 𝒫 (B \cup g (B ∖ t))$
86	85 13	sseldi	$⊢ φ \to B \in 𝒫 (B \cup g (B ∖ t))$
87		fvex	$⊢ g (B ∖ t) \in V$
88	87	elpwun	$⊢ B \in 𝒫 (B \cup g (B ∖ t)) \leftrightarrow B ∖ g (B ∖ t) \in 𝒫 B$
89	86 88	sylib	$⊢ φ \to B ∖ g (B ∖ t) \in 𝒫 B$
90	89	ad2antrr	$⊢ ((φ \land f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z))) \land t \in 𝒫 B) \to B ∖ g (B ∖ t) \in 𝒫 B$
91	83 90	fmpt3d	$⊢ (φ \land f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z))) \to f : 𝒫 B ⟶ 𝒫 B$
92	20	adantr	$⊢ (φ \land f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z))) \to 𝒫 B \in V$
93	92 92	elmapd	$⊢ (φ \land f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z))) \to (f \in ({𝒫 B}^{𝒫 B}) \leftrightarrow f : 𝒫 B ⟶ 𝒫 B)$
94	91 93	mpbird	$⊢ (φ \land f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z))) \to f \in ({𝒫 B}^{𝒫 B})$
95	94	adantrl	$⊢ (φ \land (g \in ({𝒫 B}^{𝒫 B}) \land f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z)))) \to f \in ({𝒫 B}^{𝒫 B})$
96		simplr	$⊢ ((φ \land f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z))) \land t \in 𝒫 B) \to f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z))$
97		difeq2	$⊢ z = u \to B ∖ z = B ∖ u$
98	97	fveq2d	$⊢ z = u \to g (B ∖ z) = g (B ∖ u)$
99	98	difeq2d	$⊢ z = u \to B ∖ g (B ∖ z) = B ∖ g (B ∖ u)$
100	99	cbvmptv	$⊢ (z \in 𝒫 B ⟼ B ∖ g (B ∖ z)) = (u \in 𝒫 B ⟼ B ∖ g (B ∖ u))$
101	96 100	eqtrdi	$⊢ ((φ \land f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z))) \land t \in 𝒫 B) \to f = (u \in 𝒫 B ⟼ B ∖ g (B ∖ u))$
102	31	fveq2d	$⊢ u = B ∖ t \to g (B ∖ u) = g (B ∖ (B ∖ t))$
103	102	difeq2d	$⊢ u = B ∖ t \to B ∖ g (B ∖ u) = B ∖ g (B ∖ (B ∖ t))$
104	103	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))$
105	40	ad2antrr	$⊢ ((φ \land f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z))) \land t \in 𝒫 B) \to B ∖ t \in 𝒫 B$
106		difexg	$⊢ B \in V \to B ∖ g (B ∖ (B ∖ t)) \in V$
107	3 106	syl	$⊢ φ \to B ∖ g (B ∖ (B ∖ t)) \in V$
108	107	ad2antrr	$⊢ ((φ \land f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z))) \land t \in 𝒫 B) \to B ∖ g (B ∖ (B ∖ t)) \in V$
109	101 104 105 108	fvmptd	$⊢ ((φ \land f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z))) \land t \in 𝒫 B) \to f (B ∖ t) = B ∖ g (B ∖ (B ∖ t))$
110	109	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)))$
111	110	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)))$
112	50	fveq2d	$⊢ t \in 𝒫 B \to g (B ∖ (B ∖ t)) = g (t)$
113	112	difeq2d	$⊢ t \in 𝒫 B \to B ∖ g (B ∖ (B ∖ t)) = B ∖ g (t)$
114	113	difeq2d	$⊢ t \in 𝒫 B \to B ∖ (B ∖ g (B ∖ (B ∖ t))) = B ∖ (B ∖ g (t))$
115	114	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))$
116	20 20	elmapd	$⊢ φ \to (g \in ({𝒫 B}^{𝒫 B}) \leftrightarrow g : 𝒫 B ⟶ 𝒫 B)$
117	116	biimpa	$⊢ (φ \land g \in ({𝒫 B}^{𝒫 B})) \to g : 𝒫 B ⟶ 𝒫 B$
118	117	ffvelrnda	$⊢ ((φ \land g \in ({𝒫 B}^{𝒫 B})) \land t \in 𝒫 B) \to g (t) \in 𝒫 B$
119	118	elpwid	$⊢ ((φ \land g \in ({𝒫 B}^{𝒫 B})) \land t \in 𝒫 B) \to g (t) \subseteq B$
120		dfss4	$⊢ g (t) \subseteq B \leftrightarrow B ∖ (B ∖ g (t)) = g (t)$
121	119 120	sylib	$⊢ ((φ \land g \in ({𝒫 B}^{𝒫 B})) \land t \in 𝒫 B) \to B ∖ (B ∖ g (t)) = g (t)$
122	121	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)$
123	111 115 122	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)$
124	123	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)$
125		elmapfn	$⊢ g \in ({𝒫 B}^{𝒫 B}) \to g Fn 𝒫 B$
126	125	ad2antrl	$⊢ (φ \land (g \in ({𝒫 B}^{𝒫 B}) \land f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z)))) \to g Fn 𝒫 B$
127		difeq2	$⊢ t = s \to B ∖ t = B ∖ s$
128	127	fveq2d	$⊢ t = s \to f (B ∖ t) = f (B ∖ s)$
129	128	difeq2d	$⊢ t = s \to B ∖ f (B ∖ t) = B ∖ f (B ∖ s)$
130		difexg	$⊢ B \in V \to B ∖ f (B ∖ t) \in V$
131	3 130	syl	$⊢ φ \to B ∖ f (B ∖ t) \in V$
132	131	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$
133		difexg	$⊢ B \in V \to B ∖ f (B ∖ s) \in V$
134	3 133	syl	$⊢ φ \to B ∖ f (B ∖ s) \in V$
135	134	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$
136	126 129 132 135	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))$
137	124 136	mpbird	$⊢ (φ \land (g \in ({𝒫 B}^{𝒫 B}) \land f = (z \in 𝒫 B ⟼ B ∖ g (B ∖ z)))) \to g = (s \in 𝒫 B ⟼ B ∖ f (B ∖ s))$
138	95 137	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)))$
139	77 138	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))))$
140	139	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)))$
141	1 2 3	dssmapfvd	$⊢ φ \to D = (f \in ({𝒫 B}^{𝒫 B}) ⟼ (s \in 𝒫 B ⟼ B ∖ f (B ∖ s)))$
142	141	cnveqd	$⊢ φ \to D^{-1} = {(f \in ({𝒫 B}^{𝒫 B}) ⟼ (s \in 𝒫 B ⟼ B ∖ f (B ∖ s)))}^{-1}$
143		fveq1	$⊢ f = g \to f (b ∖ s) = g (b ∖ s)$
144	143	difeq2d	$⊢ f = g \to b ∖ f (b ∖ s) = b ∖ g (b ∖ s)$
145	144	mpteq2dv	$⊢ f = g \to (s \in 𝒫 b ⟼ b ∖ f (b ∖ s)) = (s \in 𝒫 b ⟼ b ∖ g (b ∖ s))$
146		difeq2	$⊢ s = z \to b ∖ s = b ∖ z$
147	146	fveq2d	$⊢ s = z \to g (b ∖ s) = g (b ∖ z)$
148	147	difeq2d	$⊢ s = z \to b ∖ g (b ∖ s) = b ∖ g (b ∖ z)$
149	148	cbvmptv	$⊢ (s \in 𝒫 b ⟼ b ∖ g (b ∖ s)) = (z \in 𝒫 b ⟼ b ∖ g (b ∖ z))$
150	145 149	eqtrdi	$⊢ f = g \to (s \in 𝒫 b ⟼ b ∖ f (b ∖ s)) = (z \in 𝒫 b ⟼ b ∖ g (b ∖ z))$
151	150	cbvmptv	$⊢ (f \in ({𝒫 b}^{𝒫 b}) ⟼ (s \in 𝒫 b ⟼ b ∖ f (b ∖ s))) = (g \in ({𝒫 b}^{𝒫 b}) ⟼ (z \in 𝒫 b ⟼ b ∖ g (b ∖ z)))$
152	151	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))))$
153	1 152	eqtri	$⊢ O = (b \in V ⟼ (g \in ({𝒫 b}^{𝒫 b}) ⟼ (z \in 𝒫 b ⟼ b ∖ g (b ∖ z))))$
154	153 2 3	dssmapfvd	$⊢ φ \to D = (g \in ({𝒫 B}^{𝒫 B}) ⟼ (z \in 𝒫 B ⟼ B ∖ g (B ∖ z)))$
155	140 142 154	3eqtr4d	$⊢ φ \to D^{-1} = D$

Metamath Proof Explorer

Theorem dssmapnvod

Proof