Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) |
2 | | difeq2 3722 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑡 → (𝐵 ∖ 𝑠) = (𝐵 ∖ 𝑡)) |
3 | 2 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑡 → (𝑓‘(𝐵 ∖ 𝑠)) = (𝑓‘(𝐵 ∖ 𝑡))) |
4 | 3 | difeq2d 3728 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑡 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡)))) |
5 | 4 | cbvmptv 4750 |
. . . . . . . . 9
⊢ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡)))) |
6 | 1, 5 | syl6eq 2672 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))) |
7 | | ssun1 3776 |
. . . . . . . . . . . 12
⊢ 𝐵 ⊆ (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡))) |
8 | | sspwb 4917 |
. . . . . . . . . . . 12
⊢ (𝐵 ⊆ (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡))) ↔ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡)))) |
9 | 7, 8 | mpbi 220 |
. . . . . . . . . . 11
⊢ 𝒫
𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡))) |
10 | | dssmapfvd.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
11 | | pwidg 4173 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ 𝒫 𝐵) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵) |
13 | 9, 12 | sseldi 3601 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡)))) |
14 | | fvex 6201 |
. . . . . . . . . . 11
⊢ (𝑓‘(𝐵 ∖ 𝑡)) ∈ V |
15 | 14 | elpwun 6977 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑓‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵) |
16 | 13, 15 | sylib 208 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵) |
17 | 16 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵) |
18 | 6, 17 | fmpt3d 6386 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔:𝒫 𝐵⟶𝒫 𝐵) |
19 | | pwexg 4850 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑉 → 𝒫 𝐵 ∈ V) |
20 | 10, 19 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝒫 𝐵 ∈ V) |
21 | 20 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝒫 𝐵 ∈ V) |
22 | 21, 21 | elmapd 7871 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵)) |
23 | 18, 22 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) → 𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵)) |
24 | 23 | adantrl 752 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → 𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵)) |
25 | | simplr 792 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) |
26 | | difeq2 3722 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = 𝑢 → (𝐵 ∖ 𝑠) = (𝐵 ∖ 𝑢)) |
27 | 26 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑢 → (𝑓‘(𝐵 ∖ 𝑠)) = (𝑓‘(𝐵 ∖ 𝑢))) |
28 | 27 | difeq2d 3728 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑢 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢)))) |
29 | 28 | cbvmptv 4750 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢)))) |
30 | 25, 29 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑔 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))))) |
31 | | difeq2 3722 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝐵 ∖ 𝑢) = (𝐵 ∖ (𝐵 ∖ 𝑡))) |
32 | 31 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝑓‘(𝐵 ∖ 𝑢)) = (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) |
33 | 32 | difeq2d 3728 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) |
34 | 33 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵 ∖ 𝑡)) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) |
35 | | ssun1 3776 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 ⊆ (𝐵 ∪ 𝑡) |
36 | | sspwb 4917 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ⊆ (𝐵 ∪ 𝑡) ↔ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ 𝑡)) |
37 | 35, 36 | mpbi 220 |
. . . . . . . . . . . . . 14
⊢ 𝒫
𝐵 ⊆ 𝒫 (𝐵 ∪ 𝑡) |
38 | 37, 12 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ 𝒫 (𝐵 ∪ 𝑡)) |
39 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑡 ∈ V |
40 | 39 | elpwun 6977 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ 𝒫 (𝐵 ∪ 𝑡) ↔ (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) |
41 | 38, 40 | sylib 208 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) |
42 | 41 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) |
43 | | difexg 4808 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V) |
44 | 10, 43 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V) |
45 | 44 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V) |
46 | 30, 34, 42, 45 | fvmptd 6288 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘(𝐵 ∖ 𝑡)) = (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) |
47 | 46 | difeq2d 3728 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))) |
48 | 47 | adantlrl 756 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))) |
49 | | elpwi 4168 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝒫 𝐵 → 𝑡 ⊆ 𝐵) |
50 | | dfss4 3858 |
. . . . . . . . . . . . 13
⊢ (𝑡 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑡)) = 𝑡) |
51 | 49, 50 | sylib 208 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑡)) = 𝑡) |
52 | 51 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))) = (𝑓‘𝑡)) |
53 | 52 | difeq2d 3728 |
. . . . . . . . . 10
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) = (𝐵 ∖ (𝑓‘𝑡))) |
54 | 53 | difeq2d 3728 |
. . . . . . . . 9
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡)))) |
55 | 54 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡)))) |
56 | 20, 20 | elmapd 7871 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵)) |
57 | 56 | biimpa 501 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵)) → 𝑓:𝒫 𝐵⟶𝒫 𝐵) |
58 | 57 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘𝑡) ∈ 𝒫 𝐵) |
59 | 58 | elpwid 4170 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘𝑡) ⊆ 𝐵) |
60 | | dfss4 3858 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))) = (𝑓‘𝑡)) |
61 | 59, 60 | sylib 208 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))) = (𝑓‘𝑡)) |
62 | 61 | adantlrr 757 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑓‘𝑡))) = (𝑓‘𝑡)) |
63 | 48, 55, 62 | 3eqtrrd 2661 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘𝑡) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡)))) |
64 | 63 | ralrimiva 2966 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑓‘𝑡) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡)))) |
65 | | elmapfn 7880 |
. . . . . . . 8
⊢ (𝑓 ∈ (𝒫 𝐵 ↑𝑚
𝒫 𝐵) → 𝑓 Fn 𝒫 𝐵) |
66 | 65 | ad2antrl 764 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → 𝑓 Fn 𝒫 𝐵) |
67 | | difeq2 3722 |
. . . . . . . . 9
⊢ (𝑡 = 𝑧 → (𝐵 ∖ 𝑡) = (𝐵 ∖ 𝑧)) |
68 | 67 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑡 = 𝑧 → (𝑔‘(𝐵 ∖ 𝑡)) = (𝑔‘(𝐵 ∖ 𝑧))) |
69 | 68 | difeq2d 3728 |
. . . . . . 7
⊢ (𝑡 = 𝑧 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) |
70 | | difexg 4808 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ V) |
71 | 10, 70 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ V) |
72 | 71 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ V) |
73 | | difexg 4808 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) ∈ V) |
74 | 10, 73 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) ∈ V) |
75 | 74 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) ∧ 𝑧 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) ∈ V) |
76 | 66, 69, 72, 75 | fnmptfvd 6320 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → (𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑓‘𝑡) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))) |
77 | 64, 76 | mpbird 247 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) |
78 | 24, 77 | jca 554 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) → (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) |
79 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) |
80 | | difeq2 3722 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑡 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑡)) |
81 | 80 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑡 → (𝑔‘(𝐵 ∖ 𝑧)) = (𝑔‘(𝐵 ∖ 𝑡))) |
82 | 81 | difeq2d 3728 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑡 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡)))) |
83 | 82 | cbvmptv 4750 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡)))) |
84 | 79, 83 | syl6eq 2672 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓 = (𝑡 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))))) |
85 | | ssun1 3776 |
. . . . . . . . . . . 12
⊢ 𝐵 ⊆ (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡))) |
86 | | sspwb 4917 |
. . . . . . . . . . . 12
⊢ (𝐵 ⊆ (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡))) ↔ 𝒫 𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡)))) |
87 | 85, 86 | mpbi 220 |
. . . . . . . . . . 11
⊢ 𝒫
𝐵 ⊆ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡))) |
88 | 87, 12 | sseldi 3601 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡)))) |
89 | | fvex 6201 |
. . . . . . . . . . 11
⊢ (𝑔‘(𝐵 ∖ 𝑡)) ∈ V |
90 | 89 | elpwun 6977 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝒫 (𝐵 ∪ (𝑔‘(𝐵 ∖ 𝑡))) ↔ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵) |
91 | 88, 90 | sylib 208 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵) |
92 | 91 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑡))) ∈ 𝒫 𝐵) |
93 | 84, 92 | fmpt3d 6386 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓:𝒫 𝐵⟶𝒫 𝐵) |
94 | 20 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝒫 𝐵 ∈ V) |
95 | 94, 94 | elmapd 7871 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ↔ 𝑓:𝒫 𝐵⟶𝒫 𝐵)) |
96 | 93, 95 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) → 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵)) |
97 | 96 | adantrl 752 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → 𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵)) |
98 | | simplr 792 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) |
99 | | difeq2 3722 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑢 → (𝐵 ∖ 𝑧) = (𝐵 ∖ 𝑢)) |
100 | 99 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑢 → (𝑔‘(𝐵 ∖ 𝑧)) = (𝑔‘(𝐵 ∖ 𝑢))) |
101 | 100 | difeq2d 3728 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑢 → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢)))) |
102 | 101 | cbvmptv 4750 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))) = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢)))) |
103 | 98, 102 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑓 = (𝑢 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))))) |
104 | 31 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝑔‘(𝐵 ∖ 𝑢)) = (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) |
105 | 104 | difeq2d 3728 |
. . . . . . . . . . . 12
⊢ (𝑢 = (𝐵 ∖ 𝑡) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) |
106 | 105 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑢 = (𝐵 ∖ 𝑡)) → (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑢))) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) |
107 | 41 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) |
108 | | difexg 4808 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V) |
109 | 10, 108 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V) |
110 | 109 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) ∈ V) |
111 | 103, 106,
107, 110 | fvmptd 6288 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑓‘(𝐵 ∖ 𝑡)) = (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) |
112 | 111 | difeq2d 3728 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))) |
113 | 112 | adantlrl 756 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))))) |
114 | 51 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))) = (𝑔‘𝑡)) |
115 | 114 | difeq2d 3728 |
. . . . . . . . . 10
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡)))) = (𝐵 ∖ (𝑔‘𝑡))) |
116 | 115 | difeq2d 3728 |
. . . . . . . . 9
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡)))) |
117 | 116 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘(𝐵 ∖ (𝐵 ∖ 𝑡))))) = (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡)))) |
118 | 20, 20 | elmapd 7871 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ↔ 𝑔:𝒫 𝐵⟶𝒫 𝐵)) |
119 | 118 | biimpa 501 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵)) → 𝑔:𝒫 𝐵⟶𝒫 𝐵) |
120 | 119 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘𝑡) ∈ 𝒫 𝐵) |
121 | 120 | elpwid 4170 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘𝑡) ⊆ 𝐵) |
122 | | dfss4 3858 |
. . . . . . . . . 10
⊢ ((𝑔‘𝑡) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))) = (𝑔‘𝑡)) |
123 | 121, 122 | sylib 208 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))) = (𝑔‘𝑡)) |
124 | 123 | adantlrr 757 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝑔‘𝑡))) = (𝑔‘𝑡)) |
125 | 113, 117,
124 | 3eqtrrd 2661 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑔‘𝑡) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡)))) |
126 | 125 | ralrimiva 2966 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → ∀𝑡 ∈ 𝒫 𝐵(𝑔‘𝑡) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡)))) |
127 | | elmapfn 7880 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝒫 𝐵 ↑𝑚
𝒫 𝐵) → 𝑔 Fn 𝒫 𝐵) |
128 | 127 | ad2antrl 764 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → 𝑔 Fn 𝒫 𝐵) |
129 | | difeq2 3722 |
. . . . . . . . 9
⊢ (𝑡 = 𝑠 → (𝐵 ∖ 𝑡) = (𝐵 ∖ 𝑠)) |
130 | 129 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑡 = 𝑠 → (𝑓‘(𝐵 ∖ 𝑡)) = (𝑓‘(𝐵 ∖ 𝑠))) |
131 | 130 | difeq2d 3728 |
. . . . . . 7
⊢ (𝑡 = 𝑠 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) |
132 | | difexg 4808 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ V) |
133 | 10, 132 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ V) |
134 | 133 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))) ∈ V) |
135 | | difexg 4808 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) ∈ V) |
136 | 10, 135 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) ∈ V) |
137 | 136 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))) ∈ V) |
138 | 128, 131,
134, 137 | fnmptfvd 6320 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → (𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝑔‘𝑡) = (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑡))))) |
139 | 126, 138 | mpbird 247 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) |
140 | 97, 139 | jca 554 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) → (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) |
141 | 78, 140 | impbida 877 |
. . 3
⊢ (𝜑 → ((𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑔 = (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) ↔ (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ∧ 𝑓 = (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧))))))) |
142 | 141 | mptcnv 5534 |
. 2
⊢ (𝜑 → ◡(𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠))))) = (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) |
143 | | dssmapfvd.o |
. . . 4
⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))))) |
144 | | dssmapfvd.d |
. . . 4
⊢ 𝐷 = (𝑂‘𝐵) |
145 | 143, 144,
10 | dssmapfvd 38311 |
. . 3
⊢ (𝜑 → 𝐷 = (𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) |
146 | 145 | cnveqd 5298 |
. 2
⊢ (𝜑 → ◡𝐷 = ◡(𝑓 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ↦ (𝑠 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑓‘(𝐵 ∖ 𝑠)))))) |
147 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (𝑓‘(𝑏 ∖ 𝑠)) = (𝑔‘(𝑏 ∖ 𝑠))) |
148 | 147 | difeq2d 3728 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))) = (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠)))) |
149 | 148 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))) = (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠))))) |
150 | | difeq2 3722 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑧 → (𝑏 ∖ 𝑠) = (𝑏 ∖ 𝑧)) |
151 | 150 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑠 = 𝑧 → (𝑔‘(𝑏 ∖ 𝑠)) = (𝑔‘(𝑏 ∖ 𝑧))) |
152 | 151 | difeq2d 3728 |
. . . . . . . 8
⊢ (𝑠 = 𝑧 → (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠))) = (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧)))) |
153 | 152 | cbvmptv 4750 |
. . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧)))) |
154 | 149, 153 | syl6eq 2672 |
. . . . . 6
⊢ (𝑓 = 𝑔 → (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))) |
155 | 154 | cbvmptv 4750 |
. . . . 5
⊢ (𝑓 ∈ (𝒫 𝑏 ↑𝑚
𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠))))) = (𝑔 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧))))) |
156 | 155 | mpteq2i 4741 |
. . . 4
⊢ (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑𝑚
𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))))) = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧)))))) |
157 | 143, 156 | eqtri 2644 |
. . 3
⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑔 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏) ↦ (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑔‘(𝑏 ∖ 𝑧)))))) |
158 | 157, 144,
10 | dssmapfvd 38311 |
. 2
⊢ (𝜑 → 𝐷 = (𝑔 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵) ↦ (𝑧 ∈ 𝒫 𝐵 ↦ (𝐵 ∖ (𝑔‘(𝐵 ∖ 𝑧)))))) |
159 | 142, 146,
158 | 3eqtr4d 2666 |
1
⊢ (𝜑 → ◡𝐷 = 𝐷) |