dssmapnvod - Mathbox for Richard Penner

	Mathbox for Richard Penner		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dssmapnvod		Structured version Visualization version GIF version

Theorem dssmapnvod 44979

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

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

**Assertion**
Ref	Expression
dssmapnvod	⊢ (𝜑 → ^◡𝐷 = 𝐷)

Distinct variable groups: 𝐵,𝑏,𝑓,𝑠 𝜑,𝑏,𝑓,𝑠 Allowed substitution hints: 𝐷(𝑓, 𝑠, 𝑏) 𝑂(𝑓, 𝑠, 𝑏) 𝑉(𝑓, 𝑠, 𝑏)

Proof of Theorem dssmapnvod Dummy variables 𝑔 𝑧 𝑡 𝑢 are mutually distinct and distinct from all other variables.

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∀wral 3077 Vcvv 3451 ∖ cdif 3896 ∪ cun 3897 ⊆ wss 3899 𝒫 cpw 4557 ↦ cmpt 5186 ^◡ccnv 5650 Fn wfn 6526 ⟶wf 6527 ‘cfv 6531 (class class class)co 7412 ↑_m cmap 8831

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-ov 7415 df-oprab 7416 df-mpo 7417 df-1st 7990 df-2nd 7991 df-map 8833

This theorem is used by: dssmapf1od 44980 dssmap2d 44981 ntrclsnvobr 45011 clsneicnv 45064 neicvgnvo 45074 dssmapclsntr 45088

W3C validator