| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | distop 23003 | . 2
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Top) | 
| 2 |  | eqidd 2737 | . 2
⊢ (𝑋 ∈ 𝑉 → 𝑋 = 𝑋) | 
| 3 |  | snelpwi 5447 | . . . . 5
⊢ (𝑧 ∈ 𝑋 → {𝑧} ∈ 𝒫 𝑋) | 
| 4 | 3 | adantl 481 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → {𝑧} ∈ 𝒫 𝑋) | 
| 5 |  | vsnid 4662 | . . . . 5
⊢ 𝑧 ∈ {𝑧} | 
| 6 | 5 | a1i 11 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ {𝑧}) | 
| 7 |  | nfv 1913 | . . . . . 6
⊢
Ⅎ𝑢(𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) | 
| 8 |  | nfrab1 3456 | . . . . . 6
⊢
Ⅎ𝑢{𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} | 
| 9 |  | nfcv 2904 | . . . . . 6
⊢
Ⅎ𝑢{{𝑧}} | 
| 10 |  | dissnref.c | . . . . . . . . . 10
⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} | 
| 11 | 10 | eqabri 2884 | . . . . . . . . 9
⊢ (𝑢 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) | 
| 12 | 11 | anbi1i 624 | . . . . . . . 8
⊢ ((𝑢 ∈ 𝐶 ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ↔ (∃𝑥 ∈ 𝑋 𝑢 = {𝑥} ∧ (𝑢 ∩ {𝑧}) ≠ ∅)) | 
| 13 |  | simpr 484 | . . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑢 = {𝑥}) | 
| 14 |  | simplr 768 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → 𝑢 = {𝑥}) | 
| 15 | 14 | ineq1d 4218 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → (𝑢 ∩ {𝑧}) = ({𝑥} ∩ {𝑧})) | 
| 16 |  | disjsn2 4711 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ≠ 𝑧 → ({𝑥} ∩ {𝑧}) = ∅) | 
| 17 | 16 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → ({𝑥} ∩ {𝑧}) = ∅) | 
| 18 | 15, 17 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → (𝑢 ∩ {𝑧}) = ∅) | 
| 19 |  | simp-4r 783 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → (𝑢 ∩ {𝑧}) ≠ ∅) | 
| 20 | 19 | neneqd 2944 | . . . . . . . . . . . . . . . 16
⊢
((((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) ∧ 𝑥 ≠ 𝑧) → ¬ (𝑢 ∩ {𝑧}) = ∅) | 
| 21 | 18, 20 | pm2.65da 816 | . . . . . . . . . . . . . . 15
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → ¬ 𝑥 ≠ 𝑧) | 
| 22 |  | nne 2943 | . . . . . . . . . . . . . . 15
⊢ (¬
𝑥 ≠ 𝑧 ↔ 𝑥 = 𝑧) | 
| 23 | 21, 22 | sylib 218 | . . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑥 = 𝑧) | 
| 24 | 23 | sneqd 4637 | . . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → {𝑥} = {𝑧}) | 
| 25 | 13, 24 | eqtrd 2776 | . . . . . . . . . . . 12
⊢
(((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ 𝑥 ∈ 𝑋) ∧ 𝑢 = {𝑥}) → 𝑢 = {𝑧}) | 
| 26 | 25 | r19.29an 3157 | . . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ∧ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) → 𝑢 = {𝑧}) | 
| 27 | 26 | an32s 652 | . . . . . . . . . 10
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) ∧ (𝑢 ∩ {𝑧}) ≠ ∅) → 𝑢 = {𝑧}) | 
| 28 | 27 | anasss 466 | . . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ (∃𝑥 ∈ 𝑋 𝑢 = {𝑥} ∧ (𝑢 ∩ {𝑧}) ≠ ∅)) → 𝑢 = {𝑧}) | 
| 29 |  | sneq 4635 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧}) | 
| 30 | 29 | rspceeqv 3644 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ∧ 𝑢 = {𝑧}) → ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) | 
| 31 | 30 | adantll 714 | . . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}) | 
| 32 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → 𝑢 = {𝑧}) | 
| 33 | 32 | ineq1d 4218 | . . . . . . . . . . . 12
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → (𝑢 ∩ {𝑧}) = ({𝑧} ∩ {𝑧})) | 
| 34 |  | inidm 4226 | . . . . . . . . . . . 12
⊢ ({𝑧} ∩ {𝑧}) = {𝑧} | 
| 35 | 33, 34 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → (𝑢 ∩ {𝑧}) = {𝑧}) | 
| 36 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑧 ∈ V | 
| 37 | 36 | snnz 4775 | . . . . . . . . . . . 12
⊢ {𝑧} ≠ ∅ | 
| 38 | 37 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → {𝑧} ≠ ∅) | 
| 39 | 35, 38 | eqnetrd 3007 | . . . . . . . . . 10
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → (𝑢 ∩ {𝑧}) ≠ ∅) | 
| 40 | 31, 39 | jca 511 | . . . . . . . . 9
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) ∧ 𝑢 = {𝑧}) → (∃𝑥 ∈ 𝑋 𝑢 = {𝑥} ∧ (𝑢 ∩ {𝑧}) ≠ ∅)) | 
| 41 | 28, 40 | impbida 800 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → ((∃𝑥 ∈ 𝑋 𝑢 = {𝑥} ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ↔ 𝑢 = {𝑧})) | 
| 42 | 12, 41 | bitrid 283 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → ((𝑢 ∈ 𝐶 ∧ (𝑢 ∩ {𝑧}) ≠ ∅) ↔ 𝑢 = {𝑧})) | 
| 43 |  | rabid 3457 | . . . . . . 7
⊢ (𝑢 ∈ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ↔ (𝑢 ∈ 𝐶 ∧ (𝑢 ∩ {𝑧}) ≠ ∅)) | 
| 44 |  | velsn 4641 | . . . . . . 7
⊢ (𝑢 ∈ {{𝑧}} ↔ 𝑢 = {𝑧}) | 
| 45 | 42, 43, 44 | 3bitr4g 314 | . . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → (𝑢 ∈ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ↔ 𝑢 ∈ {{𝑧}})) | 
| 46 | 7, 8, 9, 45 | eqrd 4002 | . . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} = {{𝑧}}) | 
| 47 |  | snfi 9084 | . . . . 5
⊢ {{𝑧}} ∈ Fin | 
| 48 | 46, 47 | eqeltrdi 2848 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ∈ Fin) | 
| 49 |  | eleq2 2829 | . . . . . 6
⊢ (𝑦 = {𝑧} → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ {𝑧})) | 
| 50 |  | ineq2 4213 | . . . . . . . . 9
⊢ (𝑦 = {𝑧} → (𝑢 ∩ 𝑦) = (𝑢 ∩ {𝑧})) | 
| 51 | 50 | neeq1d 2999 | . . . . . . . 8
⊢ (𝑦 = {𝑧} → ((𝑢 ∩ 𝑦) ≠ ∅ ↔ (𝑢 ∩ {𝑧}) ≠ ∅)) | 
| 52 | 51 | rabbidv 3443 | . . . . . . 7
⊢ (𝑦 = {𝑧} → {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} = {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅}) | 
| 53 | 52 | eleq1d 2825 | . . . . . 6
⊢ (𝑦 = {𝑧} → ({𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈ Fin ↔ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ∈
Fin)) | 
| 54 | 49, 53 | anbi12d 632 | . . . . 5
⊢ (𝑦 = {𝑧} → ((𝑧 ∈ 𝑦 ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈ Fin) ↔ (𝑧 ∈ {𝑧} ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ∈
Fin))) | 
| 55 | 54 | rspcev 3621 | . . . 4
⊢ (({𝑧} ∈ 𝒫 𝑋 ∧ (𝑧 ∈ {𝑧} ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ {𝑧}) ≠ ∅} ∈ Fin)) →
∃𝑦 ∈ 𝒫
𝑋(𝑧 ∈ 𝑦 ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈ Fin)) | 
| 56 | 4, 6, 48, 55 | syl12anc 836 | . . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑧 ∈ 𝑋) → ∃𝑦 ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈ Fin)) | 
| 57 | 56 | ralrimiva 3145 | . 2
⊢ (𝑋 ∈ 𝑉 → ∀𝑧 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈ Fin)) | 
| 58 |  | unipw 5454 | . . . 4
⊢ ∪ 𝒫 𝑋 = 𝑋 | 
| 59 | 58 | eqcomi 2745 | . . 3
⊢ 𝑋 = ∪
𝒫 𝑋 | 
| 60 | 10 | unisngl 23536 | . . 3
⊢ 𝑋 = ∪
𝐶 | 
| 61 | 59, 60 | islocfin 23526 | . 2
⊢ (𝐶 ∈ (LocFin‘𝒫
𝑋) ↔ (𝒫 𝑋 ∈ Top ∧ 𝑋 = 𝑋 ∧ ∀𝑧 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝑋(𝑧 ∈ 𝑦 ∧ {𝑢 ∈ 𝐶 ∣ (𝑢 ∩ 𝑦) ≠ ∅} ∈
Fin))) | 
| 62 | 1, 2, 57, 61 | syl3anbrc 1343 | 1
⊢ (𝑋 ∈ 𝑉 → 𝐶 ∈ (LocFin‘𝒫 𝑋)) |