Step | Hyp | Ref
| Expression |
1 | | distop 21892 |
. 2
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Top) |
2 | | eqidd 2738 |
. 2
⊢ (𝑋 ∈ 𝑉 → 𝑋 = 𝑋) |
3 | | snelpwi 5329 |
. . . . 5
⊢ (𝑧 ∈ 𝑋 → {𝑧} ∈ 𝒫 𝑋) |
4 | 3 | adantl 485 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → {𝑧} ∈ 𝒫 𝑋) |
5 | | vsnid 4578 |
. . . . 5
⊢ 𝑧 ∈ {𝑧} |
6 | 5 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ {𝑧}) |
7 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑢(𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) |
8 | | nfrab1 3296 |
. . . . . 6
⊢
Ⅎ𝑢{𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} |
9 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑢{{𝑧}} |
10 | | dissnref.c |
. . . . . . . . . 10
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} |
11 | 10 | abeq2i 2872 |
. . . . . . . . 9
⊢ (𝑢 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) |
12 | 11 | anbi1i 627 |
. . . . . . . 8
⊢ ((𝑢 ∈ 𝐶 ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ↔ (∃𝑥 ∈ 𝑋 𝑢 = {𝑥} ∧ (𝑢 ∩ {𝑧}) ≠ ∅)) |
13 | | simpr 488 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑢 = {𝑥}) |
14 | | simplr 769 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → 𝑢 = {𝑥}) |
15 | 14 | ineq1d 4126 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → (𝑢 ∩ {𝑧}) = ({𝑥} ∩ {𝑧})) |
16 | | disjsn2 4628 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ≠ 𝑧 → ({𝑥} ∩ {𝑧}) = ∅) |
17 | 16 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → ({𝑥} ∩ {𝑧}) = ∅) |
18 | 15, 17 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → (𝑢 ∩ {𝑧}) = ∅) |
19 | | simp-4r 784 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → (𝑢 ∩ {𝑧}) ≠ ∅) |
20 | 19 | neneqd 2945 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → ¬ (𝑢 ∩ {𝑧}) = ∅) |
21 | 18, 20 | pm2.65da 817 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → ¬ 𝑥 ≠ 𝑧) |
22 | | nne 2944 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑥 ≠ 𝑧 ↔ 𝑥 = 𝑧) |
23 | 21, 22 | sylib 221 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑥 = 𝑧) |
24 | 23 | sneqd 4553 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → {𝑥} = {𝑧}) |
25 | 13, 24 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑢 = {𝑧}) |
26 | 25 | r19.29an 3207 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) → 𝑢 = {𝑧}) |
27 | 26 | an32s 652 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) → 𝑢 = {𝑧}) |
28 | 27 | anasss 470 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (∃𝑥 ∈ 𝑋 𝑢 = {𝑥} ∧ (𝑢 ∩ {𝑧}) ≠ ∅)) → 𝑢 = {𝑧}) |
29 | | sneq 4551 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧}) |
30 | 29 | rspceeqv 3552 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑢 = {𝑧}) → ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) |
31 | 30 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) |
32 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → 𝑢 = {𝑧}) |
33 | 32 | ineq1d 4126 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → (𝑢 ∩ {𝑧}) = ({𝑧} ∩ {𝑧})) |
34 | | inidm 4133 |
. . . . . . . . . . . 12
⊢ ({𝑧} ∩ {𝑧}) = {𝑧} |
35 | 33, 34 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → (𝑢 ∩ {𝑧}) = {𝑧}) |
36 | | vex 3412 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
37 | 36 | snnz 4692 |
. . . . . . . . . . . 12
⊢ {𝑧} ≠ ∅ |
38 | 37 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → {𝑧} ≠ ∅) |
39 | 35, 38 | eqnetrd 3008 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → (𝑢 ∩ {𝑧}) ≠ ∅) |
40 | 31, 39 | jca 515 |
. . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → (∃𝑥 ∈ 𝑋 𝑢 = {𝑥} ∧ (𝑢 ∩ {𝑧}) ≠ ∅)) |
41 | 28, 40 | impbida 801 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → ((∃𝑥 ∈ 𝑋 𝑢 = {𝑥} ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ↔ 𝑢 = {𝑧})) |
42 | 12, 41 | syl5bb 286 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → ((𝑢 ∈ 𝐶 ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ↔ 𝑢 = {𝑧})) |
43 | | rabid 3290 |
. . . . . . 7
⊢ (𝑢 ∈ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ↔ (𝑢 ∈ 𝐶 ∧ (𝑢 ∩ {𝑧}) ≠ ∅)) |
44 | | velsn 4557 |
. . . . . . 7
⊢ (𝑢 ∈ {{𝑧}} ↔ 𝑢 = {𝑧}) |
45 | 42, 43, 44 | 3bitr4g 317 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → (𝑢 ∈ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ↔ 𝑢 ∈ {{𝑧}})) |
46 | 7, 8, 9, 45 | eqrd 3920 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} = {{𝑧}}) |
47 | | snfi 8721 |
. . . . 5
⊢ {{𝑧}} ∈ Fin |
48 | 46, 47 | eqeltrdi 2846 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ∈ Fin) |
49 | | eleq2 2826 |
. . . . . 6
⊢ (𝑦 = {𝑧} → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ {𝑧})) |
50 | | ineq2 4121 |
. . . . . . . . 9
⊢ (𝑦 = {𝑧} → (𝑢 ∩ 𝑦) = (𝑢 ∩ {𝑧})) |
51 | 50 | neeq1d 3000 |
. . . . . . . 8
⊢ (𝑦 = {𝑧} → ((𝑢 ∩ 𝑦) ≠ ∅ ↔ (𝑢 ∩ {𝑧}) ≠ ∅)) |
52 | 51 | rabbidv 3390 |
. . . . . . 7
⊢ (𝑦 = {𝑧} → {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} = {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅}) |
53 | 52 | eleq1d 2822 |
. . . . . 6
⊢ (𝑦 = {𝑧} → ({𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈ Fin ↔ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ∈
Fin)) |
54 | 49, 53 | anbi12d 634 |
. . . . 5
⊢ (𝑦 = {𝑧} → ((𝑧 ∈ 𝑦 ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈ Fin) ↔ (𝑧 ∈ {𝑧} ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ∈
Fin))) |
55 | 54 | rspcev 3537 |
. . . 4
⊢ (({𝑧} ∈ 𝒫 𝑋 ∧ (𝑧 ∈ {𝑧} ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ∈ Fin)) →
∃𝑦 ∈ 𝒫
𝑋(𝑧 ∈ 𝑦 ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈ Fin)) |
56 | 4, 6, 48, 55 | syl12anc 837 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → ∃𝑦 ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈ Fin)) |
57 | 56 | ralrimiva 3105 |
. 2
⊢ (𝑋 ∈ 𝑉 → ∀𝑧 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈ Fin)) |
58 | | unipw 5335 |
. . . 4
⊢ ∪ 𝒫 𝑋 = 𝑋 |
59 | 58 | eqcomi 2746 |
. . 3
⊢ 𝑋 = ∪
𝒫 𝑋 |
60 | 10 | unisngl 22424 |
. . 3
⊢ 𝑋 = ∪
𝐶 |
61 | 59, 60 | islocfin 22414 |
. 2
⊢ (𝐶 ∈ (LocFin‘𝒫
𝑋) ↔ (𝒫 𝑋 ∈ Top ∧ 𝑋 = 𝑋 ∧ ∀𝑧 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈
Fin))) |
62 | 1, 2, 57, 61 | syl3anbrc 1345 |
1
⊢ (𝑋 ∈ 𝑉 → 𝐶 ∈ (LocFin‘𝒫 𝑋)) |