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 44033

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 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))
2		difeq2 4120	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (𝐵 ∖ 𝑠) = (𝐵 ∖ 𝑡))
3	2	fveq2d 6910	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → (𝑓‘(𝐵 ∖ 𝑠)) = (𝑓‘(𝐵 ∖ 𝑡)))
4	3	difeq2d 4126	. . . . . . . . . 10 ⊢ (𝑠 = 𝑡 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))
5	4	cbvmptv 5255	. . . . . . . . 9 ⊢ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))
6	1, 5	eqtrdi 2793	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡)))))
7		ssun1 4178	. . . . . . . . . . . 12 ⊢ 𝐵 ⊆ (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡)))
8	7	sspwi 4612	. . . . . . . . . . 11 ⊢ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡)))
9		dssmapfvd.b	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
10		pwidg 4620	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ 𝒫 𝐵)
11	9, 10	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵)
12	8, 11	sselid 3981	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡))))
13		fvex 6919	. . . . . . . . . . 11 ⊢ (𝑓‘(𝐵 ∖ 𝑡)) ∈ V
14	13	elpwun 7789	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
15	12, 14	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
16	15	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
17	6, 16	fmpt3d 7136	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔:𝒫 𝐵⟶𝒫 𝐵)
18	9	pwexd 5379	. . . . . . . . 9 ⊢ (𝜑 → 𝒫 𝐵 ∈ V)
19	18	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝒫 𝐵 ∈ V)
20	19, 19	elmapd 8880	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵))
21	17, 20	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
22	21	adantrl 716	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
23		simplr 769	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))
24		difeq2 4120	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝑢 → (𝐵 ∖ 𝑠) = (𝐵 ∖ 𝑢))
25	24	fveq2d 6910	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑢 → (𝑓‘(𝐵 ∖ 𝑠)) = (𝑓‘(𝐵 ∖ 𝑢)))
26	25	difeq2d 4126	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑢 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))))
27	26	cbvmptv 5255	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))))
28	23, 27	eqtrdi 2793	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢)))))
29		difeq2 4120	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝐵 ∖ 𝑢) = (𝐵 ∖ (𝐵 ∖ 𝑡)))
30	29	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝑓‘(𝐵 ∖ 𝑢)) = (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))
31	30	difeq2d 4126	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
32	31	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵 ∖ 𝑡)) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
33		ssun1 4178	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ⊆ (𝐵 ∪ 𝑡)
34	33	sspwi 4612	. . . . . . . . . . . . . 14 ⊢ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ 𝑡)
35	34, 11	sselid 3981	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ 𝒫 (𝐵 ∪ 𝑡))
36		vex 3484	. . . . . . . . . . . . . 14 ⊢ 𝑡 ∈ V
37	36	elpwun 7789	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ 𝒫 (𝐵 ∪ 𝑡) ↔ (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
38	35, 37	sylib 218	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
39	38	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
40	9	difexd 5331	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V)
41	40	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V)
42	28, 32, 39, 41	fvmptd 7023	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘(𝐵 ∖ 𝑡)) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
43	42	difeq2d 4126	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))))
44	43	adantlrl 720	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))))
45		elpwi 4607	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝒫 𝐵 → 𝑡 ⊆ 𝐵)
46		dfss4 4269	. . . . . . . . . . . . 13 ⊢ (𝑡 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑡)) = 𝑡)
47	45, 46	sylib 218	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑡)) = 𝑡)
48	47	fveq2d 6910	. . . . . . . . . . 11 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))) = (𝑓‘𝑡))
49	48	difeq2d 4126	. . . . . . . . . 10 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) = (𝐵 ∖ (𝑓‘𝑡)))
50	49	difeq2d 4126	. . . . . . . . 9 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))))
51	50	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))))
52	18, 18	elmapd 8880	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵))
53	52	biimpa 476	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) → 𝑓:𝒫 𝐵⟶𝒫 𝐵)
54	53	ffvelcdmda 7104	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘𝑡) ∈ 𝒫 𝐵)
55	54	elpwid 4609	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘𝑡) ⊆ 𝐵)
56		dfss4 4269	. . . . . . . . . 10 ⊢ ((𝑓‘𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))) = (𝑓‘𝑡))
57	55, 56	sylib 218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))) = (𝑓‘𝑡))
58	57	adantlrr 721	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))) = (𝑓‘𝑡))
59	44, 51, 58	3eqtrrd 2782	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘𝑡) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))
60	59	ralrimiva 3146	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑓‘𝑡) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))
61		elmapfn 8905	. . . . . . . 8 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) → 𝑓 Fn 𝒫 𝐵)
62	61	ad2antrl 728	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → 𝑓 Fn 𝒫 𝐵)
63		difeq2 4120	. . . . . . . . 9 ⊢ (𝑡 = 𝑧 → (𝐵 ∖ 𝑡) = (𝐵 ∖ 𝑧))
64	63	fveq2d 6910	. . . . . . . 8 ⊢ (𝑡 = 𝑧 → (𝑔‘(𝐵 ∖ 𝑡)) = (𝑔‘(𝐵 ∖ 𝑧)))
65	64	difeq2d 4126	. . . . . . 7 ⊢ (𝑡 = 𝑧 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))
66	9	difexd 5331	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ V)
67	66	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ V)
68	9	difexd 5331	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) ∈ V)
69	68	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) ∈ V)
70	62, 65, 67, 69	fnmptfvd 7061	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → (𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑓‘𝑡) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡)))))
71	60, 70	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))
72	22, 71	jca 511	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))))
73		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))
74		difeq2 4120	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑡 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑡))
75	74	fveq2d 6910	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑡 → (𝑔‘(𝐵 ∖ 𝑧)) = (𝑔‘(𝐵 ∖ 𝑡)))
76	75	difeq2d 4126	. . . . . . . . . 10 ⊢ (𝑧 = 𝑡 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))
77	76	cbvmptv 5255	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))
78	73, 77	eqtrdi 2793	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡)))))
79		ssun1 4178	. . . . . . . . . . . 12 ⊢ 𝐵 ⊆ (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡)))
80	79	sspwi 4612	. . . . . . . . . . 11 ⊢ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡)))
81	80, 11	sselid 3981	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡))))
82		fvex 6919	. . . . . . . . . . 11 ⊢ (𝑔‘(𝐵 ∖ 𝑡)) ∈ V
83	82	elpwun 7789	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
84	81, 83	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
85	84	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
86	78, 85	fmpt3d 7136	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓:𝒫 𝐵⟶𝒫 𝐵)
87	18	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝒫 𝐵 ∈ V)
88	87, 87	elmapd 8880	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵))
89	86, 88	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
90	89	adantrl 716	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
91		simplr 769	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))
92		difeq2 4120	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑢 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑢))
93	92	fveq2d 6910	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑢 → (𝑔‘(𝐵 ∖ 𝑧)) = (𝑔‘(𝐵 ∖ 𝑢)))
94	93	difeq2d 4126	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑢 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))))
95	94	cbvmptv 5255	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))))
96	91, 95	eqtrdi 2793	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢)))))
97	29	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝑔‘(𝐵 ∖ 𝑢)) = (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))
98	97	difeq2d 4126	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
99	98	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵 ∖ 𝑡)) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
100	38	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
101	9	difexd 5331	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V)
102	101	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V)
103	96, 99, 100, 102	fvmptd 7023	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘(𝐵 ∖ 𝑡)) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
104	103	difeq2d 4126	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))))
105	104	adantlrl 720	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))))
106	47	fveq2d 6910	. . . . . . . . . . 11 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))) = (𝑔‘𝑡))
107	106	difeq2d 4126	. . . . . . . . . 10 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) = (𝐵 ∖ (𝑔‘𝑡)))
108	107	difeq2d 4126	. . . . . . . . 9 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))))
109	108	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))))
110	18, 18	elmapd 8880	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵))
111	110	biimpa 476	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) → 𝑔:𝒫 𝐵⟶𝒫 𝐵)
112	111	ffvelcdmda 7104	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘𝑡) ∈ 𝒫 𝐵)
113	112	elpwid 4609	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘𝑡) ⊆ 𝐵)
114		dfss4 4269	. . . . . . . . . 10 ⊢ ((𝑔‘𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))) = (𝑔‘𝑡))
115	113, 114	sylib 218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))) = (𝑔‘𝑡))
116	115	adantlrr 721	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))) = (𝑔‘𝑡))
117	105, 109, 116	3eqtrrd 2782	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘𝑡) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))
118	117	ralrimiva 3146	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑔‘𝑡) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))
119		elmapfn 8905	. . . . . . . 8 ⊢ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) → 𝑔 Fn 𝒫 𝐵)
120	119	ad2antrl 728	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → 𝑔 Fn 𝒫 𝐵)
121		difeq2 4120	. . . . . . . . 9 ⊢ (𝑡 = 𝑠 → (𝐵 ∖ 𝑡) = (𝐵 ∖ 𝑠))
122	121	fveq2d 6910	. . . . . . . 8 ⊢ (𝑡 = 𝑠 → (𝑓‘(𝐵 ∖ 𝑡)) = (𝑓‘(𝐵 ∖ 𝑠)))
123	122	difeq2d 4126	. . . . . . 7 ⊢ (𝑡 = 𝑠 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))
124	9	difexd 5331	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ V)
125	124	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ V)
126	9	difexd 5331	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) ∈ V)
127	126	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) ∈ V)
128	120, 123, 125, 127	fnmptfvd 7061	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → (𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑔‘𝑡) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡)))))
129	118, 128	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))
130	90, 129	jca 511	. . . 4 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))))
131	72, 130	impbida 801	. . 3 ⊢ (𝜑 → ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ↔ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))))
132	131	mptcnv 6159	. 2 ⊢ (𝜑 → ^◡(𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) = (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))))
133		dssmapfvd.o	. . . 4 ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))
134		dssmapfvd.d	. . . 4 ⊢ 𝐷 = (𝑂‘𝐵)
135	133, 134, 9	dssmapfvd 44030	. . 3 ⊢ (𝜑 → 𝐷 = (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))))
136	135	cnveqd 5886	. 2 ⊢ (𝜑 → ^◡𝐷 = ^◡(𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))))
137		fveq1 6905	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑓‘(𝑏 ∖ 𝑠)) = (𝑔‘(𝑏 ∖ 𝑠)))
138	137	difeq2d 4126	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))) = (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠))))
139	138	mpteq2dv 5244	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))) = (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠)))))
140		difeq2 4120	. . . . . . . . . 10 ⊢ (𝑠 = 𝑧 → (𝑏 ∖ 𝑠) = (𝑏 ∖ 𝑧))
141	140	fveq2d 6910	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (𝑔‘(𝑏 ∖ 𝑠)) = (𝑔‘(𝑏 ∖ 𝑧)))
142	141	difeq2d 4126	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠))) = (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))
143	142	cbvmptv 5255	. . . . . . 7 ⊢ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))
144	139, 143	eqtrdi 2793	. . . . . 6 ⊢ (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧)))))
145	144	cbvmptv 5255	. . . . 5 ⊢ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))) = (𝑔 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧)))))
146	145	mpteq2i 5247	. . . 4 ⊢ (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))))) = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))))
147	133, 146	eqtri 2765	. . 3 ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))))
148	147, 134, 9	dssmapfvd 44030	. 2 ⊢ (𝜑 → 𝐷 = (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))))
149	132, 136, 148	3eqtr4d 2787	1 ⊢ (𝜑 → ^◡𝐷 = 𝐷)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ∀wral 3061 Vcvv 3480 ∖ cdif 3948 ∪ cun 3949 ⊆ wss 3951 𝒫 cpw 4600 ↦ cmpt 5225 ^◡ccnv 5684 Fn wfn 6556 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 ↑_m cmap 8866

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-ov 7434 df-oprab 7435 df-mpo 7436 df-1st 8014 df-2nd 8015 df-map 8868

This theorem is referenced by: dssmapf1od 44034 dssmap2d 44035 ntrclsnvobr 44065 clsneicnv 44118 neicvgnvo 44128 dssmapclsntr 44142

W3C validator