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 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.
StepHypRef Expression
1 simpr 484 . . . . . . . . 9 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))
2 difeq2 4120 . . . . . . . . . . . 12 (𝑠 = 𝑡 → (𝐵𝑠) = (𝐵𝑡))
32fveq2d 6910 . . . . . . . . . . 11 (𝑠 = 𝑡 → (𝑓‘(𝐵𝑠)) = (𝑓‘(𝐵𝑡)))
43difeq2d 4126 . . . . . . . . . 10 (𝑠 = 𝑡 → (𝐵 ∖ (𝑓‘(𝐵𝑠))) = (𝐵 ∖ (𝑓‘(𝐵𝑡))))
54cbvmptv 5255 . . . . . . . . 9 (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑡))))
61, 5eqtrdi 2793 . . . . . . . 8 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑡)))))
7 ssun1 4178 . . . . . . . . . . . 12 𝐵 ⊆ (𝐵 ∪ (𝑓‘(𝐵𝑡)))
87sspwi 4612 . . . . . . . . . . 11 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑓‘(𝐵𝑡)))
9 dssmapfvd.b . . . . . . . . . . . 12 (𝜑𝐵𝑉)
10 pwidg 4620 . . . . . . . . . . . 12 (𝐵𝑉𝐵 ∈ 𝒫 𝐵)
119, 10syl 17 . . . . . . . . . . 11 (𝜑𝐵 ∈ 𝒫 𝐵)
128, 11sselid 3981 . . . . . . . . . 10 (𝜑𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵𝑡))))
13 fvex 6919 . . . . . . . . . . 11 (𝑓‘(𝐵𝑡)) ∈ V
1413elpwun 7789 . . . . . . . . . 10 (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵𝑡))) ↔ (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ 𝒫 𝐵)
1512, 14sylib 218 . . . . . . . . 9 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ 𝒫 𝐵)
1615ad2antrr 726 . . . . . . . 8 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ 𝒫 𝐵)
176, 16fmpt3d 7136 . . . . . . 7 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔:𝒫 𝐵⟶𝒫 𝐵)
189pwexd 5379 . . . . . . . . 9 (𝜑 → 𝒫 𝐵 ∈ V)
1918adantr 480 . . . . . . . 8 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝒫 𝐵 ∈ V)
2019, 19elmapd 8880 . . . . . . 7 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵))
2117, 20mpbird 257 . . . . . 6 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵))
2221adantrl 716 . . . . 5 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → 𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵))
23 simplr 769 . . . . . . . . . . . 12 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))
24 difeq2 4120 . . . . . . . . . . . . . . 15 (𝑠 = 𝑢 → (𝐵𝑠) = (𝐵𝑢))
2524fveq2d 6910 . . . . . . . . . . . . . 14 (𝑠 = 𝑢 → (𝑓‘(𝐵𝑠)) = (𝑓‘(𝐵𝑢)))
2625difeq2d 4126 . . . . . . . . . . . . 13 (𝑠 = 𝑢 → (𝐵 ∖ (𝑓‘(𝐵𝑠))) = (𝐵 ∖ (𝑓‘(𝐵𝑢))))
2726cbvmptv 5255 . . . . . . . . . . . 12 (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑢))))
2823, 27eqtrdi 2793 . . . . . . . . . . 11 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑢)))))
29 difeq2 4120 . . . . . . . . . . . . . 14 (𝑢 = (𝐵𝑡) → (𝐵𝑢) = (𝐵 ∖ (𝐵𝑡)))
3029fveq2d 6910 . . . . . . . . . . . . 13 (𝑢 = (𝐵𝑡) → (𝑓‘(𝐵𝑢)) = (𝑓‘(𝐵 ∖ (𝐵𝑡))))
3130difeq2d 4126 . . . . . . . . . . . 12 (𝑢 = (𝐵𝑡) → (𝐵 ∖ (𝑓‘(𝐵𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))))
3231adantl 481 . . . . . . . . . . 11 ((((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵𝑡)) → (𝐵 ∖ (𝑓‘(𝐵𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))))
33 ssun1 4178 . . . . . . . . . . . . . . 15 𝐵 ⊆ (𝐵𝑡)
3433sspwi 4612 . . . . . . . . . . . . . 14 𝒫 𝐵 ⊆ 𝒫 (𝐵𝑡)
3534, 11sselid 3981 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ 𝒫 (𝐵𝑡))
36 vex 3484 . . . . . . . . . . . . . 14 𝑡 ∈ V
3736elpwun 7789 . . . . . . . . . . . . 13 (𝐵 ∈ 𝒫 (𝐵𝑡) ↔ (𝐵𝑡) ∈ 𝒫 𝐵)
3835, 37sylib 218 . . . . . . . . . . . 12 (𝜑 → (𝐵𝑡) ∈ 𝒫 𝐵)
3938ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵𝑡) ∈ 𝒫 𝐵)
409difexd 5331 . . . . . . . . . . . 12 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
4140ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
4228, 32, 39, 41fvmptd 7023 . . . . . . . . . 10 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘(𝐵𝑡)) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))))
4342difeq2d 4126 . . . . . . . . 9 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))))
4443adantlrl 720 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))))
45 elpwi 4607 . . . . . . . . . . . . 13 (𝑡 ∈ 𝒫 𝐵𝑡𝐵)
46 dfss4 4269 . . . . . . . . . . . . 13 (𝑡𝐵 ↔ (𝐵 ∖ (𝐵𝑡)) = 𝑡)
4745, 46sylib 218 . . . . . . . . . . . 12 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵𝑡)) = 𝑡)
4847fveq2d 6910 . . . . . . . . . . 11 (𝑡 ∈ 𝒫 𝐵 → (𝑓‘(𝐵 ∖ (𝐵𝑡))) = (𝑓𝑡))
4948difeq2d 4126 . . . . . . . . . 10 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))) = (𝐵 ∖ (𝑓𝑡)))
5049difeq2d 4126 . . . . . . . . 9 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))))
5150adantl 481 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))))
5218, 18elmapd 8880 . . . . . . . . . . . . 13 (𝜑 → (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵))
5352biimpa 476 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵)) → 𝑓:𝒫 𝐵⟶𝒫 𝐵)
5453ffvelcdmda 7104 . . . . . . . . . . 11 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓𝑡) ∈ 𝒫 𝐵)
5554elpwid 4609 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓𝑡) ⊆ 𝐵)
56 dfss4 4269 . . . . . . . . . 10 ((𝑓𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))) = (𝑓𝑡))
5755, 56sylib 218 . . . . . . . . 9 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))) = (𝑓𝑡))
5857adantlrr 721 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))) = (𝑓𝑡))
5944, 51, 583eqtrrd 2782 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓𝑡) = (𝐵 ∖ (𝑔‘(𝐵𝑡))))
6059ralrimiva 3146 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑓𝑡) = (𝐵 ∖ (𝑔‘(𝐵𝑡))))
61 elmapfn 8905 . . . . . . . 8 (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) → 𝑓 Fn 𝒫 𝐵)
6261ad2antrl 728 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → 𝑓 Fn 𝒫 𝐵)
63 difeq2 4120 . . . . . . . . 9 (𝑡 = 𝑧 → (𝐵𝑡) = (𝐵𝑧))
6463fveq2d 6910 . . . . . . . 8 (𝑡 = 𝑧 → (𝑔‘(𝐵𝑡)) = (𝑔‘(𝐵𝑧)))
6564difeq2d 4126 . . . . . . 7 (𝑡 = 𝑧 → (𝐵 ∖ (𝑔‘(𝐵𝑡))) = (𝐵 ∖ (𝑔‘(𝐵𝑧))))
669difexd 5331 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ V)
6766ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ V)
689difexd 5331 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵𝑧))) ∈ V)
6968ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑧))) ∈ V)
7062, 65, 67, 69fnmptfvd 7061 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → (𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑓𝑡) = (𝐵 ∖ (𝑔‘(𝐵𝑡)))))
7160, 70mpbird 257 . . . . 5 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))
7222, 71jca 511 . . . 4 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))))
73 simpr 484 . . . . . . . . 9 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))
74 difeq2 4120 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝐵𝑧) = (𝐵𝑡))
7574fveq2d 6910 . . . . . . . . . . 11 (𝑧 = 𝑡 → (𝑔‘(𝐵𝑧)) = (𝑔‘(𝐵𝑡)))
7675difeq2d 4126 . . . . . . . . . 10 (𝑧 = 𝑡 → (𝐵 ∖ (𝑔‘(𝐵𝑧))) = (𝐵 ∖ (𝑔‘(𝐵𝑡))))
7776cbvmptv 5255 . . . . . . . . 9 (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑡))))
7873, 77eqtrdi 2793 . . . . . . . 8 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑡)))))
79 ssun1 4178 . . . . . . . . . . . 12 𝐵 ⊆ (𝐵 ∪ (𝑔‘(𝐵𝑡)))
8079sspwi 4612 . . . . . . . . . . 11 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑔‘(𝐵𝑡)))
8180, 11sselid 3981 . . . . . . . . . 10 (𝜑𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵𝑡))))
82 fvex 6919 . . . . . . . . . . 11 (𝑔‘(𝐵𝑡)) ∈ V
8382elpwun 7789 . . . . . . . . . 10 (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵𝑡))) ↔ (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ 𝒫 𝐵)
8481, 83sylib 218 . . . . . . . . 9 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ 𝒫 𝐵)
8584ad2antrr 726 . . . . . . . 8 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ 𝒫 𝐵)
8678, 85fmpt3d 7136 . . . . . . 7 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓:𝒫 𝐵⟶𝒫 𝐵)
8718adantr 480 . . . . . . . 8 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝒫 𝐵 ∈ V)
8887, 87elmapd 8880 . . . . . . 7 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵))
8986, 88mpbird 257 . . . . . 6 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵))
9089adantrl 716 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → 𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵))
91 simplr 769 . . . . . . . . . . . 12 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))
92 difeq2 4120 . . . . . . . . . . . . . . 15 (𝑧 = 𝑢 → (𝐵𝑧) = (𝐵𝑢))
9392fveq2d 6910 . . . . . . . . . . . . . 14 (𝑧 = 𝑢 → (𝑔‘(𝐵𝑧)) = (𝑔‘(𝐵𝑢)))
9493difeq2d 4126 . . . . . . . . . . . . 13 (𝑧 = 𝑢 → (𝐵 ∖ (𝑔‘(𝐵𝑧))) = (𝐵 ∖ (𝑔‘(𝐵𝑢))))
9594cbvmptv 5255 . . . . . . . . . . . 12 (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑢))))
9691, 95eqtrdi 2793 . . . . . . . . . . 11 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑢)))))
9729fveq2d 6910 . . . . . . . . . . . . 13 (𝑢 = (𝐵𝑡) → (𝑔‘(𝐵𝑢)) = (𝑔‘(𝐵 ∖ (𝐵𝑡))))
9897difeq2d 4126 . . . . . . . . . . . 12 (𝑢 = (𝐵𝑡) → (𝐵 ∖ (𝑔‘(𝐵𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))))
9998adantl 481 . . . . . . . . . . 11 ((((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵𝑡)) → (𝐵 ∖ (𝑔‘(𝐵𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))))
10038ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵𝑡) ∈ 𝒫 𝐵)
1019difexd 5331 . . . . . . . . . . . 12 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
102101ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
10396, 99, 100, 102fvmptd 7023 . . . . . . . . . 10 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘(𝐵𝑡)) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))))
104103difeq2d 4126 . . . . . . . . 9 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))))
105104adantlrl 720 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))))
10647fveq2d 6910 . . . . . . . . . . 11 (𝑡 ∈ 𝒫 𝐵 → (𝑔‘(𝐵 ∖ (𝐵𝑡))) = (𝑔𝑡))
107106difeq2d 4126 . . . . . . . . . 10 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))) = (𝐵 ∖ (𝑔𝑡)))
108107difeq2d 4126 . . . . . . . . 9 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))))
109108adantl 481 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))))
11018, 18elmapd 8880 . . . . . . . . . . . . 13 (𝜑 → (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵))
111110biimpa 476 . . . . . . . . . . . 12 ((𝜑𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵)) → 𝑔:𝒫 𝐵⟶𝒫 𝐵)
112111ffvelcdmda 7104 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔𝑡) ∈ 𝒫 𝐵)
113112elpwid 4609 . . . . . . . . . 10 (((𝜑𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔𝑡) ⊆ 𝐵)
114 dfss4 4269 . . . . . . . . . 10 ((𝑔𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))) = (𝑔𝑡))
115113, 114sylib 218 . . . . . . . . 9 (((𝜑𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))) = (𝑔𝑡))
116115adantlrr 721 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))) = (𝑔𝑡))
117105, 109, 1163eqtrrd 2782 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔𝑡) = (𝐵 ∖ (𝑓‘(𝐵𝑡))))
118117ralrimiva 3146 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑔𝑡) = (𝐵 ∖ (𝑓‘(𝐵𝑡))))
119 elmapfn 8905 . . . . . . . 8 (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) → 𝑔 Fn 𝒫 𝐵)
120119ad2antrl 728 . . . . . . 7 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → 𝑔 Fn 𝒫 𝐵)
121 difeq2 4120 . . . . . . . . 9 (𝑡 = 𝑠 → (𝐵𝑡) = (𝐵𝑠))
122121fveq2d 6910 . . . . . . . 8 (𝑡 = 𝑠 → (𝑓‘(𝐵𝑡)) = (𝑓‘(𝐵𝑠)))
123122difeq2d 4126 . . . . . . 7 (𝑡 = 𝑠 → (𝐵 ∖ (𝑓‘(𝐵𝑡))) = (𝐵 ∖ (𝑓‘(𝐵𝑠))))
1249difexd 5331 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ V)
125124ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ V)
1269difexd 5331 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵𝑠))) ∈ V)
127126ad2antrr 726 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑠))) ∈ V)
128120, 123, 125, 127fnmptfvd 7061 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → (𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑔𝑡) = (𝐵 ∖ (𝑓‘(𝐵𝑡)))))
129118, 128mpbird 257 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))
13090, 129jca 511 . . . 4 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))))
13172, 130impbida 801 . . 3 (𝜑 → ((𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ↔ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))))
132131mptcnv 6159 . 2 (𝜑(𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) = (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))))
133 dssmapfvd.o . . . 4 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠))))))
134 dssmapfvd.d . . . 4 𝐷 = (𝑂𝐵)
135133, 134, 9dssmapfvd 44030 . . 3 (𝜑𝐷 = (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))))
136135cnveqd 5886 . 2 (𝜑𝐷 = (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))))
137 fveq1 6905 . . . . . . . . 9 (𝑓 = 𝑔 → (𝑓‘(𝑏𝑠)) = (𝑔‘(𝑏𝑠)))
138137difeq2d 4126 . . . . . . . 8 (𝑓 = 𝑔 → (𝑏 ∖ (𝑓‘(𝑏𝑠))) = (𝑏 ∖ (𝑔‘(𝑏𝑠))))
139138mpteq2dv 5244 . . . . . . 7 (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠)))) = (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑠)))))
140 difeq2 4120 . . . . . . . . . 10 (𝑠 = 𝑧 → (𝑏𝑠) = (𝑏𝑧))
141140fveq2d 6910 . . . . . . . . 9 (𝑠 = 𝑧 → (𝑔‘(𝑏𝑠)) = (𝑔‘(𝑏𝑧)))
142141difeq2d 4126 . . . . . . . 8 (𝑠 = 𝑧 → (𝑏 ∖ (𝑔‘(𝑏𝑠))) = (𝑏 ∖ (𝑔‘(𝑏𝑧))))
143142cbvmptv 5255 . . . . . . 7 (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧))))
144139, 143eqtrdi 2793 . . . . . 6 (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧)))))
145144cbvmptv 5255 . . . . 5 (𝑓 ∈ (𝒫 𝑏m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠))))) = (𝑔 ∈ (𝒫 𝑏m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧)))))
146145mpteq2i 5247 . . . 4 (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠)))))) = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧))))))
147133, 146eqtri 2765 . . 3 𝑂 = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧))))))
148147, 134, 9dssmapfvd 44030 . 2 (𝜑𝐷 = (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))))
149132, 136, 1483eqtr4d 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
  Copyright terms: Public domain W3C validator