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 41517

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 4047	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (𝐵 ∖ 𝑠) = (𝐵 ∖ 𝑡))
3	2	fveq2d 6760	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → (𝑓‘(𝐵 ∖ 𝑠)) = (𝑓‘(𝐵 ∖ 𝑡)))
4	3	difeq2d 4053	. . . . . . . . . 10 ⊢ (𝑠 = 𝑡 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))
5	4	cbvmptv 5183	. . . . . . . . 9 ⊢ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))
6	1, 5	eqtrdi 2795	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡)))))
7		ssun1 4102	. . . . . . . . . . . 12 ⊢ 𝐵 ⊆ (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡)))
8	7	sspwi 4544	. . . . . . . . . . 11 ⊢ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡)))
9		dssmapfvd.b	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
10		pwidg 4552	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ 𝒫 𝐵)
11	9, 10	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵)
12	8, 11	sselid 3915	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡))))
13		fvex 6769	. . . . . . . . . . 11 ⊢ (𝑓‘(𝐵 ∖ 𝑡)) ∈ V
14	13	elpwun 7597	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
15	12, 14	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
16	15	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
17	6, 16	fmpt3d 6972	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔:𝒫 𝐵⟶𝒫 𝐵)
18	9	pwexd 5297	. . . . . . . . 9 ⊢ (𝜑 → 𝒫 𝐵 ∈ V)
19	18	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝒫 𝐵 ∈ V)
20	19, 19	elmapd 8587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵))
21	17, 20	mpbird 256	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
22	21	adantrl 712	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
23		simplr 765	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))
24		difeq2 4047	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝑢 → (𝐵 ∖ 𝑠) = (𝐵 ∖ 𝑢))
25	24	fveq2d 6760	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑢 → (𝑓‘(𝐵 ∖ 𝑠)) = (𝑓‘(𝐵 ∖ 𝑢)))
26	25	difeq2d 4053	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑢 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))))
27	26	cbvmptv 5183	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))))
28	23, 27	eqtrdi 2795	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢)))))
29		difeq2 4047	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝐵 ∖ 𝑢) = (𝐵 ∖ (𝐵 ∖ 𝑡)))
30	29	fveq2d 6760	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝑓‘(𝐵 ∖ 𝑢)) = (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))
31	30	difeq2d 4053	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
32	31	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵 ∖ 𝑡)) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
33		ssun1 4102	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ⊆ (𝐵 ∪ 𝑡)
34	33	sspwi 4544	. . . . . . . . . . . . . 14 ⊢ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ 𝑡)
35	34, 11	sselid 3915	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ 𝒫 (𝐵 ∪ 𝑡))
36		vex 3426	. . . . . . . . . . . . . 14 ⊢ 𝑡 ∈ V
37	36	elpwun 7597	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ 𝒫 (𝐵 ∪ 𝑡) ↔ (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
38	35, 37	sylib 217	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
39	38	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
40	9	difexd 5248	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V)
41	40	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V)
42	28, 32, 39, 41	fvmptd 6864	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘(𝐵 ∖ 𝑡)) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
43	42	difeq2d 4053	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))))
44	43	adantlrl 716	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))))
45		elpwi 4539	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝒫 𝐵 → 𝑡 ⊆ 𝐵)
46		dfss4 4189	. . . . . . . . . . . . 13 ⊢ (𝑡 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑡)) = 𝑡)
47	45, 46	sylib 217	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑡)) = 𝑡)
48	47	fveq2d 6760	. . . . . . . . . . 11 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))) = (𝑓‘𝑡))
49	48	difeq2d 4053	. . . . . . . . . 10 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) = (𝐵 ∖ (𝑓‘𝑡)))
50	49	difeq2d 4053	. . . . . . . . 9 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))))
51	50	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))))
52	18, 18	elmapd 8587	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵))
53	52	biimpa 476	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) → 𝑓:𝒫 𝐵⟶𝒫 𝐵)
54	53	ffvelrnda 6943	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘𝑡) ∈ 𝒫 𝐵)
55	54	elpwid 4541	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘𝑡) ⊆ 𝐵)
56		dfss4 4189	. . . . . . . . . 10 ⊢ ((𝑓‘𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))) = (𝑓‘𝑡))
57	55, 56	sylib 217	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))) = (𝑓‘𝑡))
58	57	adantlrr 717	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))) = (𝑓‘𝑡))
59	44, 51, 58	3eqtrrd 2783	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘𝑡) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))
60	59	ralrimiva 3107	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑓‘𝑡) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))
61		elmapfn 8611	. . . . . . . 8 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) → 𝑓 Fn 𝒫 𝐵)
62	61	ad2antrl 724	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → 𝑓 Fn 𝒫 𝐵)
63		difeq2 4047	. . . . . . . . 9 ⊢ (𝑡 = 𝑧 → (𝐵 ∖ 𝑡) = (𝐵 ∖ 𝑧))
64	63	fveq2d 6760	. . . . . . . 8 ⊢ (𝑡 = 𝑧 → (𝑔‘(𝐵 ∖ 𝑡)) = (𝑔‘(𝐵 ∖ 𝑧)))
65	64	difeq2d 4053	. . . . . . 7 ⊢ (𝑡 = 𝑧 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))
66	9	difexd 5248	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ V)
67	66	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ V)
68	9	difexd 5248	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) ∈ V)
69	68	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) ∈ V)
70	62, 65, 67, 69	fnmptfvd 6900	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → (𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑓‘𝑡) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡)))))
71	60, 70	mpbird 256	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))
72	22, 71	jca 511	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))))
73		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))
74		difeq2 4047	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑡 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑡))
75	74	fveq2d 6760	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑡 → (𝑔‘(𝐵 ∖ 𝑧)) = (𝑔‘(𝐵 ∖ 𝑡)))
76	75	difeq2d 4053	. . . . . . . . . 10 ⊢ (𝑧 = 𝑡 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))
77	76	cbvmptv 5183	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))
78	73, 77	eqtrdi 2795	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡)))))
79		ssun1 4102	. . . . . . . . . . . 12 ⊢ 𝐵 ⊆ (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡)))
80	79	sspwi 4544	. . . . . . . . . . 11 ⊢ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡)))
81	80, 11	sselid 3915	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡))))
82		fvex 6769	. . . . . . . . . . 11 ⊢ (𝑔‘(𝐵 ∖ 𝑡)) ∈ V
83	82	elpwun 7597	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
84	81, 83	sylib 217	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
85	84	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
86	78, 85	fmpt3d 6972	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓:𝒫 𝐵⟶𝒫 𝐵)
87	18	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝒫 𝐵 ∈ V)
88	87, 87	elmapd 8587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵))
89	86, 88	mpbird 256	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
90	89	adantrl 712	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
91		simplr 765	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))
92		difeq2 4047	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑢 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑢))
93	92	fveq2d 6760	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑢 → (𝑔‘(𝐵 ∖ 𝑧)) = (𝑔‘(𝐵 ∖ 𝑢)))
94	93	difeq2d 4053	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑢 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))))
95	94	cbvmptv 5183	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))))
96	91, 95	eqtrdi 2795	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢)))))
97	29	fveq2d 6760	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝑔‘(𝐵 ∖ 𝑢)) = (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))
98	97	difeq2d 4053	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
99	98	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵 ∖ 𝑡)) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
100	38	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
101	9	difexd 5248	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V)
102	101	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V)
103	96, 99, 100, 102	fvmptd 6864	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘(𝐵 ∖ 𝑡)) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
104	103	difeq2d 4053	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))))
105	104	adantlrl 716	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))))
106	47	fveq2d 6760	. . . . . . . . . . 11 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))) = (𝑔‘𝑡))
107	106	difeq2d 4053	. . . . . . . . . 10 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) = (𝐵 ∖ (𝑔‘𝑡)))
108	107	difeq2d 4053	. . . . . . . . 9 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))))
109	108	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))))
110	18, 18	elmapd 8587	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵))
111	110	biimpa 476	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) → 𝑔:𝒫 𝐵⟶𝒫 𝐵)
112	111	ffvelrnda 6943	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘𝑡) ∈ 𝒫 𝐵)
113	112	elpwid 4541	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘𝑡) ⊆ 𝐵)
114		dfss4 4189	. . . . . . . . . 10 ⊢ ((𝑔‘𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))) = (𝑔‘𝑡))
115	113, 114	sylib 217	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))) = (𝑔‘𝑡))
116	115	adantlrr 717	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))) = (𝑔‘𝑡))
117	105, 109, 116	3eqtrrd 2783	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘𝑡) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))
118	117	ralrimiva 3107	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑔‘𝑡) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))
119		elmapfn 8611	. . . . . . . 8 ⊢ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) → 𝑔 Fn 𝒫 𝐵)
120	119	ad2antrl 724	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → 𝑔 Fn 𝒫 𝐵)
121		difeq2 4047	. . . . . . . . 9 ⊢ (𝑡 = 𝑠 → (𝐵 ∖ 𝑡) = (𝐵 ∖ 𝑠))
122	121	fveq2d 6760	. . . . . . . 8 ⊢ (𝑡 = 𝑠 → (𝑓‘(𝐵 ∖ 𝑡)) = (𝑓‘(𝐵 ∖ 𝑠)))
123	122	difeq2d 4053	. . . . . . 7 ⊢ (𝑡 = 𝑠 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))
124	9	difexd 5248	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ V)
125	124	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ V)
126	9	difexd 5248	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) ∈ V)
127	126	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) ∈ V)
128	120, 123, 125, 127	fnmptfvd 6900	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → (𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑔‘𝑡) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡)))))
129	118, 128	mpbird 256	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))
130	90, 129	jca 511	. . . 4 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))))
131	72, 130	impbida 797	. . 3 ⊢ (𝜑 → ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ↔ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))))
132	131	mptcnv 6032	. 2 ⊢ (𝜑 → ^◡(𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) = (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))))
133		dssmapfvd.o	. . . 4 ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))
134		dssmapfvd.d	. . . 4 ⊢ 𝐷 = (𝑂‘𝐵)
135	133, 134, 9	dssmapfvd 41514	. . 3 ⊢ (𝜑 → 𝐷 = (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))))
136	135	cnveqd 5773	. 2 ⊢ (𝜑 → ^◡𝐷 = ^◡(𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))))
137		fveq1 6755	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑓‘(𝑏 ∖ 𝑠)) = (𝑔‘(𝑏 ∖ 𝑠)))
138	137	difeq2d 4053	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))) = (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠))))
139	138	mpteq2dv 5172	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))) = (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠)))))
140		difeq2 4047	. . . . . . . . . 10 ⊢ (𝑠 = 𝑧 → (𝑏 ∖ 𝑠) = (𝑏 ∖ 𝑧))
141	140	fveq2d 6760	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (𝑔‘(𝑏 ∖ 𝑠)) = (𝑔‘(𝑏 ∖ 𝑧)))
142	141	difeq2d 4053	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠))) = (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))
143	142	cbvmptv 5183	. . . . . . 7 ⊢ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))
144	139, 143	eqtrdi 2795	. . . . . 6 ⊢ (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧)))))
145	144	cbvmptv 5183	. . . . 5 ⊢ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))) = (𝑔 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧)))))
146	145	mpteq2i 5175	. . . 4 ⊢ (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))))) = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))))
147	133, 146	eqtri 2766	. . 3 ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))))
148	147, 134, 9	dssmapfvd 41514	. 2 ⊢ (𝜑 → 𝐷 = (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))))
149	132, 136, 148	3eqtr4d 2788	1 ⊢ (𝜑 → ^◡𝐷 = 𝐷)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ∀wral 3063 Vcvv 3422 ∖ cdif 3880 ∪ cun 3881 ⊆ wss 3883 𝒫 cpw 4530 ↦ cmpt 5153 ^◡ccnv 5579 Fn wfn 6413 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 ↑_m cmap 8573

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-reu 3070 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-ov 7258 df-oprab 7259 df-mpo 7260 df-1st 7804 df-2nd 7805 df-map 8575

This theorem is referenced by: dssmapf1od 41518 dssmap2d 41519 ntrclsnvobr 41551 clsneicnv 41604 neicvgnvo 41614 dssmapclsntr 41628

W3C validator