Step | Hyp | Ref
| Expression |
1 | | distop 20610 |
. 2
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Top) |
2 | | eqidd 2611 |
. 2
⊢ (𝑋 ∈ 𝑉 → 𝑋 = 𝑋) |
3 | | snelpwi 4839 |
. . . . 5
⊢ (𝑧 ∈ 𝑋 → {𝑧} ∈ 𝒫 𝑋) |
4 | 3 | adantl 481 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → {𝑧} ∈ 𝒫 𝑋) |
5 | | vsnid 4156 |
. . . . 5
⊢ 𝑧 ∈ {𝑧} |
6 | 5 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ {𝑧}) |
7 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑢(𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) |
8 | | nfrab1 3099 |
. . . . . 6
⊢
Ⅎ𝑢{𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} |
9 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑢{{𝑧}} |
10 | | dissnref.c |
. . . . . . . . . 10
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} |
11 | 10 | abeq2i 2722 |
. . . . . . . . 9
⊢ (𝑢 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) |
12 | 11 | anbi1i 727 |
. . . . . . . 8
⊢ ((𝑢 ∈ 𝐶 ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ↔ (∃𝑥 ∈ 𝑋 𝑢 = {𝑥} ∧ (𝑢 ∩ {𝑧}) ≠ ∅)) |
13 | | simpr 476 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑢 = {𝑥}) |
14 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → 𝑢 = {𝑥}) |
15 | 14 | ineq1d 3775 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → (𝑢 ∩ {𝑧}) = ({𝑥} ∩ {𝑧})) |
16 | | disjsn2 4193 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ≠ 𝑧 → ({𝑥} ∩ {𝑧}) = ∅) |
17 | 16 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → ({𝑥} ∩ {𝑧}) = ∅) |
18 | 15, 17 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → (𝑢 ∩ {𝑧}) = ∅) |
19 | | simp-4r 803 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → (𝑢 ∩ {𝑧}) ≠ ∅) |
20 | 19 | neneqd 2787 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → ¬ (𝑢 ∩ {𝑧}) = ∅) |
21 | 18, 20 | pm2.65da 598 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → ¬ 𝑥 ≠ 𝑧) |
22 | | nne 2786 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑥 ≠ 𝑧 ↔ 𝑥 = 𝑧) |
23 | 21, 22 | sylib 207 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑥 = 𝑧) |
24 | 23 | sneqd 4137 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → {𝑥} = {𝑧}) |
25 | 13, 24 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑢 = {𝑧}) |
26 | 25 | r19.29an 3059 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) → 𝑢 = {𝑧}) |
27 | 26 | an32s 842 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) → 𝑢 = {𝑧}) |
28 | 27 | anasss 677 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (∃𝑥 ∈ 𝑋 𝑢 = {𝑥} ∧ (𝑢 ∩ {𝑧}) ≠ ∅)) → 𝑢 = {𝑧}) |
29 | | sneq 4135 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧}) |
30 | 29 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑢 = {𝑥} ↔ 𝑢 = {𝑧})) |
31 | 30 | rspcev 3282 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑢 = {𝑧}) → ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) |
32 | 31 | adantll 746 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) |
33 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → 𝑢 = {𝑧}) |
34 | 33 | ineq1d 3775 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → (𝑢 ∩ {𝑧}) = ({𝑧} ∩ {𝑧})) |
35 | | inidm 3784 |
. . . . . . . . . . . 12
⊢ ({𝑧} ∩ {𝑧}) = {𝑧} |
36 | 34, 35 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → (𝑢 ∩ {𝑧}) = {𝑧}) |
37 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
38 | 37 | snnz 4252 |
. . . . . . . . . . . 12
⊢ {𝑧} ≠ ∅ |
39 | 38 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → {𝑧} ≠ ∅) |
40 | 36, 39 | eqnetrd 2849 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → (𝑢 ∩ {𝑧}) ≠ ∅) |
41 | 32, 40 | jca 553 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → (∃𝑥 ∈ 𝑋 𝑢 = {𝑥} ∧ (𝑢 ∩ {𝑧}) ≠ ∅)) |
42 | 28, 41 | impbida 873 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → ((∃𝑥 ∈ 𝑋 𝑢 = {𝑥} ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ↔ 𝑢 = {𝑧})) |
43 | 12, 42 | syl5bb 271 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → ((𝑢 ∈ 𝐶 ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ↔ 𝑢 = {𝑧})) |
44 | | rabid 3095 |
. . . . . . 7
⊢ (𝑢 ∈ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ↔ (𝑢 ∈ 𝐶 ∧ (𝑢 ∩ {𝑧}) ≠ ∅)) |
45 | | velsn 4141 |
. . . . . . 7
⊢ (𝑢 ∈ {{𝑧}} ↔ 𝑢 = {𝑧}) |
46 | 43, 44, 45 | 3bitr4g 302 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → (𝑢 ∈ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ↔ 𝑢 ∈ {{𝑧}})) |
47 | 7, 8, 9, 46 | eqrd 3586 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} = {{𝑧}}) |
48 | | snfi 7923 |
. . . . 5
⊢ {{𝑧}} ∈ Fin |
49 | 47, 48 | syl6eqel 2696 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ∈ Fin) |
50 | | eleq2 2677 |
. . . . . 6
⊢ (𝑦 = {𝑧} → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ {𝑧})) |
51 | | ineq2 3770 |
. . . . . . . . 9
⊢ (𝑦 = {𝑧} → (𝑢 ∩ 𝑦) = (𝑢 ∩ {𝑧})) |
52 | 51 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑦 = {𝑧} → ((𝑢 ∩ 𝑦) ≠ ∅ ↔ (𝑢 ∩ {𝑧}) ≠ ∅)) |
53 | 52 | rabbidv 3164 |
. . . . . . 7
⊢ (𝑦 = {𝑧} → {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} = {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅}) |
54 | 53 | eleq1d 2672 |
. . . . . 6
⊢ (𝑦 = {𝑧} → ({𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈ Fin ↔ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ∈
Fin)) |
55 | 50, 54 | anbi12d 743 |
. . . . 5
⊢ (𝑦 = {𝑧} → ((𝑧 ∈ 𝑦 ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈ Fin) ↔ (𝑧 ∈ {𝑧} ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ∈
Fin))) |
56 | 55 | rspcev 3282 |
. . . 4
⊢ (({𝑧} ∈ 𝒫 𝑋 ∧ (𝑧 ∈ {𝑧} ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ∈ Fin)) →
∃𝑦 ∈ 𝒫
𝑋(𝑧 ∈ 𝑦 ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈ Fin)) |
57 | 4, 6, 49, 56 | syl12anc 1316 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → ∃𝑦 ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈ Fin)) |
58 | 57 | ralrimiva 2949 |
. 2
⊢ (𝑋 ∈ 𝑉 → ∀𝑧 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈ Fin)) |
59 | | unipw 4845 |
. . . 4
⊢ ∪ 𝒫 𝑋 = 𝑋 |
60 | 59 | eqcomi 2619 |
. . 3
⊢ 𝑋 = ∪
𝒫 𝑋 |
61 | 10 | unisngl 21140 |
. . 3
⊢ 𝑋 = ∪
𝐶 |
62 | 60, 61 | islocfin 21130 |
. 2
⊢ (𝐶 ∈ (LocFin‘𝒫
𝑋) ↔ (𝒫 𝑋 ∈ Top ∧ 𝑋 = 𝑋 ∧ ∀𝑧 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈
Fin))) |
63 | 1, 2, 58, 62 | syl3anbrc 1239 |
1
⊢ (𝑋 ∈ 𝑉 → 𝐶 ∈ (LocFin‘𝒫 𝑋)) |