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 37835
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 477 . . . . . . . . 9 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))
2 difeq2 3706 . . . . . . . . . . . 12 (𝑠 = 𝑡 → (𝐵𝑠) = (𝐵𝑡))
32fveq2d 6162 . . . . . . . . . . 11 (𝑠 = 𝑡 → (𝑓‘(𝐵𝑠)) = (𝑓‘(𝐵𝑡)))
43difeq2d 3712 . . . . . . . . . 10 (𝑠 = 𝑡 → (𝐵 ∖ (𝑓‘(𝐵𝑠))) = (𝐵 ∖ (𝑓‘(𝐵𝑡))))
54cbvmptv 4720 . . . . . . . . 9 (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑡))))
61, 5syl6eq 2671 . . . . . . . 8 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑡)))))
7 ssun1 3760 . . . . . . . . . . . 12 𝐵 ⊆ (𝐵 ∪ (𝑓‘(𝐵𝑡)))
8 sspwb 4888 . . . . . . . . . . . 12 (𝐵 ⊆ (𝐵 ∪ (𝑓‘(𝐵𝑡))) ↔ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑓‘(𝐵𝑡))))
97, 8mpbi 220 . . . . . . . . . . 11 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑓‘(𝐵𝑡)))
10 dssmapfvd.b . . . . . . . . . . . 12 (𝜑𝐵𝑉)
11 pwidg 4151 . . . . . . . . . . . 12 (𝐵𝑉𝐵 ∈ 𝒫 𝐵)
1210, 11syl 17 . . . . . . . . . . 11 (𝜑𝐵 ∈ 𝒫 𝐵)
139, 12sseldi 3586 . . . . . . . . . 10 (𝜑𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵𝑡))))
14 fvex 6168 . . . . . . . . . . 11 (𝑓‘(𝐵𝑡)) ∈ V
1514elpwun 6939 . . . . . . . . . 10 (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵𝑡))) ↔ (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ 𝒫 𝐵)
1613, 15sylib 208 . . . . . . . . 9 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ 𝒫 𝐵)
1716ad2antrr 761 . . . . . . . 8 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ 𝒫 𝐵)
186, 17fmpt3d 6352 . . . . . . 7 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔:𝒫 𝐵⟶𝒫 𝐵)
19 pwexg 4820 . . . . . . . . . 10 (𝐵𝑉 → 𝒫 𝐵 ∈ V)
2010, 19syl 17 . . . . . . . . 9 (𝜑 → 𝒫 𝐵 ∈ V)
2120adantr 481 . . . . . . . 8 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝒫 𝐵 ∈ V)
2221, 21elmapd 7831 . . . . . . 7 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵))
2318, 22mpbird 247 . . . . . 6 ((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) → 𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵))
2423adantrl 751 . . . . 5 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → 𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵))
25 simplr 791 . . . . . . . . . . . 12 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))
26 difeq2 3706 . . . . . . . . . . . . . . 15 (𝑠 = 𝑢 → (𝐵𝑠) = (𝐵𝑢))
2726fveq2d 6162 . . . . . . . . . . . . . 14 (𝑠 = 𝑢 → (𝑓‘(𝐵𝑠)) = (𝑓‘(𝐵𝑢)))
2827difeq2d 3712 . . . . . . . . . . . . 13 (𝑠 = 𝑢 → (𝐵 ∖ (𝑓‘(𝐵𝑠))) = (𝐵 ∖ (𝑓‘(𝐵𝑢))))
2928cbvmptv 4720 . . . . . . . . . . . 12 (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑢))))
3025, 29syl6eq 2671 . . . . . . . . . . 11 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑢)))))
31 difeq2 3706 . . . . . . . . . . . . . 14 (𝑢 = (𝐵𝑡) → (𝐵𝑢) = (𝐵 ∖ (𝐵𝑡)))
3231fveq2d 6162 . . . . . . . . . . . . 13 (𝑢 = (𝐵𝑡) → (𝑓‘(𝐵𝑢)) = (𝑓‘(𝐵 ∖ (𝐵𝑡))))
3332difeq2d 3712 . . . . . . . . . . . 12 (𝑢 = (𝐵𝑡) → (𝐵 ∖ (𝑓‘(𝐵𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))))
3433adantl 482 . . . . . . . . . . 11 ((((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵𝑡)) → (𝐵 ∖ (𝑓‘(𝐵𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))))
35 ssun1 3760 . . . . . . . . . . . . . . 15 𝐵 ⊆ (𝐵𝑡)
36 sspwb 4888 . . . . . . . . . . . . . . 15 (𝐵 ⊆ (𝐵𝑡) ↔ 𝒫 𝐵 ⊆ 𝒫 (𝐵𝑡))
3735, 36mpbi 220 . . . . . . . . . . . . . 14 𝒫 𝐵 ⊆ 𝒫 (𝐵𝑡)
3837, 12sseldi 3586 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ 𝒫 (𝐵𝑡))
39 vex 3193 . . . . . . . . . . . . . 14 𝑡 ∈ V
4039elpwun 6939 . . . . . . . . . . . . 13 (𝐵 ∈ 𝒫 (𝐵𝑡) ↔ (𝐵𝑡) ∈ 𝒫 𝐵)
4138, 40sylib 208 . . . . . . . . . . . 12 (𝜑 → (𝐵𝑡) ∈ 𝒫 𝐵)
4241ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵𝑡) ∈ 𝒫 𝐵)
43 difexg 4778 . . . . . . . . . . . . 13 (𝐵𝑉 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
4410, 43syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
4544ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
4630, 34, 42, 45fvmptd 6255 . . . . . . . . . 10 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘(𝐵𝑡)) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))))
4746difeq2d 3712 . . . . . . . . 9 (((𝜑𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))))
4847adantlrl 755 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))))
49 elpwi 4146 . . . . . . . . . . . . 13 (𝑡 ∈ 𝒫 𝐵𝑡𝐵)
50 dfss4 3842 . . . . . . . . . . . . 13 (𝑡𝐵 ↔ (𝐵 ∖ (𝐵𝑡)) = 𝑡)
5149, 50sylib 208 . . . . . . . . . . . 12 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵𝑡)) = 𝑡)
5251fveq2d 6162 . . . . . . . . . . 11 (𝑡 ∈ 𝒫 𝐵 → (𝑓‘(𝐵 ∖ (𝐵𝑡))) = (𝑓𝑡))
5352difeq2d 3712 . . . . . . . . . 10 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡)))) = (𝐵 ∖ (𝑓𝑡)))
5453difeq2d 3712 . . . . . . . . 9 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))))
5554adantl 482 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))))
5620, 20elmapd 7831 . . . . . . . . . . . . 13 (𝜑 → (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵))
5756biimpa 501 . . . . . . . . . . . 12 ((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) → 𝑓:𝒫 𝐵⟶𝒫 𝐵)
5857ffvelrnda 6325 . . . . . . . . . . 11 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓𝑡) ∈ 𝒫 𝐵)
5958elpwid 4148 . . . . . . . . . 10 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓𝑡) ⊆ 𝐵)
60 dfss4 3842 . . . . . . . . . 10 ((𝑓𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))) = (𝑓𝑡))
6159, 60sylib 208 . . . . . . . . 9 (((𝜑𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))) = (𝑓𝑡))
6261adantlrr 756 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓𝑡))) = (𝑓𝑡))
6348, 55, 623eqtrrd 2660 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓𝑡) = (𝐵 ∖ (𝑔‘(𝐵𝑡))))
6463ralrimiva 2962 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑓𝑡) = (𝐵 ∖ (𝑔‘(𝐵𝑡))))
65 elmapfn 7840 . . . . . . . 8 (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) → 𝑓 Fn 𝒫 𝐵)
6665ad2antrl 763 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → 𝑓 Fn 𝒫 𝐵)
67 difeq2 3706 . . . . . . . . 9 (𝑡 = 𝑧 → (𝐵𝑡) = (𝐵𝑧))
6867fveq2d 6162 . . . . . . . 8 (𝑡 = 𝑧 → (𝑔‘(𝐵𝑡)) = (𝑔‘(𝐵𝑧)))
6968difeq2d 3712 . . . . . . 7 (𝑡 = 𝑧 → (𝐵 ∖ (𝑔‘(𝐵𝑡))) = (𝐵 ∖ (𝑔‘(𝐵𝑧))))
70 difexg 4778 . . . . . . . . 9 (𝐵𝑉 → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ V)
7110, 70syl 17 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ V)
7271ad2antrr 761 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ V)
73 difexg 4778 . . . . . . . . 9 (𝐵𝑉 → (𝐵 ∖ (𝑔‘(𝐵𝑧))) ∈ V)
7410, 73syl 17 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵𝑧))) ∈ V)
7574ad2antrr 761 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑧))) ∈ V)
7666, 69, 72, 75fnmptfvd 6286 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → (𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑓𝑡) = (𝐵 ∖ (𝑔‘(𝐵𝑡)))))
7764, 76mpbird 247 . . . . 5 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))
7824, 77jca 554 . . . 4 ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))) → (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))))
79 simpr 477 . . . . . . . . 9 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))
80 difeq2 3706 . . . . . . . . . . . 12 (𝑧 = 𝑡 → (𝐵𝑧) = (𝐵𝑡))
8180fveq2d 6162 . . . . . . . . . . 11 (𝑧 = 𝑡 → (𝑔‘(𝐵𝑧)) = (𝑔‘(𝐵𝑡)))
8281difeq2d 3712 . . . . . . . . . 10 (𝑧 = 𝑡 → (𝐵 ∖ (𝑔‘(𝐵𝑧))) = (𝐵 ∖ (𝑔‘(𝐵𝑡))))
8382cbvmptv 4720 . . . . . . . . 9 (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑡))))
8479, 83syl6eq 2671 . . . . . . . 8 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑡)))))
85 ssun1 3760 . . . . . . . . . . . 12 𝐵 ⊆ (𝐵 ∪ (𝑔‘(𝐵𝑡)))
86 sspwb 4888 . . . . . . . . . . . 12 (𝐵 ⊆ (𝐵 ∪ (𝑔‘(𝐵𝑡))) ↔ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑔‘(𝐵𝑡))))
8785, 86mpbi 220 . . . . . . . . . . 11 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑔‘(𝐵𝑡)))
8887, 12sseldi 3586 . . . . . . . . . 10 (𝜑𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵𝑡))))
89 fvex 6168 . . . . . . . . . . 11 (𝑔‘(𝐵𝑡)) ∈ V
9089elpwun 6939 . . . . . . . . . 10 (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵𝑡))) ↔ (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ 𝒫 𝐵)
9188, 90sylib 208 . . . . . . . . 9 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ 𝒫 𝐵)
9291ad2antrr 761 . . . . . . . 8 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵𝑡))) ∈ 𝒫 𝐵)
9384, 92fmpt3d 6352 . . . . . . 7 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓:𝒫 𝐵⟶𝒫 𝐵)
9420adantr 481 . . . . . . . 8 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝒫 𝐵 ∈ V)
9594, 94elmapd 7831 . . . . . . 7 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵))
9693, 95mpbird 247 . . . . . 6 ((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) → 𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵))
9796adantrl 751 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → 𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵))
98 simplr 791 . . . . . . . . . . . 12 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))
99 difeq2 3706 . . . . . . . . . . . . . . 15 (𝑧 = 𝑢 → (𝐵𝑧) = (𝐵𝑢))
10099fveq2d 6162 . . . . . . . . . . . . . 14 (𝑧 = 𝑢 → (𝑔‘(𝐵𝑧)) = (𝑔‘(𝐵𝑢)))
101100difeq2d 3712 . . . . . . . . . . . . 13 (𝑧 = 𝑢 → (𝐵 ∖ (𝑔‘(𝐵𝑧))) = (𝐵 ∖ (𝑔‘(𝐵𝑢))))
102101cbvmptv 4720 . . . . . . . . . . . 12 (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑢))))
10398, 102syl6eq 2671 . . . . . . . . . . 11 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑢)))))
10431fveq2d 6162 . . . . . . . . . . . . 13 (𝑢 = (𝐵𝑡) → (𝑔‘(𝐵𝑢)) = (𝑔‘(𝐵 ∖ (𝐵𝑡))))
105104difeq2d 3712 . . . . . . . . . . . 12 (𝑢 = (𝐵𝑡) → (𝐵 ∖ (𝑔‘(𝐵𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))))
106105adantl 482 . . . . . . . . . . 11 ((((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵𝑡)) → (𝐵 ∖ (𝑔‘(𝐵𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))))
10741ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵𝑡) ∈ 𝒫 𝐵)
108 difexg 4778 . . . . . . . . . . . . 13 (𝐵𝑉 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
10910, 108syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
110109ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))) ∈ V)
111103, 106, 107, 110fvmptd 6255 . . . . . . . . . 10 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘(𝐵𝑡)) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))))
112111difeq2d 3712 . . . . . . . . 9 (((𝜑𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))))
113112adantlrl 755 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))))
11451fveq2d 6162 . . . . . . . . . . 11 (𝑡 ∈ 𝒫 𝐵 → (𝑔‘(𝐵 ∖ (𝐵𝑡))) = (𝑔𝑡))
115114difeq2d 3712 . . . . . . . . . 10 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡)))) = (𝐵 ∖ (𝑔𝑡)))
116115difeq2d 3712 . . . . . . . . 9 (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))))
117116adantl 482 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))))
11820, 20elmapd 7831 . . . . . . . . . . . . 13 (𝜑 → (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵))
119118biimpa 501 . . . . . . . . . . . 12 ((𝜑𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) → 𝑔:𝒫 𝐵⟶𝒫 𝐵)
120119ffvelrnda 6325 . . . . . . . . . . 11 (((𝜑𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔𝑡) ∈ 𝒫 𝐵)
121120elpwid 4148 . . . . . . . . . 10 (((𝜑𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔𝑡) ⊆ 𝐵)
122 dfss4 3842 . . . . . . . . . 10 ((𝑔𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))) = (𝑔𝑡))
123121, 122sylib 208 . . . . . . . . 9 (((𝜑𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))) = (𝑔𝑡))
124123adantlrr 756 . . . . . . . 8 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔𝑡))) = (𝑔𝑡))
125113, 117, 1243eqtrrd 2660 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔𝑡) = (𝐵 ∖ (𝑓‘(𝐵𝑡))))
126125ralrimiva 2962 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑔𝑡) = (𝐵 ∖ (𝑓‘(𝐵𝑡))))
127 elmapfn 7840 . . . . . . . 8 (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) → 𝑔 Fn 𝒫 𝐵)
128127ad2antrl 763 . . . . . . 7 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → 𝑔 Fn 𝒫 𝐵)
129 difeq2 3706 . . . . . . . . 9 (𝑡 = 𝑠 → (𝐵𝑡) = (𝐵𝑠))
130129fveq2d 6162 . . . . . . . 8 (𝑡 = 𝑠 → (𝑓‘(𝐵𝑡)) = (𝑓‘(𝐵𝑠)))
131130difeq2d 3712 . . . . . . 7 (𝑡 = 𝑠 → (𝐵 ∖ (𝑓‘(𝐵𝑡))) = (𝐵 ∖ (𝑓‘(𝐵𝑠))))
132 difexg 4778 . . . . . . . . 9 (𝐵𝑉 → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ V)
13310, 132syl 17 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ V)
134133ad2antrr 761 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑡))) ∈ V)
135 difexg 4778 . . . . . . . . 9 (𝐵𝑉 → (𝐵 ∖ (𝑓‘(𝐵𝑠))) ∈ V)
13610, 135syl 17 . . . . . . . 8 (𝜑 → (𝐵 ∖ (𝑓‘(𝐵𝑠))) ∈ V)
137136ad2antrr 761 . . . . . . 7 (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵𝑠))) ∈ V)
138128, 131, 134, 137fnmptfvd 6286 . . . . . 6 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → (𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑔𝑡) = (𝐵 ∖ (𝑓‘(𝐵𝑡)))))
139126, 138mpbird 247 . . . . 5 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠)))))
14097, 139jca 554 . . . 4 ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))) → (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))))
14178, 140impbida 876 . . 3 (𝜑 → ((𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) ↔ (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧)))))))
142141mptcnv 5503 . 2 (𝜑(𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))) = (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))))
143 dssmapfvd.o . . . 4 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠))))))
144 dssmapfvd.d . . . 4 𝐷 = (𝑂𝐵)
145143, 144, 10dssmapfvd 37832 . . 3 (𝜑𝐷 = (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))))
146145cnveqd 5268 . 2 (𝜑𝐷 = (𝑓 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵𝑠))))))
147 fveq1 6157 . . . . . . . . 9 (𝑓 = 𝑔 → (𝑓‘(𝑏𝑠)) = (𝑔‘(𝑏𝑠)))
148147difeq2d 3712 . . . . . . . 8 (𝑓 = 𝑔 → (𝑏 ∖ (𝑓‘(𝑏𝑠))) = (𝑏 ∖ (𝑔‘(𝑏𝑠))))
149148mpteq2dv 4715 . . . . . . 7 (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠)))) = (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑠)))))
150 difeq2 3706 . . . . . . . . . 10 (𝑠 = 𝑧 → (𝑏𝑠) = (𝑏𝑧))
151150fveq2d 6162 . . . . . . . . 9 (𝑠 = 𝑧 → (𝑔‘(𝑏𝑠)) = (𝑔‘(𝑏𝑧)))
152151difeq2d 3712 . . . . . . . 8 (𝑠 = 𝑧 → (𝑏 ∖ (𝑔‘(𝑏𝑠))) = (𝑏 ∖ (𝑔‘(𝑏𝑧))))
153152cbvmptv 4720 . . . . . . 7 (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧))))
154149, 153syl6eq 2671 . . . . . 6 (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧)))))
155154cbvmptv 4720 . . . . 5 (𝑓 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠))))) = (𝑔 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧)))))
156155mpteq2i 4711 . . . 4 (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏𝑠)))))) = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧))))))
157143, 156eqtri 2643 . . 3 𝑂 = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏𝑧))))))
158157, 144, 10dssmapfvd 37832 . 2 (𝜑𝐷 = (𝑔 ∈ (𝒫 𝐵𝑚 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵𝑧))))))
159142, 146, 1583eqtr4d 2665 1 (𝜑𝐷 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  wral 2908  Vcvv 3190  cdif 3557  cun 3558  wss 3560  𝒫 cpw 4136  cmpt 4683  ccnv 5083   Fn wfn 5852  wf 5853  cfv 5857  (class class class)co 6615  𝑚 cmap 7817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-reu 2915  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-id 4999  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-1st 7128  df-2nd 7129  df-map 7819
This theorem is referenced by:  dssmapf1od  37836  dssmap2d  37837  ntrclsnvobr  37871  clsneicnv  37924  neicvgnvo  37934  dssmapclsntr  37948
  Copyright terms: Public domain W3C validator