| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) |
| 2 | | difeq2 4120 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑡 → (𝐵 ∖ 𝑠) = (𝐵 ∖ 𝑡)) |
| 3 | 2 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑡 → (𝑓‘(𝐵 ∖ 𝑠)) = (𝑓‘(𝐵 ∖ 𝑡))) |
| 4 | 3 | difeq2d 4126 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑡 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡)))) |
| 5 | 4 | cbvmptv 5255 |
. . . . . . . . 9
⊢ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡)))) |
| 6 | 1, 5 | eqtrdi 2793 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))) |
| 7 | | ssun1 4178 |
. . . . . . . . . . . 12
⊢ 𝐵 ⊆ (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡))) |
| 8 | 7 | sspwi 4612 |
. . . . . . . . . . 11
⊢ 𝒫
𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡))) |
| 9 | | dssmapfvd.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
| 10 | | pwidg 4620 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ 𝒫 𝐵) |
| 11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵) |
| 12 | 8, 11 | sselid 3981 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡)))) |
| 13 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝑓‘(𝐵 ∖ 𝑡)) ∈ V |
| 14 | 13 | elpwun 7789 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵) |
| 15 | 12, 14 | sylib 218 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵) |
| 16 | 15 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵) |
| 17 | 6, 16 | fmpt3d 7136 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔:𝒫 𝐵⟶𝒫 𝐵) |
| 18 | 9 | pwexd 5379 |
. . . . . . . . 9
⊢ (𝜑 → 𝒫 𝐵 ∈ V) |
| 19 | 18 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝒫 𝐵 ∈ V) |
| 20 | 19, 19 | elmapd 8880 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵)) |
| 21 | 17, 20 | mpbird 257 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) |
| 22 | 21 | adantrl 716 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → 𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) |
| 23 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) |
| 24 | | difeq2 4120 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = 𝑢 → (𝐵 ∖ 𝑠) = (𝐵 ∖ 𝑢)) |
| 25 | 24 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑢 → (𝑓‘(𝐵 ∖ 𝑠)) = (𝑓‘(𝐵 ∖ 𝑢))) |
| 26 | 25 | difeq2d 4126 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑢 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢)))) |
| 27 | 26 | cbvmptv 5255 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢)))) |
| 28 | 23, 27 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))))) |
| 29 | | difeq2 4120 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝐵 ∖ 𝑢) = (𝐵 ∖ (𝐵 ∖ 𝑡))) |
| 30 | 29 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝑓‘(𝐵 ∖ 𝑢)) = (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) |
| 31 | 30 | difeq2d 4126 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) |
| 32 | 31 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵 ∖ 𝑡)) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) |
| 33 | | ssun1 4178 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 ⊆ (𝐵 ∪ 𝑡) |
| 34 | 33 | sspwi 4612 |
. . . . . . . . . . . . . 14
⊢ 𝒫
𝐵 ⊆ 𝒫 (𝐵 ∪ 𝑡) |
| 35 | 34, 11 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ 𝒫 (𝐵 ∪ 𝑡)) |
| 36 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑡 ∈ V |
| 37 | 36 | elpwun 7789 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ 𝒫 (𝐵 ∪ 𝑡) ↔ (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) |
| 38 | 35, 37 | sylib 218 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) |
| 39 | 38 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) |
| 40 | 9 | difexd 5331 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V) |
| 41 | 40 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V) |
| 42 | 28, 32, 39, 41 | fvmptd 7023 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘(𝐵 ∖ 𝑡)) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) |
| 43 | 42 | difeq2d 4126 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))) |
| 44 | 43 | adantlrl 720 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))) |
| 45 | | elpwi 4607 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝒫 𝐵 → 𝑡 ⊆ 𝐵) |
| 46 | | dfss4 4269 |
. . . . . . . . . . . . 13
⊢ (𝑡 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑡)) = 𝑡) |
| 47 | 45, 46 | sylib 218 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑡)) = 𝑡) |
| 48 | 47 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))) = (𝑓‘𝑡)) |
| 49 | 48 | difeq2d 4126 |
. . . . . . . . . 10
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) = (𝐵 ∖ (𝑓‘𝑡))) |
| 50 | 49 | difeq2d 4126 |
. . . . . . . . 9
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡)))) |
| 51 | 50 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡)))) |
| 52 | 18, 18 | elmapd 8880 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵)) |
| 53 | 52 | biimpa 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) → 𝑓:𝒫 𝐵⟶𝒫 𝐵) |
| 54 | 53 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘𝑡) ∈ 𝒫 𝐵) |
| 55 | 54 | elpwid 4609 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘𝑡) ⊆ 𝐵) |
| 56 | | dfss4 4269 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))) = (𝑓‘𝑡)) |
| 57 | 55, 56 | sylib 218 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))) = (𝑓‘𝑡)) |
| 58 | 57 | adantlrr 721 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))) = (𝑓‘𝑡)) |
| 59 | 44, 51, 58 | 3eqtrrd 2782 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘𝑡) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡)))) |
| 60 | 59 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑓‘𝑡) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡)))) |
| 61 | | elmapfn 8905 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) → 𝑓 Fn 𝒫 𝐵) |
| 62 | 61 | ad2antrl 728 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → 𝑓 Fn 𝒫 𝐵) |
| 63 | | difeq2 4120 |
. . . . . . . . 9
⊢ (𝑡 = 𝑧 → (𝐵 ∖ 𝑡) = (𝐵 ∖ 𝑧)) |
| 64 | 63 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑡 = 𝑧 → (𝑔‘(𝐵 ∖ 𝑡)) = (𝑔‘(𝐵 ∖ 𝑧))) |
| 65 | 64 | difeq2d 4126 |
. . . . . . 7
⊢ (𝑡 = 𝑧 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) |
| 66 | 9 | difexd 5331 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ V) |
| 67 | 66 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ V) |
| 68 | 9 | difexd 5331 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) ∈ V) |
| 69 | 68 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) ∈ V) |
| 70 | 62, 65, 67, 69 | fnmptfvd 7061 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → (𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑓‘𝑡) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))) |
| 71 | 60, 70 | mpbird 257 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) |
| 72 | 22, 71 | jca 511 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) |
| 73 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) |
| 74 | | difeq2 4120 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑡 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑡)) |
| 75 | 74 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑡 → (𝑔‘(𝐵 ∖ 𝑧)) = (𝑔‘(𝐵 ∖ 𝑡))) |
| 76 | 75 | difeq2d 4126 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑡 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡)))) |
| 77 | 76 | cbvmptv 5255 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡)))) |
| 78 | 73, 77 | eqtrdi 2793 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))) |
| 79 | | ssun1 4178 |
. . . . . . . . . . . 12
⊢ 𝐵 ⊆ (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡))) |
| 80 | 79 | sspwi 4612 |
. . . . . . . . . . 11
⊢ 𝒫
𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡))) |
| 81 | 80, 11 | sselid 3981 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡)))) |
| 82 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝑔‘(𝐵 ∖ 𝑡)) ∈ V |
| 83 | 82 | elpwun 7789 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵) |
| 84 | 81, 83 | sylib 218 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵) |
| 85 | 84 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵) |
| 86 | 78, 85 | fmpt3d 7136 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓:𝒫 𝐵⟶𝒫 𝐵) |
| 87 | 18 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝒫 𝐵 ∈ V) |
| 88 | 87, 87 | elmapd 8880 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵)) |
| 89 | 86, 88 | mpbird 257 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) |
| 90 | 89 | adantrl 716 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → 𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) |
| 91 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) |
| 92 | | difeq2 4120 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑢 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑢)) |
| 93 | 92 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑢 → (𝑔‘(𝐵 ∖ 𝑧)) = (𝑔‘(𝐵 ∖ 𝑢))) |
| 94 | 93 | difeq2d 4126 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑢 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢)))) |
| 95 | 94 | cbvmptv 5255 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢)))) |
| 96 | 91, 95 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))))) |
| 97 | 29 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝑔‘(𝐵 ∖ 𝑢)) = (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) |
| 98 | 97 | difeq2d 4126 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) |
| 99 | 98 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵 ∖ 𝑡)) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) |
| 100 | 38 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) |
| 101 | 9 | difexd 5331 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V) |
| 102 | 101 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V) |
| 103 | 96, 99, 100, 102 | fvmptd 7023 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘(𝐵 ∖ 𝑡)) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) |
| 104 | 103 | difeq2d 4126 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))) |
| 105 | 104 | adantlrl 720 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))) |
| 106 | 47 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))) = (𝑔‘𝑡)) |
| 107 | 106 | difeq2d 4126 |
. . . . . . . . . 10
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) = (𝐵 ∖ (𝑔‘𝑡))) |
| 108 | 107 | difeq2d 4126 |
. . . . . . . . 9
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡)))) |
| 109 | 108 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡)))) |
| 110 | 18, 18 | elmapd 8880 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵)) |
| 111 | 110 | biimpa 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) → 𝑔:𝒫 𝐵⟶𝒫 𝐵) |
| 112 | 111 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘𝑡) ∈ 𝒫 𝐵) |
| 113 | 112 | elpwid 4609 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘𝑡) ⊆ 𝐵) |
| 114 | | dfss4 4269 |
. . . . . . . . . 10
⊢ ((𝑔‘𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))) = (𝑔‘𝑡)) |
| 115 | 113, 114 | sylib 218 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))) = (𝑔‘𝑡)) |
| 116 | 115 | adantlrr 721 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))) = (𝑔‘𝑡)) |
| 117 | 105, 109,
116 | 3eqtrrd 2782 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘𝑡) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡)))) |
| 118 | 117 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑔‘𝑡) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡)))) |
| 119 | | elmapfn 8905 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) → 𝑔 Fn 𝒫 𝐵) |
| 120 | 119 | ad2antrl 728 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → 𝑔 Fn 𝒫 𝐵) |
| 121 | | difeq2 4120 |
. . . . . . . . 9
⊢ (𝑡 = 𝑠 → (𝐵 ∖ 𝑡) = (𝐵 ∖ 𝑠)) |
| 122 | 121 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑡 = 𝑠 → (𝑓‘(𝐵 ∖ 𝑡)) = (𝑓‘(𝐵 ∖ 𝑠))) |
| 123 | 122 | difeq2d 4126 |
. . . . . . 7
⊢ (𝑡 = 𝑠 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) |
| 124 | 9 | difexd 5331 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ V) |
| 125 | 124 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ V) |
| 126 | 9 | difexd 5331 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) ∈ V) |
| 127 | 126 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) ∈ V) |
| 128 | 120, 123,
125, 127 | fnmptfvd 7061 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → (𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑔‘𝑡) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))) |
| 129 | 118, 128 | mpbird 257 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) |
| 130 | 90, 129 | jca 511 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) |
| 131 | 72, 130 | impbida 801 |
. . 3
⊢ (𝜑 → ((𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ↔ (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))))) |
| 132 | 131 | mptcnv 6159 |
. 2
⊢ (𝜑 → ◡(𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) = (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) |
| 133 | | dssmapfvd.o |
. . . 4
⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))))) |
| 134 | | dssmapfvd.d |
. . . 4
⊢ 𝐷 = (𝑂‘𝐵) |
| 135 | 133, 134,
9 | dssmapfvd 44030 |
. . 3
⊢ (𝜑 → 𝐷 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) |
| 136 | 135 | cnveqd 5886 |
. 2
⊢ (𝜑 → ◡𝐷 = ◡(𝑓 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) |
| 137 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (𝑓‘(𝑏 ∖ 𝑠)) = (𝑔‘(𝑏 ∖ 𝑠))) |
| 138 | 137 | difeq2d 4126 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))) = (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠)))) |
| 139 | 138 | mpteq2dv 5244 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))) = (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠))))) |
| 140 | | difeq2 4120 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑧 → (𝑏 ∖ 𝑠) = (𝑏 ∖ 𝑧)) |
| 141 | 140 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑠 = 𝑧 → (𝑔‘(𝑏 ∖ 𝑠)) = (𝑔‘(𝑏 ∖ 𝑧))) |
| 142 | 141 | difeq2d 4126 |
. . . . . . . 8
⊢ (𝑠 = 𝑧 → (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠))) = (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧)))) |
| 143 | 142 | cbvmptv 5255 |
. . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧)))) |
| 144 | 139, 143 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))) |
| 145 | 144 | cbvmptv 5255 |
. . . . 5
⊢ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫
𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))) = (𝑔 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))) |
| 146 | 145 | mpteq2i 5247 |
. . . 4
⊢ (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑m 𝒫
𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))))) = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧)))))) |
| 147 | 133, 146 | eqtri 2765 |
. . 3
⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧)))))) |
| 148 | 147, 134,
9 | dssmapfvd 44030 |
. 2
⊢ (𝜑 → 𝐷 = (𝑔 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) |
| 149 | 132, 136,
148 | 3eqtr4d 2787 |
1
⊢ (𝜑 → ◡𝐷 = 𝐷) |