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 44032

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 4068	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑡 → (𝐵 ∖ 𝑠) = (𝐵 ∖ 𝑡))
3	2	fveq2d 6821	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → (𝑓‘(𝐵 ∖ 𝑠)) = (𝑓‘(𝐵 ∖ 𝑡)))
4	3	difeq2d 4074	. . . . . . . . . 10 ⊢ (𝑠 = 𝑡 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))
5	4	cbvmptv 5193	. . . . . . . . 9 ⊢ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))
6	1, 5	eqtrdi 2781	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡)))))
7		ssun1 4126	. . . . . . . . . . . 12 ⊢ 𝐵 ⊆ (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡)))
8	7	sspwi 4560	. . . . . . . . . . 11 ⊢ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡)))
9		dssmapfvd.b	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
10		pwidg 4568	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ 𝒫 𝐵)
11	9, 10	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵)
12	8, 11	sselid 3930	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡))))
13		fvex 6830	. . . . . . . . . . 11 ⊢ (𝑓‘(𝐵 ∖ 𝑡)) ∈ V
14	13	elpwun 7697	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
15	12, 14	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
16	15	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
17	6, 16	fmpt3d 7044	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔:𝒫 𝐵⟶𝒫 𝐵)
18	9	pwexd 5315	. . . . . . . . 9 ⊢ (𝜑 → 𝒫 𝐵 ∈ V)
19	18	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝒫 𝐵 ∈ V)
20	19, 19	elmapd 8759	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵))
21	17, 20	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
22	21	adantrl 716	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
23		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))
24		difeq2 4068	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝑢 → (𝐵 ∖ 𝑠) = (𝐵 ∖ 𝑢))
25	24	fveq2d 6821	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑢 → (𝑓‘(𝐵 ∖ 𝑠)) = (𝑓‘(𝐵 ∖ 𝑢)))
26	25	difeq2d 4074	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑢 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))))
27	26	cbvmptv 5193	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))))
28	23, 27	eqtrdi 2781	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢)))))
29		difeq2 4068	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝐵 ∖ 𝑢) = (𝐵 ∖ (𝐵 ∖ 𝑡)))
30	29	fveq2d 6821	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝑓‘(𝐵 ∖ 𝑢)) = (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))
31	30	difeq2d 4074	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
32	31	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵 ∖ 𝑡)) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
33		ssun1 4126	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ⊆ (𝐵 ∪ 𝑡)
34	33	sspwi 4560	. . . . . . . . . . . . . 14 ⊢ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ 𝑡)
35	34, 11	sselid 3930	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ∈ 𝒫 (𝐵 ∪ 𝑡))
36		vex 3438	. . . . . . . . . . . . . 14 ⊢ 𝑡 ∈ V
37	36	elpwun 7697	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ 𝒫 (𝐵 ∪ 𝑡) ↔ (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
38	35, 37	sylib 218	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
39	38	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
40	9	difexd 5267	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V)
41	40	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V)
42	28, 32, 39, 41	fvmptd 6931	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘(𝐵 ∖ 𝑡)) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
43	42	difeq2d 4074	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))))
44	43	adantlrl 720	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))))
45		elpwi 4555	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ 𝒫 𝐵 → 𝑡 ⊆ 𝐵)
46		dfss4 4217	. . . . . . . . . . . . 13 ⊢ (𝑡 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑡)) = 𝑡)
47	45, 46	sylib 218	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑡)) = 𝑡)
48	47	fveq2d 6821	. . . . . . . . . . 11 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))) = (𝑓‘𝑡))
49	48	difeq2d 4074	. . . . . . . . . 10 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) = (𝐵 ∖ (𝑓‘𝑡)))
50	49	difeq2d 4074	. . . . . . . . 9 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))))
51	50	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))))
52	18, 18	elmapd 8759	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵))
53	52	biimpa 476	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) → 𝑓:𝒫 𝐵⟶𝒫 𝐵)
54	53	ffvelcdmda 7012	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘𝑡) ∈ 𝒫 𝐵)
55	54	elpwid 4557	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘𝑡) ⊆ 𝐵)
56		dfss4 4217	. . . . . . . . . 10 ⊢ ((𝑓‘𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))) = (𝑓‘𝑡))
57	55, 56	sylib 218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))) = (𝑓‘𝑡))
58	57	adantlrr 721	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))) = (𝑓‘𝑡))
59	44, 51, 58	3eqtrrd 2770	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘𝑡) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))
60	59	ralrimiva 3122	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑓‘𝑡) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))
61		elmapfn 8784	. . . . . . . 8 ⊢ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) → 𝑓 Fn 𝒫 𝐵)
62	61	ad2antrl 728	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → 𝑓 Fn 𝒫 𝐵)
63		difeq2 4068	. . . . . . . . 9 ⊢ (𝑡 = 𝑧 → (𝐵 ∖ 𝑡) = (𝐵 ∖ 𝑧))
64	63	fveq2d 6821	. . . . . . . 8 ⊢ (𝑡 = 𝑧 → (𝑔‘(𝐵 ∖ 𝑡)) = (𝑔‘(𝐵 ∖ 𝑧)))
65	64	difeq2d 4074	. . . . . . 7 ⊢ (𝑡 = 𝑧 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))
66	9	difexd 5267	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ V)
67	66	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ V)
68	9	difexd 5267	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) ∈ V)
69	68	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) ∈ V)
70	62, 65, 67, 69	fnmptfvd 6969	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → (𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑓‘𝑡) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡)))))
71	60, 70	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))
72	22, 71	jca 511	. . . 4 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))))
73		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))
74		difeq2 4068	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑡 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑡))
75	74	fveq2d 6821	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑡 → (𝑔‘(𝐵 ∖ 𝑧)) = (𝑔‘(𝐵 ∖ 𝑡)))
76	75	difeq2d 4074	. . . . . . . . . 10 ⊢ (𝑧 = 𝑡 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))
77	76	cbvmptv 5193	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))
78	73, 77	eqtrdi 2781	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡)))))
79		ssun1 4126	. . . . . . . . . . . 12 ⊢ 𝐵 ⊆ (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡)))
80	79	sspwi 4560	. . . . . . . . . . 11 ⊢ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡)))
81	80, 11	sselid 3930	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡))))
82		fvex 6830	. . . . . . . . . . 11 ⊢ (𝑔‘(𝐵 ∖ 𝑡)) ∈ V
83	82	elpwun 7697	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
84	81, 83	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
85	84	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵)
86	78, 85	fmpt3d 7044	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓:𝒫 𝐵⟶𝒫 𝐵)
87	18	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝒫 𝐵 ∈ V)
88	87, 87	elmapd 8759	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵))
89	86, 88	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
90	89	adantrl 716	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → 𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵))
91		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))
92		difeq2 4068	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑢 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑢))
93	92	fveq2d 6821	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑢 → (𝑔‘(𝐵 ∖ 𝑧)) = (𝑔‘(𝐵 ∖ 𝑢)))
94	93	difeq2d 4074	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑢 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))))
95	94	cbvmptv 5193	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))))
96	91, 95	eqtrdi 2781	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢)))))
97	29	fveq2d 6821	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝑔‘(𝐵 ∖ 𝑢)) = (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))
98	97	difeq2d 4074	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
99	98	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵 ∖ 𝑡)) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
100	38	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
101	9	difexd 5267	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V)
102	101	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V)
103	96, 99, 100, 102	fvmptd 6931	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘(𝐵 ∖ 𝑡)) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))
104	103	difeq2d 4074	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))))
105	104	adantlrl 720	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))))
106	47	fveq2d 6821	. . . . . . . . . . 11 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))) = (𝑔‘𝑡))
107	106	difeq2d 4074	. . . . . . . . . 10 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) = (𝐵 ∖ (𝑔‘𝑡)))
108	107	difeq2d 4074	. . . . . . . . 9 ⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))))
109	108	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))))
110	18, 18	elmapd 8759	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵))
111	110	biimpa 476	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) → 𝑔:𝒫 𝐵⟶𝒫 𝐵)
112	111	ffvelcdmda 7012	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘𝑡) ∈ 𝒫 𝐵)
113	112	elpwid 4557	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘𝑡) ⊆ 𝐵)
114		dfss4 4217	. . . . . . . . . 10 ⊢ ((𝑔‘𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))) = (𝑔‘𝑡))
115	113, 114	sylib 218	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))) = (𝑔‘𝑡))
116	115	adantlrr 721	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))) = (𝑔‘𝑡))
117	105, 109, 116	3eqtrrd 2770	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘𝑡) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))
118	117	ralrimiva 3122	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑔‘𝑡) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))
119		elmapfn 8784	. . . . . . . 8 ⊢ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) → 𝑔 Fn 𝒫 𝐵)
120	119	ad2antrl 728	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → 𝑔 Fn 𝒫 𝐵)
121		difeq2 4068	. . . . . . . . 9 ⊢ (𝑡 = 𝑠 → (𝐵 ∖ 𝑡) = (𝐵 ∖ 𝑠))
122	121	fveq2d 6821	. . . . . . . 8 ⊢ (𝑡 = 𝑠 → (𝑓‘(𝐵 ∖ 𝑡)) = (𝑓‘(𝐵 ∖ 𝑠)))
123	122	difeq2d 4074	. . . . . . 7 ⊢ (𝑡 = 𝑠 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))
124	9	difexd 5267	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ V)
125	124	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ V)
126	9	difexd 5267	. . . . . . . 8 ⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) ∈ V)
127	126	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) ∈ V)
128	120, 123, 125, 127	fnmptfvd 6969	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → (𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑔‘𝑡) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡)))))
129	118, 128	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))
130	90, 129	jca 511	. . . 4 ⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))))
131	72, 130	impbida 800	. . 3 ⊢ (𝜑 → ((𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ↔ (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))))
132	131	mptcnv 6083	. 2 ⊢ (𝜑 → ^◡(𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) = (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))))
133		dssmapfvd.o	. . . 4 ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))))
134		dssmapfvd.d	. . . 4 ⊢ 𝐷 = (𝑂‘𝐵)
135	133, 134, 9	dssmapfvd 44029	. . 3 ⊢ (𝜑 → 𝐷 = (𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))))
136	135	cnveqd 5813	. 2 ⊢ (𝜑 → ^◡𝐷 = ^◡(𝑓 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))))
137		fveq1 6816	. . . . . . . . 9 ⊢ (𝑓 = 𝑔 → (𝑓‘(𝑏 ∖ 𝑠)) = (𝑔‘(𝑏 ∖ 𝑠)))
138	137	difeq2d 4074	. . . . . . . 8 ⊢ (𝑓 = 𝑔 → (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))) = (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠))))
139	138	mpteq2dv 5183	. . . . . . 7 ⊢ (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))) = (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠)))))
140		difeq2 4068	. . . . . . . . . 10 ⊢ (𝑠 = 𝑧 → (𝑏 ∖ 𝑠) = (𝑏 ∖ 𝑧))
141	140	fveq2d 6821	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (𝑔‘(𝑏 ∖ 𝑠)) = (𝑔‘(𝑏 ∖ 𝑧)))
142	141	difeq2d 4074	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠))) = (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))
143	142	cbvmptv 5193	. . . . . . 7 ⊢ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))
144	139, 143	eqtrdi 2781	. . . . . 6 ⊢ (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧)))))
145	144	cbvmptv 5193	. . . . 5 ⊢ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))) = (𝑔 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧)))))
146	145	mpteq2i 5185	. . . 4 ⊢ (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))))) = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))))
147	133, 146	eqtri 2753	. . 3 ⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏 ↑_m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))))
148	147, 134, 9	dssmapfvd 44029	. 2 ⊢ (𝜑 → 𝐷 = (𝑔 ∈ (𝒫 𝐵 ↑_m 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))))
149	132, 136, 148	3eqtr4d 2775	1 ⊢ (𝜑 → ^◡𝐷 = 𝐷)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2110 ∀wral 3045 Vcvv 3434 ∖ cdif 3897 ∪ cun 3898 ⊆ wss 3900 𝒫 cpw 4548 ↦ cmpt 5170 ^◡ccnv 5613 Fn wfn 6472 ⟶wf 6473 ‘cfv 6477 (class class class)co 7341 ↑_m cmap 8745

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7663

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-reu 3345 df-rab 3394 df-v 3436 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-nul 4282 df-if 4474 df-pw 4550 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4858 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-id 5509 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-iota 6433 df-fun 6479 df-fn 6480 df-f 6481 df-f1 6482 df-fo 6483 df-f1o 6484 df-fv 6485 df-ov 7344 df-oprab 7345 df-mpo 7346 df-1st 7916 df-2nd 7917 df-map 8747

This theorem is referenced by: dssmapf1od 44033 dssmap2d 44034 ntrclsnvobr 44064 clsneicnv 44117 neicvgnvo 44127 dssmapclsntr 44141

W3C validator