Step | Hyp | Ref
| Expression |
1 | | utoptop.1 |
. . . . . . . 8
⊢ 𝐽 = (unifTop‘𝑈) |
2 | | utopval 22036 |
. . . . . . . 8
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎}) |
3 | 1, 2 | syl5eq 2668 |
. . . . . . 7
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎}) |
4 | | simpll 790 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → 𝑈 ∈ (UnifOn‘𝑋)) |
5 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑎 ∈ 𝒫 𝑋) |
6 | 5 | elpwid 4170 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑎 ⊆ 𝑋) |
7 | 6 | sselda 3603 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → 𝑝 ∈ 𝑋) |
8 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ 𝑋) |
9 | | mptexg 6484 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V) |
10 | | rnexg 7098 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V) |
12 | 11 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V) |
13 | | utopsnneip.2 |
. . . . . . . . . . . . . . 15
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) |
14 | 13 | fvmpt2 6291 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V) → (𝑁‘𝑝) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) |
15 | 8, 12, 14 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) |
16 | 15 | eleq2d 2687 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑎 ∈ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))) |
17 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑎 ∈ V |
18 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) = (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) |
19 | 18 | elrnmpt 5372 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ V → (𝑎 ∈ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))) |
20 | 17, 19 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) |
21 | 16, 20 | syl6bb 276 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))) |
22 | 4, 7, 21 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))) |
23 | | nfv 1843 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑣((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) |
24 | | nfre1 3005 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑣∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}) |
25 | 23, 24 | nfan 1828 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑣(((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) |
26 | | simplr 792 |
. . . . . . . . . . . . 13
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) ∧ 𝑣 ∈ 𝑈) ∧ 𝑎 = (𝑣 “ {𝑝})) → 𝑣 ∈ 𝑈) |
27 | | eqimss2 3658 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑣 “ {𝑝}) → (𝑣 “ {𝑝}) ⊆ 𝑎) |
28 | 27 | adantl 482 |
. . . . . . . . . . . . 13
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) ∧ 𝑣 ∈ 𝑈) ∧ 𝑎 = (𝑣 “ {𝑝})) → (𝑣 “ {𝑝}) ⊆ 𝑎) |
29 | | imaeq1 5461 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑣 → (𝑤 “ {𝑝}) = (𝑣 “ {𝑝})) |
30 | 29 | sseq1d 3632 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑣 → ((𝑤 “ {𝑝}) ⊆ 𝑎 ↔ (𝑣 “ {𝑝}) ⊆ 𝑎)) |
31 | 30 | rspcev 3309 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ 𝑈 ∧ (𝑣 “ {𝑝}) ⊆ 𝑎) → ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎) |
32 | 26, 28, 31 | syl2anc 693 |
. . . . . . . . . . . 12
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) ∧ 𝑣 ∈ 𝑈) ∧ 𝑎 = (𝑣 “ {𝑝})) → ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎) |
33 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) → ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) |
34 | 25, 32, 33 | r19.29af 3076 |
. . . . . . . . . . 11
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) → ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎) |
35 | 4 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑈 ∈ (UnifOn‘𝑋)) |
36 | 7 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑝 ∈ 𝑋) |
37 | 35, 36 | jca 554 |
. . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋)) |
38 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑤 “ {𝑝}) ⊆ 𝑎) |
39 | 6 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑎 ⊆ 𝑋) |
40 | | simplr 792 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑤 ∈ 𝑈) |
41 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 “ {𝑝}) = (𝑤 “ {𝑝}) |
42 | | imaeq1 5461 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑤 → (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})) |
43 | 42 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑤 → ((𝑤 “ {𝑝}) = (𝑢 “ {𝑝}) ↔ (𝑤 “ {𝑝}) = (𝑤 “ {𝑝}))) |
44 | 43 | rspcev 3309 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ 𝑈 ∧ (𝑤 “ {𝑝}) = (𝑤 “ {𝑝})) → ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝})) |
45 | 41, 44 | mpan2 707 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ 𝑈 → ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝})) |
46 | 45 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝})) |
47 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑤 ∈ V |
48 | 47 | imaex 7104 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 “ {𝑝}) ∈ V |
49 | 13 | ustuqtoplem 22043 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ V) → ((𝑤 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))) |
50 | 48, 49 | mpan2 707 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → ((𝑤 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))) |
51 | 50 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ((𝑤 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))) |
52 | 46, 51 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)) |
53 | 35, 36, 40, 52 | syl21anc 1325 |
. . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)) |
54 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ⊆ 𝑎 ↔ (𝑤 “ {𝑝}) ⊆ 𝑎)) |
55 | 54 | 3anbi2d 1404 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑤 “ {𝑝}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋))) |
56 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ∈ (𝑁‘𝑝) ↔ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝))) |
57 | 55, 56 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑤 “ {𝑝}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)))) |
58 | 57 | imbi1d 331 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑤 “ {𝑝}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝)))) |
59 | 13 | ustuqtop1 22045 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝)) |
60 | 48, 58, 59 | vtocl 3259 |
. . . . . . . . . . . . . 14
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝)) |
61 | 37, 38, 39, 53, 60 | syl31anc 1329 |
. . . . . . . . . . . . 13
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑎 ∈ (𝑁‘𝑝)) |
62 | 37, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))) |
63 | 61, 62 | mpbid 222 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) |
64 | 63 | r19.29an 3077 |
. . . . . . . . . . 11
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎) → ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) |
65 | 34, 64 | impbida 877 |
. . . . . . . . . 10
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → (∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}) ↔ ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎)) |
66 | 22, 65 | bitrd 268 |
. . . . . . . . 9
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎)) |
67 | 66 | ralbidva 2985 |
. . . . . . . 8
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝) ↔ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎)) |
68 | 67 | rabbidva 3188 |
. . . . . . 7
⊢ (𝑈 ∈ (UnifOn‘𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎}) |
69 | 3, 68 | eqtr4d 2659 |
. . . . . 6
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}) |
70 | | utopsnneip.1 |
. . . . . 6
⊢ 𝐾 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} |
71 | 69, 70 | syl6eqr 2674 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = 𝐾) |
72 | 71 | fveq2d 6195 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (nei‘𝐽) = (nei‘𝐾)) |
73 | 72 | fveq1d 6193 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ((nei‘𝐽)‘{𝑃}) = ((nei‘𝐾)‘{𝑃})) |
74 | 73 | adantr 481 |
. 2
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ((nei‘𝐾)‘{𝑃})) |
75 | 13 | ustuqtop0 22044 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁:𝑋⟶𝒫 𝒫 𝑋) |
76 | 13 | ustuqtop1 22045 |
. . . . 5
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) |
77 | 13 | ustuqtop2 22046 |
. . . . 5
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) |
78 | 13 | ustuqtop3 22047 |
. . . . 5
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) |
79 | 13 | ustuqtop4 22048 |
. . . . 5
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) |
80 | 13 | ustuqtop5 22049 |
. . . . 5
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) |
81 | 70, 75, 76, 77, 78, 79, 80 | neiptopnei 20936 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐾)‘{𝑝}))) |
82 | 81 | adantr 481 |
. . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐾)‘{𝑝}))) |
83 | | simpr 477 |
. . . . 5
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃) |
84 | 83 | sneqd 4189 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑝 = 𝑃) → {𝑝} = {𝑃}) |
85 | 84 | fveq2d 6195 |
. . 3
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑝 = 𝑃) → ((nei‘𝐾)‘{𝑝}) = ((nei‘𝐾)‘{𝑃})) |
86 | | simpr 477 |
. . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → 𝑃 ∈ 𝑋) |
87 | | fvexd 6203 |
. . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐾)‘{𝑃}) ∈ V) |
88 | 82, 85, 86, 87 | fvmptd 6288 |
. 2
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁‘𝑃) = ((nei‘𝐾)‘{𝑃})) |
89 | | mptexg 6484 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) |
90 | | rnexg 7098 |
. . . . 5
⊢ ((𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) |
91 | 89, 90 | syl 17 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) |
92 | 91 | adantr 481 |
. . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) |
93 | 13 | a1i 11 |
. . . 4
⊢ ((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) → 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))) |
94 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑣 𝑃 ∈ 𝑋 |
95 | | nfmpt1 4747 |
. . . . . . . . . 10
⊢
Ⅎ𝑣(𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) |
96 | 95 | nfrn 5368 |
. . . . . . . . 9
⊢
Ⅎ𝑣ran
(𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) |
97 | 96 | nfel1 2779 |
. . . . . . . 8
⊢
Ⅎ𝑣ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V |
98 | 94, 97 | nfan 1828 |
. . . . . . 7
⊢
Ⅎ𝑣(𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) |
99 | | nfv 1843 |
. . . . . . 7
⊢
Ⅎ𝑣 𝑝 = 𝑃 |
100 | 98, 99 | nfan 1828 |
. . . . . 6
⊢
Ⅎ𝑣((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) |
101 | | simpr2 1068 |
. . . . . . . . 9
⊢ ((𝑃 ∈ 𝑋 ∧ (ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V ∧ 𝑝 = 𝑃 ∧ 𝑣 ∈ 𝑈)) → 𝑝 = 𝑃) |
102 | 101 | sneqd 4189 |
. . . . . . . 8
⊢ ((𝑃 ∈ 𝑋 ∧ (ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V ∧ 𝑝 = 𝑃 ∧ 𝑣 ∈ 𝑈)) → {𝑝} = {𝑃}) |
103 | 102 | imaeq2d 5466 |
. . . . . . 7
⊢ ((𝑃 ∈ 𝑋 ∧ (ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V ∧ 𝑝 = 𝑃 ∧ 𝑣 ∈ 𝑈)) → (𝑣 “ {𝑝}) = (𝑣 “ {𝑃})) |
104 | 103 | 3anassrs 1290 |
. . . . . 6
⊢ ((((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) ∧ 𝑣 ∈ 𝑈) → (𝑣 “ {𝑝}) = (𝑣 “ {𝑃})) |
105 | 100, 104 | mpteq2da 4743 |
. . . . 5
⊢ (((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) → (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) = (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))) |
106 | 105 | rneqd 5353 |
. . . 4
⊢ (((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))) |
107 | | simpl 473 |
. . . 4
⊢ ((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) → 𝑃 ∈ 𝑋) |
108 | | simpr 477 |
. . . 4
⊢ ((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) |
109 | 93, 106, 107, 108 | fvmptd 6288 |
. . 3
⊢ ((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) → (𝑁‘𝑃) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))) |
110 | 86, 92, 109 | syl2anc 693 |
. 2
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁‘𝑃) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))) |
111 | 74, 88, 110 | 3eqtr2d 2662 |
1
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))) |