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 43073
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 483 . . . . . . . . 9 ((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) β†’ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))
2 difeq2 4115 . . . . . . . . . . . 12 (𝑠 = 𝑑 β†’ (𝐡 βˆ– 𝑠) = (𝐡 βˆ– 𝑑))
32fveq2d 6894 . . . . . . . . . . 11 (𝑠 = 𝑑 β†’ (π‘“β€˜(𝐡 βˆ– 𝑠)) = (π‘“β€˜(𝐡 βˆ– 𝑑)))
43difeq2d 4121 . . . . . . . . . 10 (𝑠 = 𝑑 β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))))
54cbvmptv 5260 . . . . . . . . 9 (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))) = (𝑑 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))))
61, 5eqtrdi 2786 . . . . . . . 8 ((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) β†’ 𝑔 = (𝑑 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑)))))
7 ssun1 4171 . . . . . . . . . . . 12 𝐡 βŠ† (𝐡 βˆͺ (π‘“β€˜(𝐡 βˆ– 𝑑)))
87sspwi 4613 . . . . . . . . . . 11 𝒫 𝐡 βŠ† 𝒫 (𝐡 βˆͺ (π‘“β€˜(𝐡 βˆ– 𝑑)))
9 dssmapfvd.b . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 ∈ 𝑉)
10 pwidg 4621 . . . . . . . . . . . 12 (𝐡 ∈ 𝑉 β†’ 𝐡 ∈ 𝒫 𝐡)
119, 10syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ∈ 𝒫 𝐡)
128, 11sselid 3979 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ 𝒫 (𝐡 βˆͺ (π‘“β€˜(𝐡 βˆ– 𝑑))))
13 fvex 6903 . . . . . . . . . . 11 (π‘“β€˜(𝐡 βˆ– 𝑑)) ∈ V
1413elpwun 7758 . . . . . . . . . 10 (𝐡 ∈ 𝒫 (𝐡 βˆͺ (π‘“β€˜(𝐡 βˆ– 𝑑))) ↔ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) ∈ 𝒫 𝐡)
1512, 14sylib 217 . . . . . . . . 9 (πœ‘ β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) ∈ 𝒫 𝐡)
1615ad2antrr 722 . . . . . . . 8 (((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) ∈ 𝒫 𝐡)
176, 16fmpt3d 7116 . . . . . . 7 ((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) β†’ 𝑔:𝒫 π΅βŸΆπ’« 𝐡)
189pwexd 5376 . . . . . . . . 9 (πœ‘ β†’ 𝒫 𝐡 ∈ V)
1918adantr 479 . . . . . . . 8 ((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) β†’ 𝒫 𝐡 ∈ V)
2019, 19elmapd 8836 . . . . . . 7 ((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) β†’ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↔ 𝑔:𝒫 π΅βŸΆπ’« 𝐡))
2117, 20mpbird 256 . . . . . 6 ((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) β†’ 𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡))
2221adantrl 712 . . . . 5 ((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) β†’ 𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡))
23 simplr 765 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))
24 difeq2 4115 . . . . . . . . . . . . . . 15 (𝑠 = 𝑒 β†’ (𝐡 βˆ– 𝑠) = (𝐡 βˆ– 𝑒))
2524fveq2d 6894 . . . . . . . . . . . . . 14 (𝑠 = 𝑒 β†’ (π‘“β€˜(𝐡 βˆ– 𝑠)) = (π‘“β€˜(𝐡 βˆ– 𝑒)))
2625difeq2d 4121 . . . . . . . . . . . . 13 (𝑠 = 𝑒 β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑒))))
2726cbvmptv 5260 . . . . . . . . . . . 12 (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))) = (𝑒 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑒))))
2823, 27eqtrdi 2786 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ 𝑔 = (𝑒 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑒)))))
29 difeq2 4115 . . . . . . . . . . . . . 14 (𝑒 = (𝐡 βˆ– 𝑑) β†’ (𝐡 βˆ– 𝑒) = (𝐡 βˆ– (𝐡 βˆ– 𝑑)))
3029fveq2d 6894 . . . . . . . . . . . . 13 (𝑒 = (𝐡 βˆ– 𝑑) β†’ (π‘“β€˜(𝐡 βˆ– 𝑒)) = (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))
3130difeq2d 4121 . . . . . . . . . . . 12 (𝑒 = (𝐡 βˆ– 𝑑) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑒))) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))))
3231adantl 480 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) ∧ 𝑒 = (𝐡 βˆ– 𝑑)) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑒))) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))))
33 ssun1 4171 . . . . . . . . . . . . . . 15 𝐡 βŠ† (𝐡 βˆͺ 𝑑)
3433sspwi 4613 . . . . . . . . . . . . . 14 𝒫 𝐡 βŠ† 𝒫 (𝐡 βˆͺ 𝑑)
3534, 11sselid 3979 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐡 ∈ 𝒫 (𝐡 βˆͺ 𝑑))
36 vex 3476 . . . . . . . . . . . . . 14 𝑑 ∈ V
3736elpwun 7758 . . . . . . . . . . . . 13 (𝐡 ∈ 𝒫 (𝐡 βˆͺ 𝑑) ↔ (𝐡 βˆ– 𝑑) ∈ 𝒫 𝐡)
3835, 37sylib 217 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐡 βˆ– 𝑑) ∈ 𝒫 𝐡)
3938ad2antrr 722 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– 𝑑) ∈ 𝒫 𝐡)
409difexd 5328 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))) ∈ V)
4140ad2antrr 722 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))) ∈ V)
4228, 32, 39, 41fvmptd 7004 . . . . . . . . . 10 (((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘”β€˜(𝐡 βˆ– 𝑑)) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))))
4342difeq2d 4121 . . . . . . . . 9 (((πœ‘ ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) = (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))))
4443adantlrl 716 . . . . . . . 8 (((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) = (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))))
45 elpwi 4608 . . . . . . . . . . . . 13 (𝑑 ∈ 𝒫 𝐡 β†’ 𝑑 βŠ† 𝐡)
46 dfss4 4257 . . . . . . . . . . . . 13 (𝑑 βŠ† 𝐡 ↔ (𝐡 βˆ– (𝐡 βˆ– 𝑑)) = 𝑑)
4745, 46sylib 217 . . . . . . . . . . . 12 (𝑑 ∈ 𝒫 𝐡 β†’ (𝐡 βˆ– (𝐡 βˆ– 𝑑)) = 𝑑)
4847fveq2d 6894 . . . . . . . . . . 11 (𝑑 ∈ 𝒫 𝐡 β†’ (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))) = (π‘“β€˜π‘‘))
4948difeq2d 4121 . . . . . . . . . 10 (𝑑 ∈ 𝒫 𝐡 β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))) = (𝐡 βˆ– (π‘“β€˜π‘‘)))
5049difeq2d 4121 . . . . . . . . 9 (𝑑 ∈ 𝒫 𝐡 β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))) = (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜π‘‘))))
5150adantl 480 . . . . . . . 8 (((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))) = (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜π‘‘))))
5218, 18elmapd 8836 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↔ 𝑓:𝒫 π΅βŸΆπ’« 𝐡))
5352biimpa 475 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) β†’ 𝑓:𝒫 π΅βŸΆπ’« 𝐡)
5453ffvelcdmda 7085 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘“β€˜π‘‘) ∈ 𝒫 𝐡)
5554elpwid 4610 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘“β€˜π‘‘) βŠ† 𝐡)
56 dfss4 4257 . . . . . . . . . 10 ((π‘“β€˜π‘‘) βŠ† 𝐡 ↔ (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜π‘‘))) = (π‘“β€˜π‘‘))
5755, 56sylib 217 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜π‘‘))) = (π‘“β€˜π‘‘))
5857adantlrr 717 . . . . . . . 8 (((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘“β€˜π‘‘))) = (π‘“β€˜π‘‘))
5944, 51, 583eqtrrd 2775 . . . . . . 7 (((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘“β€˜π‘‘) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))))
6059ralrimiva 3144 . . . . . 6 ((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) β†’ βˆ€π‘‘ ∈ 𝒫 𝐡(π‘“β€˜π‘‘) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))))
61 elmapfn 8861 . . . . . . . 8 (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) β†’ 𝑓 Fn 𝒫 𝐡)
6261ad2antrl 724 . . . . . . 7 ((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) β†’ 𝑓 Fn 𝒫 𝐡)
63 difeq2 4115 . . . . . . . . 9 (𝑑 = 𝑧 β†’ (𝐡 βˆ– 𝑑) = (𝐡 βˆ– 𝑧))
6463fveq2d 6894 . . . . . . . 8 (𝑑 = 𝑧 β†’ (π‘”β€˜(𝐡 βˆ– 𝑑)) = (π‘”β€˜(𝐡 βˆ– 𝑧)))
6564difeq2d 4121 . . . . . . 7 (𝑑 = 𝑧 β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))
669difexd 5328 . . . . . . . 8 (πœ‘ β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) ∈ V)
6766ad2antrr 722 . . . . . . 7 (((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) ∈ V)
689difexd 5328 . . . . . . . 8 (πœ‘ β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))) ∈ V)
6968ad2antrr 722 . . . . . . 7 (((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) ∧ 𝑧 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))) ∈ V)
7062, 65, 67, 69fnmptfvd 7041 . . . . . 6 ((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) β†’ (𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))) ↔ βˆ€π‘‘ ∈ 𝒫 𝐡(π‘“β€˜π‘‘) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑)))))
7160, 70mpbird 256 . . . . 5 ((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) β†’ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))
7222, 71jca 510 . . . 4 ((πœ‘ ∧ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))) β†’ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))))
73 simpr 483 . . . . . . . . 9 ((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) β†’ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))
74 difeq2 4115 . . . . . . . . . . . 12 (𝑧 = 𝑑 β†’ (𝐡 βˆ– 𝑧) = (𝐡 βˆ– 𝑑))
7574fveq2d 6894 . . . . . . . . . . 11 (𝑧 = 𝑑 β†’ (π‘”β€˜(𝐡 βˆ– 𝑧)) = (π‘”β€˜(𝐡 βˆ– 𝑑)))
7675difeq2d 4121 . . . . . . . . . 10 (𝑧 = 𝑑 β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))))
7776cbvmptv 5260 . . . . . . . . 9 (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))) = (𝑑 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))))
7873, 77eqtrdi 2786 . . . . . . . 8 ((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) β†’ 𝑓 = (𝑑 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑)))))
79 ssun1 4171 . . . . . . . . . . . 12 𝐡 βŠ† (𝐡 βˆͺ (π‘”β€˜(𝐡 βˆ– 𝑑)))
8079sspwi 4613 . . . . . . . . . . 11 𝒫 𝐡 βŠ† 𝒫 (𝐡 βˆͺ (π‘”β€˜(𝐡 βˆ– 𝑑)))
8180, 11sselid 3979 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 ∈ 𝒫 (𝐡 βˆͺ (π‘”β€˜(𝐡 βˆ– 𝑑))))
82 fvex 6903 . . . . . . . . . . 11 (π‘”β€˜(𝐡 βˆ– 𝑑)) ∈ V
8382elpwun 7758 . . . . . . . . . 10 (𝐡 ∈ 𝒫 (𝐡 βˆͺ (π‘”β€˜(𝐡 βˆ– 𝑑))) ↔ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) ∈ 𝒫 𝐡)
8481, 83sylib 217 . . . . . . . . 9 (πœ‘ β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) ∈ 𝒫 𝐡)
8584ad2antrr 722 . . . . . . . 8 (((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑑))) ∈ 𝒫 𝐡)
8678, 85fmpt3d 7116 . . . . . . 7 ((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) β†’ 𝑓:𝒫 π΅βŸΆπ’« 𝐡)
8718adantr 479 . . . . . . . 8 ((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) β†’ 𝒫 𝐡 ∈ V)
8887, 87elmapd 8836 . . . . . . 7 ((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) β†’ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↔ 𝑓:𝒫 π΅βŸΆπ’« 𝐡))
8986, 88mpbird 256 . . . . . 6 ((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) β†’ 𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡))
9089adantrl 712 . . . . 5 ((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) β†’ 𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡))
91 simplr 765 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))
92 difeq2 4115 . . . . . . . . . . . . . . 15 (𝑧 = 𝑒 β†’ (𝐡 βˆ– 𝑧) = (𝐡 βˆ– 𝑒))
9392fveq2d 6894 . . . . . . . . . . . . . 14 (𝑧 = 𝑒 β†’ (π‘”β€˜(𝐡 βˆ– 𝑧)) = (π‘”β€˜(𝐡 βˆ– 𝑒)))
9493difeq2d 4121 . . . . . . . . . . . . 13 (𝑧 = 𝑒 β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑒))))
9594cbvmptv 5260 . . . . . . . . . . . 12 (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))) = (𝑒 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑒))))
9691, 95eqtrdi 2786 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ 𝑓 = (𝑒 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑒)))))
9729fveq2d 6894 . . . . . . . . . . . . 13 (𝑒 = (𝐡 βˆ– 𝑑) β†’ (π‘”β€˜(𝐡 βˆ– 𝑒)) = (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))
9897difeq2d 4121 . . . . . . . . . . . 12 (𝑒 = (𝐡 βˆ– 𝑑) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑒))) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))))
9998adantl 480 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) ∧ 𝑒 = (𝐡 βˆ– 𝑑)) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑒))) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))))
10038ad2antrr 722 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– 𝑑) ∈ 𝒫 𝐡)
1019difexd 5328 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))) ∈ V)
102101ad2antrr 722 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))) ∈ V)
10396, 99, 100, 102fvmptd 7004 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘“β€˜(𝐡 βˆ– 𝑑)) = (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))))
104103difeq2d 4121 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) = (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))))
105104adantlrl 716 . . . . . . . 8 (((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) = (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))))
10647fveq2d 6894 . . . . . . . . . . 11 (𝑑 ∈ 𝒫 𝐡 β†’ (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))) = (π‘”β€˜π‘‘))
107106difeq2d 4121 . . . . . . . . . 10 (𝑑 ∈ 𝒫 𝐡 β†’ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑)))) = (𝐡 βˆ– (π‘”β€˜π‘‘)))
108107difeq2d 4121 . . . . . . . . 9 (𝑑 ∈ 𝒫 𝐡 β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))) = (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜π‘‘))))
109108adantl 480 . . . . . . . 8 (((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– (𝐡 βˆ– 𝑑))))) = (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜π‘‘))))
11018, 18elmapd 8836 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↔ 𝑔:𝒫 π΅βŸΆπ’« 𝐡))
111110biimpa 475 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) β†’ 𝑔:𝒫 π΅βŸΆπ’« 𝐡)
112111ffvelcdmda 7085 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘”β€˜π‘‘) ∈ 𝒫 𝐡)
113112elpwid 4610 . . . . . . . . . 10 (((πœ‘ ∧ 𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘”β€˜π‘‘) βŠ† 𝐡)
114 dfss4 4257 . . . . . . . . . 10 ((π‘”β€˜π‘‘) βŠ† 𝐡 ↔ (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜π‘‘))) = (π‘”β€˜π‘‘))
115113, 114sylib 217 . . . . . . . . 9 (((πœ‘ ∧ 𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡)) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜π‘‘))) = (π‘”β€˜π‘‘))
116115adantlrr 717 . . . . . . . 8 (((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (𝐡 βˆ– (π‘”β€˜π‘‘))) = (π‘”β€˜π‘‘))
117105, 109, 1163eqtrrd 2775 . . . . . . 7 (((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (π‘”β€˜π‘‘) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))))
118117ralrimiva 3144 . . . . . 6 ((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) β†’ βˆ€π‘‘ ∈ 𝒫 𝐡(π‘”β€˜π‘‘) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))))
119 elmapfn 8861 . . . . . . . 8 (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) β†’ 𝑔 Fn 𝒫 𝐡)
120119ad2antrl 724 . . . . . . 7 ((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) β†’ 𝑔 Fn 𝒫 𝐡)
121 difeq2 4115 . . . . . . . . 9 (𝑑 = 𝑠 β†’ (𝐡 βˆ– 𝑑) = (𝐡 βˆ– 𝑠))
122121fveq2d 6894 . . . . . . . 8 (𝑑 = 𝑠 β†’ (π‘“β€˜(𝐡 βˆ– 𝑑)) = (π‘“β€˜(𝐡 βˆ– 𝑠)))
123122difeq2d 4121 . . . . . . 7 (𝑑 = 𝑠 β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))
1249difexd 5328 . . . . . . . 8 (πœ‘ β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) ∈ V)
125124ad2antrr 722 . . . . . . 7 (((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) ∧ 𝑑 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑))) ∈ V)
1269difexd 5328 . . . . . . . 8 (πœ‘ β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))) ∈ V)
127126ad2antrr 722 . . . . . . 7 (((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) ∧ 𝑠 ∈ 𝒫 𝐡) β†’ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))) ∈ V)
128120, 123, 125, 127fnmptfvd 7041 . . . . . 6 ((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) β†’ (𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))) ↔ βˆ€π‘‘ ∈ 𝒫 𝐡(π‘”β€˜π‘‘) = (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑑)))))
129118, 128mpbird 256 . . . . 5 ((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) β†’ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠)))))
13090, 129jca 510 . . . 4 ((πœ‘ ∧ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))) β†’ (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))))
13172, 130impbida 797 . . 3 (πœ‘ β†’ ((𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) ↔ (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧)))))))
132131mptcnv 6138 . 2 (πœ‘ β†’ β—‘(𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↦ (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))) = (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↦ (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))))
133 dssmapfvd.o . . . 4 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘“β€˜(𝑏 βˆ– 𝑠))))))
134 dssmapfvd.d . . . 4 𝐷 = (π‘‚β€˜π΅)
135133, 134, 9dssmapfvd 43070 . . 3 (πœ‘ β†’ 𝐷 = (𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↦ (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))))
136135cnveqd 5874 . 2 (πœ‘ β†’ ◑𝐷 = β—‘(𝑓 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↦ (𝑠 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘“β€˜(𝐡 βˆ– 𝑠))))))
137 fveq1 6889 . . . . . . . . 9 (𝑓 = 𝑔 β†’ (π‘“β€˜(𝑏 βˆ– 𝑠)) = (π‘”β€˜(𝑏 βˆ– 𝑠)))
138137difeq2d 4121 . . . . . . . 8 (𝑓 = 𝑔 β†’ (𝑏 βˆ– (π‘“β€˜(𝑏 βˆ– 𝑠))) = (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑠))))
139138mpteq2dv 5249 . . . . . . 7 (𝑓 = 𝑔 β†’ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘“β€˜(𝑏 βˆ– 𝑠)))) = (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑠)))))
140 difeq2 4115 . . . . . . . . . 10 (𝑠 = 𝑧 β†’ (𝑏 βˆ– 𝑠) = (𝑏 βˆ– 𝑧))
141140fveq2d 6894 . . . . . . . . 9 (𝑠 = 𝑧 β†’ (π‘”β€˜(𝑏 βˆ– 𝑠)) = (π‘”β€˜(𝑏 βˆ– 𝑧)))
142141difeq2d 4121 . . . . . . . 8 (𝑠 = 𝑧 β†’ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑠))) = (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑧))))
143142cbvmptv 5260 . . . . . . 7 (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑧))))
144139, 143eqtrdi 2786 . . . . . 6 (𝑓 = 𝑔 β†’ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘“β€˜(𝑏 βˆ– 𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑧)))))
145144cbvmptv 5260 . . . . 5 (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘“β€˜(𝑏 βˆ– 𝑠))))) = (𝑔 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑧)))))
146145mpteq2i 5252 . . . 4 (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘“β€˜(𝑏 βˆ– 𝑠)))))) = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑧))))))
147133, 146eqtri 2758 . . 3 𝑂 = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 βˆ– (π‘”β€˜(𝑏 βˆ– 𝑧))))))
148147, 134, 9dssmapfvd 43070 . 2 (πœ‘ β†’ 𝐷 = (𝑔 ∈ (𝒫 𝐡 ↑m 𝒫 𝐡) ↦ (𝑧 ∈ 𝒫 𝐡 ↦ (𝐡 βˆ– (π‘”β€˜(𝐡 βˆ– 𝑧))))))
149132, 136, 1483eqtr4d 2780 1 (πœ‘ β†’ ◑𝐷 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104  βˆ€wral 3059  Vcvv 3472   βˆ– cdif 3944   βˆͺ cun 3945   βŠ† wss 3947  π’« cpw 4601   ↦ cmpt 5230  β—‘ccnv 5674   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411   ↑m cmap 8822
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978  df-map 8824
This theorem is referenced by:  dssmapf1od  43074  dssmap2d  43075  ntrclsnvobr  43105  clsneicnv  43158  neicvgnvo  43168  dssmapclsntr  43182
  Copyright terms: Public domain W3C validator