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 38631
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 ↦ (𝑓 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠))))))
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 476 . . . . . . . . 9 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))
2 difeq2 3755 . . . . . . . . . . . 12 (𝑠 = 𝑡 → (𝐵𝑠) = (𝐵𝑡))
32fveq2d 6233 . . . . . . . . . . 11 (𝑠 = 𝑡 → (𝑓‘(𝐵𝑠)) = (𝑓‘(𝐵𝑡)))
43difeq2d 3761 . . . . . . . . . 10 (𝑠 = 𝑡 → (𝐵 ∖ (𝑓‘(𝐵𝑠))) = (𝐵 ∖ (𝑓‘(𝐵𝑡))))
54cbvmptv 4783 . . . . . . . . 9 (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑡))))
61, 5syl6eq 2701 . . . . . . . 8 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑡)))))
7 ssun1 3809 . . . . . . . . . . . 12 𝐵 ⊆ (𝐵 ∪ (𝑓‘(𝐵𝑡)))
8 sspwb 4947 . . . . . . . . . . . 12 (𝐵 ⊆ (𝐵 ∪ (𝑓‘(𝐵𝑡))) ↔ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑓‘(𝐵𝑡))))
97, 8mpbi 220 . . . . . . . . . . 11 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑓‘(𝐵𝑡)))
10 dssmapfvd.b . . . . . . . . . . . 12 (𝜑𝐵𝑉)
11 pwidg 4206 . . . . . . . . . . . 12 (𝐵𝑉𝐵 ∈ 𝒫 𝐵)
1210, 11syl 17 . . . . . . . . . . 11 (𝜑𝐵 ∈ 𝒫 𝐵)
139, 12sseldi 3634 . . . . . . . . . 10 (𝜑𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵𝑡))))
14 fvex 6239 . . . . . . . . . . 11 (𝑓‘(𝐵𝑡)) ∈ V
1514elpwun 7019 . . . . . . . . . 10 (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵𝑡))) ↔ (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ 𝒫 𝐵)
1613, 15sylib 208 . . . . . . . . 9 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ 𝒫 𝐵)
1716ad2antrr 762 . . . . . . . 8 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ 𝒫 𝐵)
186, 17fmpt3d 6426 . . . . . . 7 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔:𝒫 𝐵⟶𝒫 𝐵)
19 pwexg 4880 . . . . . . . . . 10 (𝐵𝑉 → 𝒫 𝐵 ∈ V)
2010, 19syl 17 . . . . . . . . 9 (𝜑 → 𝒫 𝐵 ∈ V)
2120adantr 480 . . . . . . . 8 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝒫 𝐵 ∈ V)
2221, 21elmapd 7913 . . . . . . 7 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵))
2318, 22mpbird 247 . . . . . 6 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵))
2423adantrl 752 . . . . 5 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → 𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵))
25 simplr 807 . . . . . . . . . . . 12 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))
26 difeq2 3755 . . . . . . . . . . . . . . 15 (𝑠 = 𝑢 → (𝐵𝑠) = (𝐵𝑢))
2726fveq2d 6233 . . . . . . . . . . . . . 14 (𝑠 = 𝑢 → (𝑓‘(𝐵𝑠)) = (𝑓‘(𝐵𝑢)))
2827difeq2d 3761 . . . . . . . . . . . . 13 (𝑠 = 𝑢 → (𝐵 ∖ (𝑓‘(𝐵𝑠))) = (𝐵 ∖ (𝑓‘(𝐵𝑢))))
2928cbvmptv 4783 . . . . . . . . . . . 12 (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑢))))
3025, 29syl6eq 2701 . . . . . . . . . . 11 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑢)))))
31 difeq2 3755 . . . . . . . . . . . . . 14 (𝑢 = (𝐵𝑡) → (𝐵𝑢) = (𝐵 ∖ (𝐵𝑡)))
3231fveq2d 6233 . . . . . . . . . . . . 13 (𝑢 = (𝐵𝑡) → (𝑓‘(𝐵𝑢)) = (𝑓‘(𝐵 ∖ (𝐵𝑡))))
3332difeq2d 3761 . . . . . . . . . . . 12 (𝑢 = (𝐵𝑡) → (𝐵 ∖ (𝑓‘(𝐵𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))))
3433adantl 481 . . . . . . . . . . 11 ((((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵𝑡)) → (𝐵 ∖ (𝑓‘(𝐵𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))))
35 ssun1 3809 . . . . . . . . . . . . . . 15 𝐵 ⊆ (𝐵𝑡)
36 sspwb 4947 . . . . . . . . . . . . . . 15 (𝐵 ⊆ (𝐵𝑡) ↔ 𝒫 𝐵 ⊆ 𝒫 (𝐵𝑡))
3735, 36mpbi 220 . . . . . . . . . . . . . 14 𝒫 𝐵 ⊆ 𝒫 (𝐵𝑡)
3837, 12sseldi 3634 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ 𝒫 (𝐵𝑡))
39 vex 3234 . . . . . . . . . . . . . 14 𝑡 ∈ V
4039elpwun 7019 . . . . . . . . . . . . 13 (𝐵 ∈ 𝒫 (𝐵𝑡) ↔ (𝐵𝑡) ∈ 𝒫 𝐵)
4138, 40sylib 208 . . . . . . . . . . . 12 (𝜑 → (𝐵𝑡) ∈ 𝒫 𝐵)
4241ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵𝑡) ∈ 𝒫 𝐵)
43 difexg 4841 . . . . . . . . . . . . 13 (𝐵𝑉 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
4410, 43syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
4544ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
4630, 34, 42, 45fvmptd 6327 . . . . . . . . . 10 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘(𝐵𝑡)) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))))
4746difeq2d 3761 . . . . . . . . 9 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))))
4847adantlrl 756 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))))
49 elpwi 4201 . . . . . . . . . . . . 13 (𝑡 ∈ 𝒫 𝐵𝑡𝐵)
50 dfss4 3891 . . . . . . . . . . . . 13 (𝑡𝐵 ↔ (𝐵 ∖ (𝐵𝑡)) = 𝑡)
5149, 50sylib 208 . . . . . . . . . . . 12 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵𝑡)) = 𝑡)
5251fveq2d 6233 . . . . . . . . . . 11 (𝑡 ∈ 𝒫 𝐵 → (𝑓‘(𝐵 ∖ (𝐵𝑡))) = (𝑓𝑡))
5352difeq2d 3761 . . . . . . . . . 10 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))) = (𝐵 ∖ (𝑓𝑡)))
5453difeq2d 3761 . . . . . . . . 9 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))))
5554adantl 481 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))))
5620, 20elmapd 7913 . . . . . . . . . . . . 13 (𝜑 → (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵))
5756biimpa 500 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) → 𝑓:𝒫 𝐵⟶𝒫 𝐵)
5857ffvelrnda 6399 . . . . . . . . . . 11 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓𝑡) ∈ 𝒫 𝐵)
5958elpwid 4203 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓𝑡) ⊆ 𝐵)
60 dfss4 3891 . . . . . . . . . 10 ((𝑓𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))) = (𝑓𝑡))
6159, 60sylib 208 . . . . . . . . 9 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))) = (𝑓𝑡))
6261adantlrr 757 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))) = (𝑓𝑡))
6348, 55, 623eqtrrd 2690 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓𝑡) = (𝐵 ∖ (𝑔‘(𝐵𝑡))))
6463ralrimiva 2995 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑓𝑡) = (𝐵 ∖ (𝑔‘(𝐵𝑡))))
65 elmapfn 7922 . . . . . . . 8 (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) → 𝑓 Fn 𝒫 𝐵)
6665ad2antrl 764 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → 𝑓 Fn 𝒫 𝐵)
67 difeq2 3755 . . . . . . . . 9 (𝑡 = 𝑧 → (𝐵𝑡) = (𝐵𝑧))
6867fveq2d 6233 . . . . . . . 8 (𝑡 = 𝑧 → (𝑔‘(𝐵𝑡)) = (𝑔‘(𝐵𝑧)))
6968difeq2d 3761 . . . . . . 7 (𝑡 = 𝑧 → (𝐵 ∖ (𝑔‘(𝐵𝑡))) = (𝐵 ∖ (𝑔‘(𝐵𝑧))))
70 difexg 4841 . . . . . . . . 9 (𝐵𝑉 → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ V)
7110, 70syl 17 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ V)
7271ad2antrr 762 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ V)
73 difexg 4841 . . . . . . . . 9 (𝐵𝑉 → (𝐵 ∖ (𝑔‘(𝐵𝑧))) ∈ V)
7410, 73syl 17 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵𝑧))) ∈ V)
7574ad2antrr 762 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑧))) ∈ V)
7666, 69, 72, 75fnmptfvd 6360 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → (𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑓𝑡) = (𝐵 ∖ (𝑔‘(𝐵𝑡)))))
7764, 76mpbird 247 . . . . 5 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))
7824, 77jca 553 . . . 4 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))))
79 simpr 476 . . . . . . . . 9 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))
80 difeq2 3755 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝐵𝑧) = (𝐵𝑡))
8180fveq2d 6233 . . . . . . . . . . 11 (𝑧 = 𝑡 → (𝑔‘(𝐵𝑧)) = (𝑔‘(𝐵𝑡)))
8281difeq2d 3761 . . . . . . . . . 10 (𝑧 = 𝑡 → (𝐵 ∖ (𝑔‘(𝐵𝑧))) = (𝐵 ∖ (𝑔‘(𝐵𝑡))))
8382cbvmptv 4783 . . . . . . . . 9 (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑡))))
8479, 83syl6eq 2701 . . . . . . . 8 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑡)))))
85 ssun1 3809 . . . . . . . . . . . 12 𝐵 ⊆ (𝐵 ∪ (𝑔‘(𝐵𝑡)))
86 sspwb 4947 . . . . . . . . . . . 12 (𝐵 ⊆ (𝐵 ∪ (𝑔‘(𝐵𝑡))) ↔ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑔‘(𝐵𝑡))))
8785, 86mpbi 220 . . . . . . . . . . 11 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑔‘(𝐵𝑡)))
8887, 12sseldi 3634 . . . . . . . . . 10 (𝜑𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵𝑡))))
89 fvex 6239 . . . . . . . . . . 11 (𝑔‘(𝐵𝑡)) ∈ V
9089elpwun 7019 . . . . . . . . . 10 (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵𝑡))) ↔ (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ 𝒫 𝐵)
9188, 90sylib 208 . . . . . . . . 9 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ 𝒫 𝐵)
9291ad2antrr 762 . . . . . . . 8 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ 𝒫 𝐵)
9384, 92fmpt3d 6426 . . . . . . 7 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓:𝒫 𝐵⟶𝒫 𝐵)
9420adantr 480 . . . . . . . 8 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝒫 𝐵 ∈ V)
9594, 94elmapd 7913 . . . . . . 7 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵))
9693, 95mpbird 247 . . . . . 6 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵))
9796adantrl 752 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → 𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵))
98 simplr 807 . . . . . . . . . . . 12 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))
99 difeq2 3755 . . . . . . . . . . . . . . 15 (𝑧 = 𝑢 → (𝐵𝑧) = (𝐵𝑢))
10099fveq2d 6233 . . . . . . . . . . . . . 14 (𝑧 = 𝑢 → (𝑔‘(𝐵𝑧)) = (𝑔‘(𝐵𝑢)))
101100difeq2d 3761 . . . . . . . . . . . . 13 (𝑧 = 𝑢 → (𝐵 ∖ (𝑔‘(𝐵𝑧))) = (𝐵 ∖ (𝑔‘(𝐵𝑢))))
102101cbvmptv 4783 . . . . . . . . . . . 12 (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑢))))
10398, 102syl6eq 2701 . . . . . . . . . . 11 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑢)))))
10431fveq2d 6233 . . . . . . . . . . . . 13 (𝑢 = (𝐵𝑡) → (𝑔‘(𝐵𝑢)) = (𝑔‘(𝐵 ∖ (𝐵𝑡))))
105104difeq2d 3761 . . . . . . . . . . . 12 (𝑢 = (𝐵𝑡) → (𝐵 ∖ (𝑔‘(𝐵𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))))
106105adantl 481 . . . . . . . . . . 11 ((((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵𝑡)) → (𝐵 ∖ (𝑔‘(𝐵𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))))
10741ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵𝑡) ∈ 𝒫 𝐵)
108 difexg 4841 . . . . . . . . . . . . 13 (𝐵𝑉 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
10910, 108syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
110109ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
111103, 106, 107, 110fvmptd 6327 . . . . . . . . . 10 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘(𝐵𝑡)) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))))
112111difeq2d 3761 . . . . . . . . 9 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))))
113112adantlrl 756 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))))
11451fveq2d 6233 . . . . . . . . . . 11 (𝑡 ∈ 𝒫 𝐵 → (𝑔‘(𝐵 ∖ (𝐵𝑡))) = (𝑔𝑡))
115114difeq2d 3761 . . . . . . . . . 10 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))) = (𝐵 ∖ (𝑔𝑡)))
116115difeq2d 3761 . . . . . . . . 9 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))))
117116adantl 481 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))))
11820, 20elmapd 7913 . . . . . . . . . . . . 13 (𝜑 → (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵))
119118biimpa 500 . . . . . . . . . . . 12 ((𝜑𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) → 𝑔:𝒫 𝐵⟶𝒫 𝐵)
120119ffvelrnda 6399 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔𝑡) ∈ 𝒫 𝐵)
121120elpwid 4203 . . . . . . . . . 10 (((𝜑𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔𝑡) ⊆ 𝐵)
122 dfss4 3891 . . . . . . . . . 10 ((𝑔𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))) = (𝑔𝑡))
123121, 122sylib 208 . . . . . . . . 9 (((𝜑𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))) = (𝑔𝑡))
124123adantlrr 757 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))) = (𝑔𝑡))
125113, 117, 1243eqtrrd 2690 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔𝑡) = (𝐵 ∖ (𝑓‘(𝐵𝑡))))
126125ralrimiva 2995 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑔𝑡) = (𝐵 ∖ (𝑓‘(𝐵𝑡))))
127 elmapfn 7922 . . . . . . . 8 (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) → 𝑔 Fn 𝒫 𝐵)
128127ad2antrl 764 . . . . . . 7 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → 𝑔 Fn 𝒫 𝐵)
129 difeq2 3755 . . . . . . . . 9 (𝑡 = 𝑠 → (𝐵𝑡) = (𝐵𝑠))
130129fveq2d 6233 . . . . . . . 8 (𝑡 = 𝑠 → (𝑓‘(𝐵𝑡)) = (𝑓‘(𝐵𝑠)))
131130difeq2d 3761 . . . . . . 7 (𝑡 = 𝑠 → (𝐵 ∖ (𝑓‘(𝐵𝑡))) = (𝐵 ∖ (𝑓‘(𝐵𝑠))))
132 difexg 4841 . . . . . . . . 9 (𝐵𝑉 → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ V)
13310, 132syl 17 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ V)
134133ad2antrr 762 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ V)
135 difexg 4841 . . . . . . . . 9 (𝐵𝑉 → (𝐵 ∖ (𝑓‘(𝐵𝑠))) ∈ V)
13610, 135syl 17 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵𝑠))) ∈ V)
137136ad2antrr 762 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑠))) ∈ V)
138128, 131, 134, 137fnmptfvd 6360 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → (𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑔𝑡) = (𝐵 ∖ (𝑓‘(𝐵𝑡)))))
139126, 138mpbird 247 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))
14097, 139jca 553 . . . 4 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))))
14178, 140impbida 895 . . 3 (𝜑 → ((𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ↔ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))))
142141mptcnv 5569 . 2 (𝜑(𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) = (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))))
143 dssmapfvd.o . . . 4 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠))))))
144 dssmapfvd.d . . . 4 𝐷 = (𝑂𝐵)
145143, 144, 10dssmapfvd 38628 . . 3 (𝜑𝐷 = (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))))
146145cnveqd 5330 . 2 (𝜑𝐷 = (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))))
147 fveq1 6228 . . . . . . . . 9 (𝑓 = 𝑔 → (𝑓‘(𝑏𝑠)) = (𝑔‘(𝑏𝑠)))
148147difeq2d 3761 . . . . . . . 8 (𝑓 = 𝑔 → (𝑏 ∖ (𝑓‘(𝑏𝑠))) = (𝑏 ∖ (𝑔‘(𝑏𝑠))))
149148mpteq2dv 4778 . . . . . . 7 (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠)))) = (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑠)))))
150 difeq2 3755 . . . . . . . . . 10 (𝑠 = 𝑧 → (𝑏𝑠) = (𝑏𝑧))
151150fveq2d 6233 . . . . . . . . 9 (𝑠 = 𝑧 → (𝑔‘(𝑏𝑠)) = (𝑔‘(𝑏𝑧)))
152151difeq2d 3761 . . . . . . . 8 (𝑠 = 𝑧 → (𝑏 ∖ (𝑔‘(𝑏𝑠))) = (𝑏 ∖ (𝑔‘(𝑏𝑧))))
153152cbvmptv 4783 . . . . . . 7 (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧))))
154149, 153syl6eq 2701 . . . . . 6 (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧)))))
155154cbvmptv 4783 . . . . 5 (𝑓 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠))))) = (𝑔 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧)))))
156155mpteq2i 4774 . . . 4 (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠)))))) = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧))))))
157143, 156eqtri 2673 . . 3 𝑂 = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧))))))
158157, 144, 10dssmapfvd 38628 . 2 (𝜑𝐷 = (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))))
159142, 146, 1583eqtr4d 2695 1 (𝜑𝐷 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wcel 2030  wral 2941  Vcvv 3231  cdif 3604  cun 3605  wss 3607  𝒫 cpw 4191  cmpt 4762  ccnv 5142   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  𝑚 cmap 7899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-map 7901
This theorem is referenced by:  dssmapf1od  38632  dssmap2d  38633  ntrclsnvobr  38667  clsneicnv  38720  neicvgnvo  38730  dssmapclsntr  38744
  Copyright terms: Public domain W3C validator