| Step | Hyp | Ref
| Expression |
|---|
| 1 | | distop 22505 |
. 2
β’ (π β π β π« π β Top) |
| 2 | | eqidd 2733 |
. 2
β’ (π β π β π = π) |
| 3 | | snelpwi 5443 |
. . . . 5
β’ (π§ β π β {π§} β π« π) |
| 4 | 3 | adantl 482 |
. . . 4
β’ ((π β π β§ π§ β π) β {π§} β π« π) |
| 5 | | vsnid 4665 |
. . . . 5
β’ π§ β {π§} |
| 6 | 5 | a1i 11 |
. . . 4
β’ ((π β π β§ π§ β π) β π§ β {π§}) |
| 7 | | nfv 1917 |
. . . . . 6
β’
β²π’(π β π β§ π§ β π) |
| 8 | | nfrab1 3451 |
. . . . . 6
β’
β²π’{π’ β πΆ β£ (π’ β© {π§}) β β
} |
| 9 | | nfcv 2903 |
. . . . . 6
β’
β²π’{{π§}} |
| 10 | | dissnref.c |
. . . . . . . . . 10
β’ πΆ = {π’ β£ βπ₯ β π π’ = {π₯}} |
| 11 | 10 | eqabri 2877 |
. . . . . . . . 9
β’ (π’ β πΆ β βπ₯ β π π’ = {π₯}) |
| 12 | 11 | anbi1i 624 |
. . . . . . . 8
β’ ((π’ β πΆ β§ (π’ β© {π§}) β β
) β (βπ₯ β π π’ = {π₯} β§ (π’ β© {π§}) β β
)) |
| 13 | | simpr 485 |
. . . . . . . . . . . . 13
β’
(((((π β π β§ π§ β π) β§ (π’ β© {π§}) β β
) β§ π₯ β π) β§ π’ = {π₯}) β π’ = {π₯}) |
| 14 | | simplr 767 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β π β§ π§ β π) β§ (π’ β© {π§}) β β
) β§ π₯ β π) β§ π’ = {π₯}) β§ π₯ β π§) β π’ = {π₯}) |
| 15 | 14 | ineq1d 4211 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β π β§ π§ β π) β§ (π’ β© {π§}) β β
) β§ π₯ β π) β§ π’ = {π₯}) β§ π₯ β π§) β (π’ β© {π§}) = ({π₯} β© {π§})) |
| 16 | | disjsn2 4716 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β π§ β ({π₯} β© {π§}) = β
) |
| 17 | 16 | adantl 482 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β π β§ π§ β π) β§ (π’ β© {π§}) β β
) β§ π₯ β π) β§ π’ = {π₯}) β§ π₯ β π§) β ({π₯} β© {π§}) = β
) |
| 18 | 15, 17 | eqtrd 2772 |
. . . . . . . . . . . . . . . 16
β’
((((((π β π β§ π§ β π) β§ (π’ β© {π§}) β β
) β§ π₯ β π) β§ π’ = {π₯}) β§ π₯ β π§) β (π’ β© {π§}) = β
) |
| 19 | | simp-4r 782 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β π β§ π§ β π) β§ (π’ β© {π§}) β β
) β§ π₯ β π) β§ π’ = {π₯}) β§ π₯ β π§) β (π’ β© {π§}) β β
) |
| 20 | 19 | neneqd 2945 |
. . . . . . . . . . . . . . . 16
β’
((((((π β π β§ π§ β π) β§ (π’ β© {π§}) β β
) β§ π₯ β π) β§ π’ = {π₯}) β§ π₯ β π§) β Β¬ (π’ β© {π§}) = β
) |
| 21 | 18, 20 | pm2.65da 815 |
. . . . . . . . . . . . . . 15
β’
(((((π β π β§ π§ β π) β§ (π’ β© {π§}) β β
) β§ π₯ β π) β§ π’ = {π₯}) β Β¬ π₯ β π§) |
| 22 | | nne 2944 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π₯ β π§ β π₯ = π§) |
| 23 | 21, 22 | sylib 217 |
. . . . . . . . . . . . . 14
β’
(((((π β π β§ π§ β π) β§ (π’ β© {π§}) β β
) β§ π₯ β π) β§ π’ = {π₯}) β π₯ = π§) |
| 24 | 23 | sneqd 4640 |
. . . . . . . . . . . . 13
β’
(((((π β π β§ π§ β π) β§ (π’ β© {π§}) β β
) β§ π₯ β π) β§ π’ = {π₯}) β {π₯} = {π§}) |
| 25 | 13, 24 | eqtrd 2772 |
. . . . . . . . . . . 12
β’
(((((π β π β§ π§ β π) β§ (π’ β© {π§}) β β
) β§ π₯ β π) β§ π’ = {π₯}) β π’ = {π§}) |
| 26 | 25 | r19.29an 3158 |
. . . . . . . . . . 11
β’ ((((π β π β§ π§ β π) β§ (π’ β© {π§}) β β
) β§ βπ₯ β π π’ = {π₯}) β π’ = {π§}) |
| 27 | 26 | an32s 650 |
. . . . . . . . . 10
β’ ((((π β π β§ π§ β π) β§ βπ₯ β π π’ = {π₯}) β§ (π’ β© {π§}) β β
) β π’ = {π§}) |
| 28 | 27 | anasss 467 |
. . . . . . . . 9
β’ (((π β π β§ π§ β π) β§ (βπ₯ β π π’ = {π₯} β§ (π’ β© {π§}) β β
)) β π’ = {π§}) |
| 29 | | sneq 4638 |
. . . . . . . . . . . 12
β’ (π₯ = π§ β {π₯} = {π§}) |
| 30 | 29 | rspceeqv 3633 |
. . . . . . . . . . 11
β’ ((π§ β π β§ π’ = {π§}) β βπ₯ β π π’ = {π₯}) |
| 31 | 30 | adantll 712 |
. . . . . . . . . 10
β’ (((π β π β§ π§ β π) β§ π’ = {π§}) β βπ₯ β π π’ = {π₯}) |
| 32 | | simpr 485 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π§ β π) β§ π’ = {π§}) β π’ = {π§}) |
| 33 | 32 | ineq1d 4211 |
. . . . . . . . . . . 12
β’ (((π β π β§ π§ β π) β§ π’ = {π§}) β (π’ β© {π§}) = ({π§} β© {π§})) |
| 34 | | inidm 4218 |
. . . . . . . . . . . 12
β’ ({π§} β© {π§}) = {π§} |
| 35 | 33, 34 | eqtrdi 2788 |
. . . . . . . . . . 11
β’ (((π β π β§ π§ β π) β§ π’ = {π§}) β (π’ β© {π§}) = {π§}) |
| 36 | | vex 3478 |
. . . . . . . . . . . . 13
β’ π§ β V |
| 37 | 36 | snnz 4780 |
. . . . . . . . . . . 12
β’ {π§} β β
|
| 38 | 37 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β π β§ π§ β π) β§ π’ = {π§}) β {π§} β β
) |
| 39 | 35, 38 | eqnetrd 3008 |
. . . . . . . . . 10
β’ (((π β π β§ π§ β π) β§ π’ = {π§}) β (π’ β© {π§}) β β
) |
| 40 | 31, 39 | jca 512 |
. . . . . . . . 9
β’ (((π β π β§ π§ β π) β§ π’ = {π§}) β (βπ₯ β π π’ = {π₯} β§ (π’ β© {π§}) β β
)) |
| 41 | 28, 40 | impbida 799 |
. . . . . . . 8
β’ ((π β π β§ π§ β π) β ((βπ₯ β π π’ = {π₯} β§ (π’ β© {π§}) β β
) β π’ = {π§})) |
| 42 | 12, 41 | bitrid 282 |
. . . . . . 7
β’ ((π β π β§ π§ β π) β ((π’ β πΆ β§ (π’ β© {π§}) β β
) β π’ = {π§})) |
| 43 | | rabid 3452 |
. . . . . . 7
β’ (π’ β {π’ β πΆ β£ (π’ β© {π§}) β β
} β (π’ β πΆ β§ (π’ β© {π§}) β β
)) |
| 44 | | velsn 4644 |
. . . . . . 7
β’ (π’ β {{π§}} β π’ = {π§}) |
| 45 | 42, 43, 44 | 3bitr4g 313 |
. . . . . 6
β’ ((π β π β§ π§ β π) β (π’ β {π’ β πΆ β£ (π’ β© {π§}) β β
} β π’ β {{π§}})) |
| 46 | 7, 8, 9, 45 | eqrd 4001 |
. . . . 5
β’ ((π β π β§ π§ β π) β {π’ β πΆ β£ (π’ β© {π§}) β β
} = {{π§}}) |
| 47 | | snfi 9046 |
. . . . 5
β’ {{π§}} β Fin |
| 48 | 46, 47 | eqeltrdi 2841 |
. . . 4
β’ ((π β π β§ π§ β π) β {π’ β πΆ β£ (π’ β© {π§}) β β
} β Fin) |
| 49 | | eleq2 2822 |
. . . . . 6
β’ (π¦ = {π§} β (π§ β π¦ β π§ β {π§})) |
| 50 | | ineq2 4206 |
. . . . . . . . 9
β’ (π¦ = {π§} β (π’ β© π¦) = (π’ β© {π§})) |
| 51 | 50 | neeq1d 3000 |
. . . . . . . 8
β’ (π¦ = {π§} β ((π’ β© π¦) β β
β (π’ β© {π§}) β β
)) |
| 52 | 51 | rabbidv 3440 |
. . . . . . 7
β’ (π¦ = {π§} β {π’ β πΆ β£ (π’ β© π¦) β β
} = {π’ β πΆ β£ (π’ β© {π§}) β β
}) |
| 53 | 52 | eleq1d 2818 |
. . . . . 6
β’ (π¦ = {π§} β ({π’ β πΆ β£ (π’ β© π¦) β β
} β Fin β {π’ β πΆ β£ (π’ β© {π§}) β β
} β
Fin)) |
| 54 | 49, 53 | anbi12d 631 |
. . . . 5
β’ (π¦ = {π§} β ((π§ β π¦ β§ {π’ β πΆ β£ (π’ β© π¦) β β
} β Fin) β (π§ β {π§} β§ {π’ β πΆ β£ (π’ β© {π§}) β β
} β
Fin))) |
| 55 | 54 | rspcev 3612 |
. . . 4
β’ (({π§} β π« π β§ (π§ β {π§} β§ {π’ β πΆ β£ (π’ β© {π§}) β β
} β Fin)) β
βπ¦ β π«
π(π§ β π¦ β§ {π’ β πΆ β£ (π’ β© π¦) β β
} β Fin)) |
| 56 | 4, 6, 48, 55 | syl12anc 835 |
. . 3
β’ ((π β π β§ π§ β π) β βπ¦ β π« π(π§ β π¦ β§ {π’ β πΆ β£ (π’ β© π¦) β β
} β Fin)) |
| 57 | 56 | ralrimiva 3146 |
. 2
β’ (π β π β βπ§ β π βπ¦ β π« π(π§ β π¦ β§ {π’ β πΆ β£ (π’ β© π¦) β β
} β Fin)) |
| 58 | | unipw 5450 |
. . . 4
β’ βͺ π« π = π |
| 59 | 58 | eqcomi 2741 |
. . 3
β’ π = βͺ
π« π |
| 60 | 10 | unisngl 23038 |
. . 3
β’ π = βͺ
πΆ |
| 61 | 59, 60 | islocfin 23028 |
. 2
β’ (πΆ β (LocFinβπ«
π) β (π« π β Top β§ π = π β§ βπ§ β π βπ¦ β π« π(π§ β π¦ β§ {π’ β πΆ β£ (π’ β© π¦) β β
} β
Fin))) |
| 62 | 1, 2, 57, 61 | syl3anbrc 1343 |
1
β’ (π β π β πΆ β (LocFinβπ« π)) |
