Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dssmapnvod Structured version   Visualization version   GIF version
Theorem dssmapnvod 42757
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.
StepHypRef Expression
1 simpr 486 . . . . . . . . 9 ((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) β†’ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))
2 difeq2 4116 . . . . . . . . . . . 12 (𝑠 = 𝑑 β†’ (𝐡 βˆ– 𝑠) = (𝐡 βˆ– 𝑑))
32fveq2d 6893 . . . . . . . . . . 11 (𝑠 = 𝑑 β†’ (π‘“β€˜(𝐡 βˆ– 𝑠)) = (π‘“β€˜(𝐡 βˆ– 𝑑)))
43difeq2d 4122 . . . . . . . . . 10 (𝑠 = 𝑑 β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))))
54cbvmptv 5261 . . . . . . . . 9 (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))) = (𝑑 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))))
61, 5eqtrdi 2789 . . . . . . . 8 ((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) β†’ 𝑔 = (𝑑 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑)))))
7 ssun1 4172 . . . . . . . . . . . 12 𝐡 βŠ† (𝐡 βˆͺ (π‘“β€˜(𝐡 βˆ– 𝑑)))
87sspwi 4614 . . . . . . . . . . 11 𝒫 𝐡 βŠ† 𝒫 (𝐡 βˆͺ (π‘“β€˜(𝐡 βˆ– 𝑑)))
9 dssmapfvd.b . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ 𝑉)
10 pwidg 4622 . . . . . . . . . . . 12 (𝐡 ∈ 𝑉 β†’ 𝐡 ∈ 𝒫 𝐡)
119, 10syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ∈ 𝒫 𝐡)
128, 11sselid 3980 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ 𝒫 (𝐡 βˆͺ (π‘“β€˜(𝐡 βˆ– 𝑑))))
13 fvex 6902 . . . . . . . . . . 11 (π‘“β€˜(𝐡 βˆ– 𝑑)) ∈ V
1413elpwun 7753 . . . . . . . . . 10 (𝐡 ∈ 𝒫 (𝐡 βˆͺ (π‘“β€˜(𝐡 βˆ– 𝑑))) ↔ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) ∈ 𝒫 𝐡)
1512, 14sylib 217 . . . . . . . . 9 (πœ‘ β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) ∈ 𝒫 𝐡)
1615ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) ∈ 𝒫 𝐡)
176, 16fmpt3d 7113 . . . . . . 7 ((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) β†’ 𝑔:𝒫 π΅βŸΆπ’« 𝐡)
189pwexd 5377 . . . . . . . . 9 (πœ‘ β†’ 𝒫 𝐡 ∈ V)
1918adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) β†’ 𝒫 𝐡 ∈ V)
2019, 19elmapd 8831 . . . . . . 7 ((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) β†’ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↔ 𝑔:𝒫 π΅βŸΆπ’« 𝐡))
2117, 20mpbird 257 . . . . . 6 ((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) β†’ 𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡))
2221adantrl 715 . . . . 5 ((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) β†’ 𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡))
23 simplr 768 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))
24 difeq2 4116 . . . . . . . . . . . . . . 15 (𝑠 = 𝑒 β†’ (𝐡 βˆ– 𝑠) = (𝐡 βˆ– 𝑒))
2524fveq2d 6893 . . . . . . . . . . . . . 14 (𝑠 = 𝑒 β†’ (π‘“β€˜(𝐡 βˆ– 𝑠)) = (π‘“β€˜(𝐡 βˆ– 𝑒)))
2625difeq2d 4122 . . . . . . . . . . . . 13 (𝑠 = 𝑒 β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑒))))
2726cbvmptv 5261 . . . . . . . . . . . 12 (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))) = (𝑒 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑒))))
2823, 27eqtrdi 2789 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ 𝑔 = (𝑒 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑒)))))
29 difeq2 4116 . . . . . . . . . . . . . 14 (𝑒 = (𝐡 βˆ– 𝑑) β†’ (𝐡 βˆ– 𝑒) = (𝐡 βˆ– (𝐡 βˆ– 𝑑)))
3029fveq2d 6893 . . . . . . . . . . . . 13 (𝑒 = (𝐡 βˆ– 𝑑) β†’ (π‘“β€˜(𝐡 βˆ– 𝑒)) = (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))
3130difeq2d 4122 . . . . . . . . . . . 12 (𝑒 = (𝐡 βˆ– 𝑑) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑒))) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))))
3231adantl 483 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) ∧ 𝑒 = (𝐡 βˆ– 𝑑)) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑒))) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))))
33 ssun1 4172 . . . . . . . . . . . . . . 15 𝐡 βŠ† (𝐡 βˆͺ 𝑑)
3433sspwi 4614 . . . . . . . . . . . . . 14 𝒫 𝐡 βŠ† 𝒫 (𝐡 βˆͺ 𝑑)
3534, 11sselid 3980 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐡 ∈ 𝒫 (𝐡 βˆͺ 𝑑))
36 vex 3479 . . . . . . . . . . . . . 14 𝑑 ∈ V
3736elpwun 7753 . . . . . . . . . . . . 13 (𝐡 ∈ 𝒫 (𝐡 βˆͺ 𝑑) ↔ (𝐡 βˆ– 𝑑) ∈ 𝒫 𝐡)
3835, 37sylib 217 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐡 βˆ– 𝑑) ∈ 𝒫 𝐡)
3938ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– 𝑑) ∈ 𝒫 𝐡)
409difexd 5329 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))) ∈ V)
4140ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))) ∈ V)
4228, 32, 39, 41fvmptd 7003 . . . . . . . . . 10 (((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘”β€˜(𝐡 βˆ– 𝑑)) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))))
4342difeq2d 4122 . . . . . . . . 9 (((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) = (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))))
4443adantlrl 719 . . . . . . . 8 (((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) = (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))))
45 elpwi 4609 . . . . . . . . . . . . 13 (𝑑 ∈ 𝒫 𝐡 β†’ 𝑑 βŠ† 𝐡)
46 dfss4 4258 . . . . . . . . . . . . 13 (𝑑 βŠ† 𝐡 ↔ (𝐡 βˆ– (𝐡 βˆ– 𝑑)) = 𝑑)
4745, 46sylib 217 . . . . . . . . . . . 12 (𝑑 ∈ 𝒫 𝐡 β†’ (𝐡 βˆ– (𝐡 βˆ– 𝑑)) = 𝑑)
4847fveq2d 6893 . . . . . . . . . . 11 (𝑑 ∈ 𝒫 𝐡 β†’ (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))) = (π‘“β€˜π‘‘))
4948difeq2d 4122 . . . . . . . . . 10 (𝑑 ∈ 𝒫 𝐡 β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))) = (𝐡 βˆ– (π‘“β€˜π‘‘)))
5049difeq2d 4122 . . . . . . . . 9 (𝑑 ∈ 𝒫 𝐡 β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))) = (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜π‘‘))))
5150adantl 483 . . . . . . . 8 (((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))) = (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜π‘‘))))
5218, 18elmapd 8831 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↔ 𝑓:𝒫 π΅βŸΆπ’« 𝐡))
5352biimpa 478 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) β†’ 𝑓:𝒫 π΅βŸΆπ’« 𝐡)
5453ffvelcdmda 7084 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘“β€˜π‘‘) ∈ 𝒫 𝐡)
5554elpwid 4611 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘“β€˜π‘‘) βŠ† 𝐡)
56 dfss4 4258 . . . . . . . . . 10 ((π‘“β€˜π‘‘) βŠ† 𝐡 ↔ (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜π‘‘))) = (π‘“β€˜π‘‘))
5755, 56sylib 217 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜π‘‘))) = (π‘“β€˜π‘‘))
5857adantlrr 720 . . . . . . . 8 (((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜π‘‘))) = (π‘“β€˜π‘‘))
5944, 51, 583eqtrrd 2778 . . . . . . 7 (((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘“β€˜π‘‘) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))))
6059ralrimiva 3147 . . . . . 6 ((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) β†’ βˆ€π‘‘ ∈ 𝒫 𝐡(π‘“β€˜π‘‘) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))))
61 elmapfn 8856 . . . . . . . 8 (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) β†’ 𝑓 Fn 𝒫 𝐡)
6261ad2antrl 727 . . . . . . 7 ((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) β†’ 𝑓 Fn 𝒫 𝐡)
63 difeq2 4116 . . . . . . . . 9 (𝑑 = 𝑧 β†’ (𝐡 βˆ– 𝑑) = (𝐡 βˆ– 𝑧))
6463fveq2d 6893 . . . . . . . 8 (𝑑 = 𝑧 β†’ (π‘”β€˜(𝐡 βˆ– 𝑑)) = (π‘”β€˜(𝐡 βˆ– 𝑧)))
6564difeq2d 4122 . . . . . . 7 (𝑑 = 𝑧 β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))
669difexd 5329 . . . . . . . 8 (πœ‘ β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) ∈ V)
6766ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) ∈ V)
689difexd 5329 . . . . . . . 8 (πœ‘ β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))) ∈ V)
6968ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) ∧ 𝑧 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))) ∈ V)
7062, 65, 67, 69fnmptfvd 7040 . . . . . 6 ((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) β†’ (𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))) ↔ βˆ€π‘‘ ∈ 𝒫 𝐡(π‘“β€˜π‘‘) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑)))))
7160, 70mpbird 257 . . . . 5 ((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) β†’ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))
7222, 71jca 513 . . . 4 ((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) β†’ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))))
73 simpr 486 . . . . . . . . 9 ((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) β†’ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))
74 difeq2 4116 . . . . . . . . . . . 12 (𝑧 = 𝑑 β†’ (𝐡 βˆ– 𝑧) = (𝐡 βˆ– 𝑑))
7574fveq2d 6893 . . . . . . . . . . 11 (𝑧 = 𝑑 β†’ (π‘”β€˜(𝐡 βˆ– 𝑧)) = (π‘”β€˜(𝐡 βˆ– 𝑑)))
7675difeq2d 4122 . . . . . . . . . 10 (𝑧 = 𝑑 β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))))
7776cbvmptv 5261 . . . . . . . . 9 (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))) = (𝑑 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))))
7873, 77eqtrdi 2789 . . . . . . . 8 ((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) β†’ 𝑓 = (𝑑 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑)))))
79 ssun1 4172 . . . . . . . . . . . 12 𝐡 βŠ† (𝐡 βˆͺ (π‘”β€˜(𝐡 βˆ– 𝑑)))
8079sspwi 4614 . . . . . . . . . . 11 𝒫 𝐡 βŠ† 𝒫 (𝐡 βˆͺ (π‘”β€˜(𝐡 βˆ– 𝑑)))
8180, 11sselid 3980 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ 𝒫 (𝐡 βˆͺ (π‘”β€˜(𝐡 βˆ– 𝑑))))
82 fvex 6902 . . . . . . . . . . 11 (π‘”β€˜(𝐡 βˆ– 𝑑)) ∈ V
8382elpwun 7753 . . . . . . . . . 10 (𝐡 ∈ 𝒫 (𝐡 βˆͺ (π‘”β€˜(𝐡 βˆ– 𝑑))) ↔ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) ∈ 𝒫 𝐡)
8481, 83sylib 217 . . . . . . . . 9 (πœ‘ β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) ∈ 𝒫 𝐡)
8584ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) ∈ 𝒫 𝐡)
8678, 85fmpt3d 7113 . . . . . . 7 ((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) β†’ 𝑓:𝒫 π΅βŸΆπ’« 𝐡)
8718adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) β†’ 𝒫 𝐡 ∈ V)
8887, 87elmapd 8831 . . . . . . 7 ((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) β†’ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↔ 𝑓:𝒫 π΅βŸΆπ’« 𝐡))
8986, 88mpbird 257 . . . . . 6 ((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) β†’ 𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡))
9089adantrl 715 . . . . 5 ((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) β†’ 𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡))
91 simplr 768 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))
92 difeq2 4116 . . . . . . . . . . . . . . 15 (𝑧 = 𝑒 β†’ (𝐡 βˆ– 𝑧) = (𝐡 βˆ– 𝑒))
9392fveq2d 6893 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 β†’ (π‘”β€˜(𝐡 βˆ– 𝑧)) = (π‘”β€˜(𝐡 βˆ– 𝑒)))
9493difeq2d 4122 . . . . . . . . . . . . 13 (𝑧 = 𝑒 β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑒))))
9594cbvmptv 5261 . . . . . . . . . . . 12 (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))) = (𝑒 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑒))))
9691, 95eqtrdi 2789 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ 𝑓 = (𝑒 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑒)))))
9729fveq2d 6893 . . . . . . . . . . . . 13 (𝑒 = (𝐡 βˆ– 𝑑) β†’ (π‘”β€˜(𝐡 βˆ– 𝑒)) = (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))
9897difeq2d 4122 . . . . . . . . . . . 12 (𝑒 = (𝐡 βˆ– 𝑑) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑒))) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))))
9998adantl 483 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) ∧ 𝑒 = (𝐡 βˆ– 𝑑)) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑒))) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))))
10038ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– 𝑑) ∈ 𝒫 𝐡)
1019difexd 5329 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))) ∈ V)
102101ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))) ∈ V)
10396, 99, 100, 102fvmptd 7003 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘“β€˜(𝐡 βˆ– 𝑑)) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))))
104103difeq2d 4122 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) = (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))))
105104adantlrl 719 . . . . . . . 8 (((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) = (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))))
10647fveq2d 6893 . . . . . . . . . . 11 (𝑑 ∈ 𝒫 𝐡 β†’ (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))) = (π‘”β€˜π‘‘))
107106difeq2d 4122 . . . . . . . . . 10 (𝑑 ∈ 𝒫 𝐡 β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))) = (𝐡 βˆ– (π‘”β€˜π‘‘)))
108107difeq2d 4122 . . . . . . . . 9 (𝑑 ∈ 𝒫 𝐡 β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))) = (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜π‘‘))))
109108adantl 483 . . . . . . . 8 (((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))) = (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜π‘‘))))
11018, 18elmapd 8831 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↔ 𝑔:𝒫 π΅βŸΆπ’« 𝐡))
111110biimpa 478 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) β†’ 𝑔:𝒫 π΅βŸΆπ’« 𝐡)
112111ffvelcdmda 7084 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘”β€˜π‘‘) ∈ 𝒫 𝐡)
113112elpwid 4611 . . . . . . . . . 10 (((πœ‘ ∧ 𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘”β€˜π‘‘) βŠ† 𝐡)
114 dfss4 4258 . . . . . . . . . 10 ((π‘”β€˜π‘‘) βŠ† 𝐡 ↔ (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜π‘‘))) = (π‘”β€˜π‘‘))
115113, 114sylib 217 . . . . . . . . 9 (((πœ‘ ∧ 𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜π‘‘))) = (π‘”β€˜π‘‘))
116115adantlrr 720 . . . . . . . 8 (((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜π‘‘))) = (π‘”β€˜π‘‘))
117105, 109, 1163eqtrrd 2778 . . . . . . 7 (((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘”β€˜π‘‘) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))))
118117ralrimiva 3147 . . . . . 6 ((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) β†’ βˆ€π‘‘ ∈ 𝒫 𝐡(π‘”β€˜π‘‘) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))))
119 elmapfn 8856 . . . . . . . 8 (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) β†’ 𝑔 Fn 𝒫 𝐡)
120119ad2antrl 727 . . . . . . 7 ((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) β†’ 𝑔 Fn 𝒫 𝐡)
121 difeq2 4116 . . . . . . . . 9 (𝑑 = 𝑠 β†’ (𝐡 βˆ– 𝑑) = (𝐡 βˆ– 𝑠))
122121fveq2d 6893 . . . . . . . 8 (𝑑 = 𝑠 β†’ (π‘“β€˜(𝐡 βˆ– 𝑑)) = (π‘“β€˜(𝐡 βˆ– 𝑠)))
123122difeq2d 4122 . . . . . . 7 (𝑑 = 𝑠 β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))
1249difexd 5329 . . . . . . . 8 (πœ‘ β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) ∈ V)
125124ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) ∈ V)
1269difexd 5329 . . . . . . . 8 (πœ‘ β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))) ∈ V)
127126ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) ∧ 𝑠 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))) ∈ V)
128120, 123, 125, 127fnmptfvd 7040 . . . . . 6 ((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) β†’ (𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))) ↔ βˆ€π‘‘ ∈ 𝒫 𝐡(π‘”β€˜π‘‘) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑)))))
129118, 128mpbird 257 . . . . 5 ((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) β†’ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))
13090, 129jca 513 . . . 4 ((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) β†’ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))))
13172, 130impbida 800 . . 3 (πœ‘ β†’ ((𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ↔ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))))
132131mptcnv 6137 . 2 (πœ‘ β†’ β—‘(𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↦ (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) = (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↦ (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))))
133 dssmapfvd.o . . . 4 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘“β€˜(𝑏 βˆ– 𝑠))))))
134 dssmapfvd.d . . . 4 𝐷 = (π‘‚β€˜π΅)
135133, 134, 9dssmapfvd 42754 . . 3 (πœ‘ β†’ 𝐷 = (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↦ (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))))
136135cnveqd 5874 . 2 (πœ‘ β†’ ◑𝐷 = β—‘(𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↦ (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))))
137 fveq1 6888 . . . . . . . . 9 (𝑓 = 𝑔 β†’ (π‘“β€˜(𝑏 βˆ– 𝑠)) = (π‘”β€˜(𝑏 βˆ– 𝑠)))
138137difeq2d 4122 . . . . . . . 8 (𝑓 = 𝑔 β†’ (𝑏 βˆ– (π‘“β€˜(𝑏 βˆ– 𝑠))) = (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑠))))
139138mpteq2dv 5250 . . . . . . 7 (𝑓 = 𝑔 β†’ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘“β€˜(𝑏 βˆ– 𝑠)))) = (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑠)))))
140 difeq2 4116 . . . . . . . . . 10 (𝑠 = 𝑧 β†’ (𝑏 βˆ– 𝑠) = (𝑏 βˆ– 𝑧))
141140fveq2d 6893 . . . . . . . . 9 (𝑠 = 𝑧 β†’ (π‘”β€˜(𝑏 βˆ– 𝑠)) = (π‘”β€˜(𝑏 βˆ– 𝑧)))
142141difeq2d 4122 . . . . . . . 8 (𝑠 = 𝑧 β†’ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑠))) = (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑧))))
143142cbvmptv 5261 . . . . . . 7 (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑧))))
144139, 143eqtrdi 2789 . . . . . 6 (𝑓 = 𝑔 β†’ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘“β€˜(𝑏 βˆ– 𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑧)))))
145144cbvmptv 5261 . . . . 5 (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘“β€˜(𝑏 βˆ– 𝑠))))) = (𝑔 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑧)))))
146145mpteq2i 5253 . . . 4 (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘“β€˜(𝑏 βˆ– 𝑠)))))) = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑧))))))
147133, 146eqtri 2761 . . 3 𝑂 = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑧))))))
148147, 134, 9dssmapfvd 42754 . 2 (πœ‘ β†’ 𝐷 = (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↦ (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))))
149132, 136, 1483eqtr4d 2783 1 (πœ‘ β†’ ◑𝐷 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  Vcvv 3475   βˆ– cdif 3945   βˆͺ cun 3946   βŠ† wss 3948  π’« cpw 4602   ↦ cmpt 5231  β—‘ccnv 5675   Fn wfn 6536  βŸΆwf 6537  β€˜cfv 6541  (class class class)co 7406   ↑m cmap 8817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-1st 7972  df-2nd 7973  df-map 8819
This theorem is referenced by:  dssmapf1od  42758  dssmap2d  42759  ntrclsnvobr  42789  clsneicnv  42842  neicvgnvo  42852  dssmapclsntr  42866
  Copyright terms: Public domain W3C validator