Step | Hyp | Ref
| Expression |
1 | | vpwex 4775 |
. . . . . . 7
⊢ 𝒫
𝑡 ∈ V |
2 | 1 | inex2 4728 |
. . . . . 6
⊢ (𝐽 ∩ 𝒫 𝑡) ∈ V |
3 | 2 | uniex 6851 |
. . . . 5
⊢ ∪ (𝐽
∩ 𝒫 𝑡) ∈
V |
4 | 3 | rgenw 2908 |
. . . 4
⊢
∀𝑡 ∈
𝒫 𝑋∪ (𝐽
∩ 𝒫 𝑡) ∈
V |
5 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑡𝒫 𝑋 |
6 | 5 | fnmptf 5929 |
. . . 4
⊢
(∀𝑡 ∈
𝒫 𝑋∪ (𝐽
∩ 𝒫 𝑡) ∈ V
→ (𝑡 ∈ 𝒫
𝑋 ↦ ∪ (𝐽
∩ 𝒫 𝑡)) Fn
𝒫 𝑋) |
7 | 4, 6 | mp1i 13 |
. . 3
⊢ (𝐽 ∈ Top → (𝑡 ∈ 𝒫 𝑋 ↦ ∪ (𝐽
∩ 𝒫 𝑡)) Fn
𝒫 𝑋) |
8 | | dssmapclsntr.i |
. . . . 5
⊢ 𝐼 = (int‘𝐽) |
9 | | dssmapclsntr.x |
. . . . . 6
⊢ 𝑋 = ∪
𝐽 |
10 | 9 | ntrfval 20638 |
. . . . 5
⊢ (𝐽 ∈ Top →
(int‘𝐽) = (𝑡 ∈ 𝒫 𝑋 ↦ ∪ (𝐽
∩ 𝒫 𝑡))) |
11 | 8, 10 | syl5eq 2656 |
. . . 4
⊢ (𝐽 ∈ Top → 𝐼 = (𝑡 ∈ 𝒫 𝑋 ↦ ∪ (𝐽 ∩ 𝒫 𝑡))) |
12 | 11 | fneq1d 5895 |
. . 3
⊢ (𝐽 ∈ Top → (𝐼 Fn 𝒫 𝑋 ↔ (𝑡 ∈ 𝒫 𝑋 ↦ ∪ (𝐽 ∩ 𝒫 𝑡)) Fn 𝒫 𝑋)) |
13 | 7, 12 | mpbird 246 |
. 2
⊢ (𝐽 ∈ Top → 𝐼 Fn 𝒫 𝑋) |
14 | | dssmapclsntr.o |
. . . . . 6
⊢ 𝑂 = (𝑏 ∈ V ↦ (𝑓 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏) ↦ (𝑠 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ (𝑓‘(𝑏 ∖ 𝑠)))))) |
15 | | dssmapclsntr.d |
. . . . . 6
⊢ 𝐷 = (𝑂‘𝑋) |
16 | 9 | topopn 20536 |
. . . . . 6
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
17 | 14, 15, 16 | dssmapf1od 37335 |
. . . . 5
⊢ (𝐽 ∈ Top → 𝐷:(𝒫 𝑋 ↑𝑚 𝒫 𝑋)–1-1-onto→(𝒫 𝑋 ↑𝑚 𝒫 𝑋)) |
18 | | f1of 6050 |
. . . . 5
⊢ (𝐷:(𝒫 𝑋 ↑𝑚 𝒫 𝑋)–1-1-onto→(𝒫 𝑋 ↑𝑚 𝒫 𝑋) → 𝐷:(𝒫 𝑋 ↑𝑚 𝒫 𝑋)⟶(𝒫 𝑋 ↑𝑚
𝒫 𝑋)) |
19 | 17, 18 | syl 17 |
. . . 4
⊢ (𝐽 ∈ Top → 𝐷:(𝒫 𝑋 ↑𝑚 𝒫 𝑋)⟶(𝒫 𝑋 ↑𝑚
𝒫 𝑋)) |
20 | | dssmapclsntr.k |
. . . . 5
⊢ 𝐾 = (cls‘𝐽) |
21 | 9, 20 | clselmap 37445 |
. . . 4
⊢ (𝐽 ∈ Top → 𝐾 ∈ (𝒫 𝑋 ↑𝑚
𝒫 𝑋)) |
22 | 19, 21 | ffvelrnd 6268 |
. . 3
⊢ (𝐽 ∈ Top → (𝐷‘𝐾) ∈ (𝒫 𝑋 ↑𝑚 𝒫 𝑋)) |
23 | | elmapfn 7766 |
. . 3
⊢ ((𝐷‘𝐾) ∈ (𝒫 𝑋 ↑𝑚 𝒫 𝑋) → (𝐷‘𝐾) Fn 𝒫 𝑋) |
24 | 22, 23 | syl 17 |
. 2
⊢ (𝐽 ∈ Top → (𝐷‘𝐾) Fn 𝒫 𝑋) |
25 | | elpwi 4117 |
. . . . 5
⊢ (𝑡 ∈ 𝒫 𝑋 → 𝑡 ⊆ 𝑋) |
26 | 9 | ntrval2 20665 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑡 ⊆ 𝑋) → ((int‘𝐽)‘𝑡) = (𝑋 ∖ ((cls‘𝐽)‘(𝑋 ∖ 𝑡)))) |
27 | 25, 26 | sylan2 490 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑡 ∈ 𝒫 𝑋) → ((int‘𝐽)‘𝑡) = (𝑋 ∖ ((cls‘𝐽)‘(𝑋 ∖ 𝑡)))) |
28 | 8 | fveq1i 6104 |
. . . 4
⊢ (𝐼‘𝑡) = ((int‘𝐽)‘𝑡) |
29 | 20 | fveq1i 6104 |
. . . . 5
⊢ (𝐾‘(𝑋 ∖ 𝑡)) = ((cls‘𝐽)‘(𝑋 ∖ 𝑡)) |
30 | 29 | difeq2i 3687 |
. . . 4
⊢ (𝑋 ∖ (𝐾‘(𝑋 ∖ 𝑡))) = (𝑋 ∖ ((cls‘𝐽)‘(𝑋 ∖ 𝑡))) |
31 | 27, 28, 30 | 3eqtr4g 2669 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑡 ∈ 𝒫 𝑋) → (𝐼‘𝑡) = (𝑋 ∖ (𝐾‘(𝑋 ∖ 𝑡)))) |
32 | 16 | adantr 480 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑡 ∈ 𝒫 𝑋) → 𝑋 ∈ 𝐽) |
33 | 21 | adantr 480 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑡 ∈ 𝒫 𝑋) → 𝐾 ∈ (𝒫 𝑋 ↑𝑚 𝒫 𝑋)) |
34 | | eqid 2610 |
. . . 4
⊢ (𝐷‘𝐾) = (𝐷‘𝐾) |
35 | | simpr 476 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑡 ∈ 𝒫 𝑋) → 𝑡 ∈ 𝒫 𝑋) |
36 | | eqid 2610 |
. . . 4
⊢ ((𝐷‘𝐾)‘𝑡) = ((𝐷‘𝐾)‘𝑡) |
37 | 14, 15, 32, 33, 34, 35, 36 | dssmapfv3d 37333 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑡 ∈ 𝒫 𝑋) → ((𝐷‘𝐾)‘𝑡) = (𝑋 ∖ (𝐾‘(𝑋 ∖ 𝑡)))) |
38 | 31, 37 | eqtr4d 2647 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑡 ∈ 𝒫 𝑋) → (𝐼‘𝑡) = ((𝐷‘𝐾)‘𝑡)) |
39 | 13, 24, 38 | eqfnfvd 6222 |
1
⊢ (𝐽 ∈ Top → 𝐼 = (𝐷‘𝐾)) |