Mathbox for Richard Penner < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dssmapnvod Structured version   Visualization version   GIF version

Theorem dssmapnvod 41116
 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 488 . . . . . . . . 9 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))
2 difeq2 4022 . . . . . . . . . . . 12 (𝑠 = 𝑡 → (𝐵𝑠) = (𝐵𝑡))
32fveq2d 6662 . . . . . . . . . . 11 (𝑠 = 𝑡 → (𝑓‘(𝐵𝑠)) = (𝑓‘(𝐵𝑡)))
43difeq2d 4028 . . . . . . . . . 10 (𝑠 = 𝑡 → (𝐵 ∖ (𝑓‘(𝐵𝑠))) = (𝐵 ∖ (𝑓‘(𝐵𝑡))))
54cbvmptv 5135 . . . . . . . . 9 (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑡))))
61, 5eqtrdi 2809 . . . . . . . 8 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑡)))))
7 ssun1 4077 . . . . . . . . . . . 12 𝐵 ⊆ (𝐵 ∪ (𝑓‘(𝐵𝑡)))
87sspwi 4508 . . . . . . . . . . 11 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑓‘(𝐵𝑡)))
9 dssmapfvd.b . . . . . . . . . . . 12 (𝜑𝐵𝑉)
10 pwidg 4516 . . . . . . . . . . . 12 (𝐵𝑉𝐵 ∈ 𝒫 𝐵)
119, 10syl 17 . . . . . . . . . . 11 (𝜑𝐵 ∈ 𝒫 𝐵)
128, 11sseldi 3890 . . . . . . . . . 10 (𝜑𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵𝑡))))
13 fvex 6671 . . . . . . . . . . 11 (𝑓‘(𝐵𝑡)) ∈ V
1413elpwun 7490 . . . . . . . . . 10 (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵𝑡))) ↔ (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ 𝒫 𝐵)
1512, 14sylib 221 . . . . . . . . 9 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ 𝒫 𝐵)
1615ad2antrr 725 . . . . . . . 8 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ 𝒫 𝐵)
176, 16fmpt3d 6871 . . . . . . 7 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔:𝒫 𝐵⟶𝒫 𝐵)
189pwexd 5248 . . . . . . . . 9 (𝜑 → 𝒫 𝐵 ∈ V)
1918adantr 484 . . . . . . . 8 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝒫 𝐵 ∈ V)
2019, 19elmapd 8430 . . . . . . 7 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵))
2117, 20mpbird 260 . . . . . 6 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵))
2221adantrl 715 . . . . 5 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → 𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵))
23 simplr 768 . . . . . . . . . . . 12 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))
24 difeq2 4022 . . . . . . . . . . . . . . 15 (𝑠 = 𝑢 → (𝐵𝑠) = (𝐵𝑢))
2524fveq2d 6662 . . . . . . . . . . . . . 14 (𝑠 = 𝑢 → (𝑓‘(𝐵𝑠)) = (𝑓‘(𝐵𝑢)))
2625difeq2d 4028 . . . . . . . . . . . . 13 (𝑠 = 𝑢 → (𝐵 ∖ (𝑓‘(𝐵𝑠))) = (𝐵 ∖ (𝑓‘(𝐵𝑢))))
2726cbvmptv 5135 . . . . . . . . . . . 12 (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑢))))
2823, 27eqtrdi 2809 . . . . . . . . . . 11 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑢)))))
29 difeq2 4022 . . . . . . . . . . . . . 14 (𝑢 = (𝐵𝑡) → (𝐵𝑢) = (𝐵 ∖ (𝐵𝑡)))
3029fveq2d 6662 . . . . . . . . . . . . 13 (𝑢 = (𝐵𝑡) → (𝑓‘(𝐵𝑢)) = (𝑓‘(𝐵 ∖ (𝐵𝑡))))
3130difeq2d 4028 . . . . . . . . . . . 12 (𝑢 = (𝐵𝑡) → (𝐵 ∖ (𝑓‘(𝐵𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))))
3231adantl 485 . . . . . . . . . . 11 ((((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵𝑡)) → (𝐵 ∖ (𝑓‘(𝐵𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))))
33 ssun1 4077 . . . . . . . . . . . . . . 15 𝐵 ⊆ (𝐵𝑡)
3433sspwi 4508 . . . . . . . . . . . . . 14 𝒫 𝐵 ⊆ 𝒫 (𝐵𝑡)
3534, 11sseldi 3890 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ 𝒫 (𝐵𝑡))
36 vex 3413 . . . . . . . . . . . . . 14 𝑡 ∈ V
3736elpwun 7490 . . . . . . . . . . . . 13 (𝐵 ∈ 𝒫 (𝐵𝑡) ↔ (𝐵𝑡) ∈ 𝒫 𝐵)
3835, 37sylib 221 . . . . . . . . . . . 12 (𝜑 → (𝐵𝑡) ∈ 𝒫 𝐵)
3938ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵𝑡) ∈ 𝒫 𝐵)
40 difexg 5197 . . . . . . . . . . . . 13 (𝐵𝑉 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
419, 40syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
4241ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
4328, 32, 39, 42fvmptd 6766 . . . . . . . . . 10 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘(𝐵𝑡)) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))))
4443difeq2d 4028 . . . . . . . . 9 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))))
4544adantlrl 719 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))))
46 elpwi 4503 . . . . . . . . . . . . 13 (𝑡 ∈ 𝒫 𝐵𝑡𝐵)
47 dfss4 4163 . . . . . . . . . . . . 13 (𝑡𝐵 ↔ (𝐵 ∖ (𝐵𝑡)) = 𝑡)
4846, 47sylib 221 . . . . . . . . . . . 12 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵𝑡)) = 𝑡)
4948fveq2d 6662 . . . . . . . . . . 11 (𝑡 ∈ 𝒫 𝐵 → (𝑓‘(𝐵 ∖ (𝐵𝑡))) = (𝑓𝑡))
5049difeq2d 4028 . . . . . . . . . 10 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))) = (𝐵 ∖ (𝑓𝑡)))
5150difeq2d 4028 . . . . . . . . 9 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))))
5251adantl 485 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))))
5318, 18elmapd 8430 . . . . . . . . . . . . 13 (𝜑 → (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵))
5453biimpa 480 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵)) → 𝑓:𝒫 𝐵⟶𝒫 𝐵)
5554ffvelrnda 6842 . . . . . . . . . . 11 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓𝑡) ∈ 𝒫 𝐵)
5655elpwid 4505 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓𝑡) ⊆ 𝐵)
57 dfss4 4163 . . . . . . . . . 10 ((𝑓𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))) = (𝑓𝑡))
5856, 57sylib 221 . . . . . . . . 9 (((𝜑𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))) = (𝑓𝑡))
5958adantlrr 720 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))) = (𝑓𝑡))
6045, 52, 593eqtrrd 2798 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓𝑡) = (𝐵 ∖ (𝑔‘(𝐵𝑡))))
6160ralrimiva 3113 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑓𝑡) = (𝐵 ∖ (𝑔‘(𝐵𝑡))))
62 elmapfn 8447 . . . . . . . 8 (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) → 𝑓 Fn 𝒫 𝐵)
6362ad2antrl 727 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → 𝑓 Fn 𝒫 𝐵)
64 difeq2 4022 . . . . . . . . 9 (𝑡 = 𝑧 → (𝐵𝑡) = (𝐵𝑧))
6564fveq2d 6662 . . . . . . . 8 (𝑡 = 𝑧 → (𝑔‘(𝐵𝑡)) = (𝑔‘(𝐵𝑧)))
6665difeq2d 4028 . . . . . . 7 (𝑡 = 𝑧 → (𝐵 ∖ (𝑔‘(𝐵𝑡))) = (𝐵 ∖ (𝑔‘(𝐵𝑧))))
67 difexg 5197 . . . . . . . . 9 (𝐵𝑉 → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ V)
689, 67syl 17 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ V)
6968ad2antrr 725 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ V)
70 difexg 5197 . . . . . . . . 9 (𝐵𝑉 → (𝐵 ∖ (𝑔‘(𝐵𝑧))) ∈ V)
719, 70syl 17 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵𝑧))) ∈ V)
7271ad2antrr 725 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑧))) ∈ V)
7363, 66, 69, 72fnmptfvd 6802 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → (𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑓𝑡) = (𝐵 ∖ (𝑔‘(𝐵𝑡)))))
7461, 73mpbird 260 . . . . 5 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))
7522, 74jca 515 . . . 4 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))))
76 simpr 488 . . . . . . . . 9 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))
77 difeq2 4022 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝐵𝑧) = (𝐵𝑡))
7877fveq2d 6662 . . . . . . . . . . 11 (𝑧 = 𝑡 → (𝑔‘(𝐵𝑧)) = (𝑔‘(𝐵𝑡)))
7978difeq2d 4028 . . . . . . . . . 10 (𝑧 = 𝑡 → (𝐵 ∖ (𝑔‘(𝐵𝑧))) = (𝐵 ∖ (𝑔‘(𝐵𝑡))))
8079cbvmptv 5135 . . . . . . . . 9 (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑡))))
8176, 80eqtrdi 2809 . . . . . . . 8 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑡)))))
82 ssun1 4077 . . . . . . . . . . . 12 𝐵 ⊆ (𝐵 ∪ (𝑔‘(𝐵𝑡)))
8382sspwi 4508 . . . . . . . . . . 11 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑔‘(𝐵𝑡)))
8483, 11sseldi 3890 . . . . . . . . . 10 (𝜑𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵𝑡))))
85 fvex 6671 . . . . . . . . . . 11 (𝑔‘(𝐵𝑡)) ∈ V
8685elpwun 7490 . . . . . . . . . 10 (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵𝑡))) ↔ (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ 𝒫 𝐵)
8784, 86sylib 221 . . . . . . . . 9 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ 𝒫 𝐵)
8887ad2antrr 725 . . . . . . . 8 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ 𝒫 𝐵)
8981, 88fmpt3d 6871 . . . . . . 7 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓:𝒫 𝐵⟶𝒫 𝐵)
9018adantr 484 . . . . . . . 8 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝒫 𝐵 ∈ V)
9190, 90elmapd 8430 . . . . . . 7 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵))
9289, 91mpbird 260 . . . . . 6 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵))
9392adantrl 715 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → 𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵))
94 simplr 768 . . . . . . . . . . . 12 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))
95 difeq2 4022 . . . . . . . . . . . . . . 15 (𝑧 = 𝑢 → (𝐵𝑧) = (𝐵𝑢))
9695fveq2d 6662 . . . . . . . . . . . . . 14 (𝑧 = 𝑢 → (𝑔‘(𝐵𝑧)) = (𝑔‘(𝐵𝑢)))
9796difeq2d 4028 . . . . . . . . . . . . 13 (𝑧 = 𝑢 → (𝐵 ∖ (𝑔‘(𝐵𝑧))) = (𝐵 ∖ (𝑔‘(𝐵𝑢))))
9897cbvmptv 5135 . . . . . . . . . . . 12 (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑢))))
9994, 98eqtrdi 2809 . . . . . . . . . . 11 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑢)))))
10029fveq2d 6662 . . . . . . . . . . . . 13 (𝑢 = (𝐵𝑡) → (𝑔‘(𝐵𝑢)) = (𝑔‘(𝐵 ∖ (𝐵𝑡))))
101100difeq2d 4028 . . . . . . . . . . . 12 (𝑢 = (𝐵𝑡) → (𝐵 ∖ (𝑔‘(𝐵𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))))
102101adantl 485 . . . . . . . . . . 11 ((((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵𝑡)) → (𝐵 ∖ (𝑔‘(𝐵𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))))
10338ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵𝑡) ∈ 𝒫 𝐵)
104 difexg 5197 . . . . . . . . . . . . 13 (𝐵𝑉 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
1059, 104syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
106105ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
10799, 102, 103, 106fvmptd 6766 . . . . . . . . . 10 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘(𝐵𝑡)) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))))
108107difeq2d 4028 . . . . . . . . 9 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))))
109108adantlrl 719 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))))
11048fveq2d 6662 . . . . . . . . . . 11 (𝑡 ∈ 𝒫 𝐵 → (𝑔‘(𝐵 ∖ (𝐵𝑡))) = (𝑔𝑡))
111110difeq2d 4028 . . . . . . . . . 10 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))) = (𝐵 ∖ (𝑔𝑡)))
112111difeq2d 4028 . . . . . . . . 9 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))))
113112adantl 485 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))))
11418, 18elmapd 8430 . . . . . . . . . . . . 13 (𝜑 → (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵))
115114biimpa 480 . . . . . . . . . . . 12 ((𝜑𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵)) → 𝑔:𝒫 𝐵⟶𝒫 𝐵)
116115ffvelrnda 6842 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔𝑡) ∈ 𝒫 𝐵)
117116elpwid 4505 . . . . . . . . . 10 (((𝜑𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔𝑡) ⊆ 𝐵)
118 dfss4 4163 . . . . . . . . . 10 ((𝑔𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))) = (𝑔𝑡))
119117, 118sylib 221 . . . . . . . . 9 (((𝜑𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))) = (𝑔𝑡))
120119adantlrr 720 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))) = (𝑔𝑡))
121109, 113, 1203eqtrrd 2798 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔𝑡) = (𝐵 ∖ (𝑓‘(𝐵𝑡))))
122121ralrimiva 3113 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑔𝑡) = (𝐵 ∖ (𝑓‘(𝐵𝑡))))
123 elmapfn 8447 . . . . . . . 8 (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) → 𝑔 Fn 𝒫 𝐵)
124123ad2antrl 727 . . . . . . 7 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → 𝑔 Fn 𝒫 𝐵)
125 difeq2 4022 . . . . . . . . 9 (𝑡 = 𝑠 → (𝐵𝑡) = (𝐵𝑠))
126125fveq2d 6662 . . . . . . . 8 (𝑡 = 𝑠 → (𝑓‘(𝐵𝑡)) = (𝑓‘(𝐵𝑠)))
127126difeq2d 4028 . . . . . . 7 (𝑡 = 𝑠 → (𝐵 ∖ (𝑓‘(𝐵𝑡))) = (𝐵 ∖ (𝑓‘(𝐵𝑠))))
128 difexg 5197 . . . . . . . . 9 (𝐵𝑉 → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ V)
1299, 128syl 17 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ V)
130129ad2antrr 725 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ V)
131 difexg 5197 . . . . . . . . 9 (𝐵𝑉 → (𝐵 ∖ (𝑓‘(𝐵𝑠))) ∈ V)
1329, 131syl 17 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵𝑠))) ∈ V)
133132ad2antrr 725 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑠))) ∈ V)
134124, 127, 130, 133fnmptfvd 6802 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → (𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑔𝑡) = (𝐵 ∖ (𝑓‘(𝐵𝑡)))))
135122, 134mpbird 260 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))
13693, 135jca 515 . . . 4 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))))
13775, 136impbida 800 . . 3 (𝜑 → ((𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ↔ (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))))
138137mptcnv 5970 . 2 (𝜑(𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) = (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))))
139 dssmapfvd.o . . . 4 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠))))))
140 dssmapfvd.d . . . 4 𝐷 = (𝑂𝐵)
141139, 140, 9dssmapfvd 41113 . . 3 (𝜑𝐷 = (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))))
142141cnveqd 5715 . 2 (𝜑𝐷 = (𝑓 ∈ (𝒫 𝐵m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))))
143 fveq1 6657 . . . . . . . . 9 (𝑓 = 𝑔 → (𝑓‘(𝑏𝑠)) = (𝑔‘(𝑏𝑠)))
144143difeq2d 4028 . . . . . . . 8 (𝑓 = 𝑔 → (𝑏 ∖ (𝑓‘(𝑏𝑠))) = (𝑏 ∖ (𝑔‘(𝑏𝑠))))
145144mpteq2dv 5128 . . . . . . 7 (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠)))) = (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑠)))))
146 difeq2 4022 . . . . . . . . . 10 (𝑠 = 𝑧 → (𝑏𝑠) = (𝑏𝑧))
147146fveq2d 6662 . . . . . . . . 9 (𝑠 = 𝑧 → (𝑔‘(𝑏𝑠)) = (𝑔‘(𝑏𝑧)))
148147difeq2d 4028 . . . . . . . 8 (𝑠 = 𝑧 → (𝑏 ∖ (𝑔‘(𝑏𝑠))) = (𝑏 ∖ (𝑔‘(𝑏𝑧))))
149148cbvmptv 5135 . . . . . . 7 (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧))))
150145, 149eqtrdi 2809 . . . . . 6 (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧)))))
151150cbvmptv 5135 . . . . 5 (𝑓 ∈ (𝒫 𝑏m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠))))) = (𝑔 ∈ (𝒫 𝑏m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧)))))
152151mpteq2i 5124 . . . 4 (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠)))))) = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧))))))
153139, 152eqtri 2781 . . 3 𝑂 = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧))))))
154153, 140, 9dssmapfvd 41113 . 2 (𝜑𝐷 = (𝑔 ∈ (𝒫 𝐵m 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))))
155138, 142, 1543eqtr4d 2803 1 (𝜑𝐷 = 𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3070  Vcvv 3409   ∖ cdif 3855   ∪ cun 3856   ⊆ wss 3858  𝒫 cpw 4494   ↦ cmpt 5112  ◡ccnv 5523   Fn wfn 6330  ⟶wf 6331  ‘cfv 6335  (class class class)co 7150   ↑m cmap 8416 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7693  df-2nd 7694  df-map 8418 This theorem is referenced by:  dssmapf1od  41117  dssmap2d  41118  ntrclsnvobr  41150  clsneicnv  41203  neicvgnvo  41213  dssmapclsntr  41227
 Copyright terms: Public domain W3C validator