Step | Hyp | Ref
| Expression |
1 | | ctex 8906 |
. 2
β’ (π βΌ Ο β π β V) |
2 | | pwexr 7700 |
. 2
β’
(π« π β
2ndΟ β π β V) |
3 | | vsnex 5387 |
. . . . . . . 8
β’ {π₯} β V |
4 | 3 | 2a1i 12 |
. . . . . . 7
β’ (π β V β (π₯ β π β {π₯} β V)) |
5 | | vex 3448 |
. . . . . . . . . 10
β’ π₯ β V |
6 | 5 | sneqr 4799 |
. . . . . . . . 9
β’ ({π₯} = {π¦} β π₯ = π¦) |
7 | | sneq 4597 |
. . . . . . . . 9
β’ (π₯ = π¦ β {π₯} = {π¦}) |
8 | 6, 7 | impbii 208 |
. . . . . . . 8
β’ ({π₯} = {π¦} β π₯ = π¦) |
9 | 8 | 2a1i 12 |
. . . . . . 7
β’ (π β V β ((π₯ β π β§ π¦ β π) β ({π₯} = {π¦} β π₯ = π¦))) |
10 | 4, 9 | dom2lem 8935 |
. . . . . 6
β’ (π β V β (π₯ β π β¦ {π₯}):πβ1-1βV) |
11 | | f1f1orn 6796 |
. . . . . 6
β’ ((π₯ β π β¦ {π₯}):πβ1-1βV β (π₯ β π β¦ {π₯}):πβ1-1-ontoβran
(π₯ β π β¦ {π₯})) |
12 | 10, 11 | syl 17 |
. . . . 5
β’ (π β V β (π₯ β π β¦ {π₯}):πβ1-1-ontoβran
(π₯ β π β¦ {π₯})) |
13 | | f1oeng 8914 |
. . . . 5
β’ ((π β V β§ (π₯ β π β¦ {π₯}):πβ1-1-ontoβran
(π₯ β π β¦ {π₯})) β π β ran (π₯ β π β¦ {π₯})) |
14 | 12, 13 | mpdan 686 |
. . . 4
β’ (π β V β π β ran (π₯ β π β¦ {π₯})) |
15 | | domen1 9066 |
. . . 4
β’ (π β ran (π₯ β π β¦ {π₯}) β (π βΌ Ο β ran (π₯ β π β¦ {π₯}) βΌ Ο)) |
16 | 14, 15 | syl 17 |
. . 3
β’ (π β V β (π βΌ Ο β ran
(π₯ β π β¦ {π₯}) βΌ Ο)) |
17 | | distop 22361 |
. . . . . . 7
β’ (π β V β π« π β Top) |
18 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β V β§ π₯ β π) β π₯ β π) |
19 | 5 | snelpw 5403 |
. . . . . . . . . 10
β’ (π₯ β π β {π₯} β π« π) |
20 | 18, 19 | sylib 217 |
. . . . . . . . 9
β’ ((π β V β§ π₯ β π) β {π₯} β π« π) |
21 | 20 | fmpttd 7064 |
. . . . . . . 8
β’ (π β V β (π₯ β π β¦ {π₯}):πβΆπ« π) |
22 | 21 | frnd 6677 |
. . . . . . 7
β’ (π β V β ran (π₯ β π β¦ {π₯}) β π« π) |
23 | | elpwi 4568 |
. . . . . . . . . . . . 13
β’ (π¦ β π« π β π¦ β π) |
24 | 23 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ ((π β V β§ (π¦ β π« π β§ π§ β π¦)) β π¦ β π) |
25 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π β V β§ (π¦ β π« π β§ π§ β π¦)) β π§ β π¦) |
26 | 24, 25 | sseldd 3946 |
. . . . . . . . . . 11
β’ ((π β V β§ (π¦ β π« π β§ π§ β π¦)) β π§ β π) |
27 | | eqidd 2734 |
. . . . . . . . . . 11
β’ ((π β V β§ (π¦ β π« π β§ π§ β π¦)) β {π§} = {π§}) |
28 | | sneq 4597 |
. . . . . . . . . . . 12
β’ (π₯ = π§ β {π₯} = {π§}) |
29 | 28 | rspceeqv 3596 |
. . . . . . . . . . 11
β’ ((π§ β π β§ {π§} = {π§}) β βπ₯ β π {π§} = {π₯}) |
30 | 26, 27, 29 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β V β§ (π¦ β π« π β§ π§ β π¦)) β βπ₯ β π {π§} = {π₯}) |
31 | | vsnex 5387 |
. . . . . . . . . . 11
β’ {π§} β V |
32 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π₯ β π β¦ {π₯}) = (π₯ β π β¦ {π₯}) |
33 | 32 | elrnmpt 5912 |
. . . . . . . . . . 11
β’ ({π§} β V β ({π§} β ran (π₯ β π β¦ {π₯}) β βπ₯ β π {π§} = {π₯})) |
34 | 31, 33 | ax-mp 5 |
. . . . . . . . . 10
β’ ({π§} β ran (π₯ β π β¦ {π₯}) β βπ₯ β π {π§} = {π₯}) |
35 | 30, 34 | sylibr 233 |
. . . . . . . . 9
β’ ((π β V β§ (π¦ β π« π β§ π§ β π¦)) β {π§} β ran (π₯ β π β¦ {π₯})) |
36 | | vsnid 4624 |
. . . . . . . . . 10
β’ π§ β {π§} |
37 | 36 | a1i 11 |
. . . . . . . . 9
β’ ((π β V β§ (π¦ β π« π β§ π§ β π¦)) β π§ β {π§}) |
38 | 25 | snssd 4770 |
. . . . . . . . 9
β’ ((π β V β§ (π¦ β π« π β§ π§ β π¦)) β {π§} β π¦) |
39 | | eleq2 2823 |
. . . . . . . . . . 11
β’ (π€ = {π§} β (π§ β π€ β π§ β {π§})) |
40 | | sseq1 3970 |
. . . . . . . . . . 11
β’ (π€ = {π§} β (π€ β π¦ β {π§} β π¦)) |
41 | 39, 40 | anbi12d 632 |
. . . . . . . . . 10
β’ (π€ = {π§} β ((π§ β π€ β§ π€ β π¦) β (π§ β {π§} β§ {π§} β π¦))) |
42 | 41 | rspcev 3580 |
. . . . . . . . 9
β’ (({π§} β ran (π₯ β π β¦ {π₯}) β§ (π§ β {π§} β§ {π§} β π¦)) β βπ€ β ran (π₯ β π β¦ {π₯})(π§ β π€ β§ π€ β π¦)) |
43 | 35, 37, 38, 42 | syl12anc 836 |
. . . . . . . 8
β’ ((π β V β§ (π¦ β π« π β§ π§ β π¦)) β βπ€ β ran (π₯ β π β¦ {π₯})(π§ β π€ β§ π€ β π¦)) |
44 | 43 | ralrimivva 3194 |
. . . . . . 7
β’ (π β V β βπ¦ β π« πβπ§ β π¦ βπ€ β ran (π₯ β π β¦ {π₯})(π§ β π€ β§ π€ β π¦)) |
45 | | basgen2 22355 |
. . . . . . 7
β’
((π« π β
Top β§ ran (π₯ β
π β¦ {π₯}) β π« π β§ βπ¦ β π« πβπ§ β π¦ βπ€ β ran (π₯ β π β¦ {π₯})(π§ β π€ β§ π€ β π¦)) β (topGenβran (π₯ β π β¦ {π₯})) = π« π) |
46 | 17, 22, 44, 45 | syl3anc 1372 |
. . . . . 6
β’ (π β V β
(topGenβran (π₯ β
π β¦ {π₯})) = π« π) |
47 | 46 | adantr 482 |
. . . . 5
β’ ((π β V β§ ran (π₯ β π β¦ {π₯}) βΌ Ο) β (topGenβran
(π₯ β π β¦ {π₯})) = π« π) |
48 | 46, 17 | eqeltrd 2834 |
. . . . . . 7
β’ (π β V β
(topGenβran (π₯ β
π β¦ {π₯})) β Top) |
49 | | tgclb 22336 |
. . . . . . 7
β’ (ran
(π₯ β π β¦ {π₯}) β TopBases β (topGenβran
(π₯ β π β¦ {π₯})) β Top) |
50 | 48, 49 | sylibr 233 |
. . . . . 6
β’ (π β V β ran (π₯ β π β¦ {π₯}) β TopBases) |
51 | | 2ndci 22815 |
. . . . . 6
β’ ((ran
(π₯ β π β¦ {π₯}) β TopBases β§ ran (π₯ β π β¦ {π₯}) βΌ Ο) β (topGenβran
(π₯ β π β¦ {π₯})) β
2ndΟ) |
52 | 50, 51 | sylan 581 |
. . . . 5
β’ ((π β V β§ ran (π₯ β π β¦ {π₯}) βΌ Ο) β (topGenβran
(π₯ β π β¦ {π₯})) β
2ndΟ) |
53 | 47, 52 | eqeltrrd 2835 |
. . . 4
β’ ((π β V β§ ran (π₯ β π β¦ {π₯}) βΌ Ο) β π« π β
2ndΟ) |
54 | | is2ndc 22813 |
. . . . . 6
β’
(π« π β
2ndΟ β βπ β TopBases (π βΌ Ο β§ (topGenβπ) = π« π)) |
55 | | vex 3448 |
. . . . . . . . 9
β’ π β V |
56 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((((π β V β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) =
π« π)) β§ π₯ β π) β π₯ β π) |
57 | 56, 19 | sylib 217 |
. . . . . . . . . . . . . 14
β’ ((((π β V β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) =
π« π)) β§ π₯ β π) β {π₯} β π« π) |
58 | | simplrr 777 |
. . . . . . . . . . . . . 14
β’ ((((π β V β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) =
π« π)) β§ π₯ β π) β (topGenβπ) = π« π) |
59 | 57, 58 | eleqtrrd 2837 |
. . . . . . . . . . . . 13
β’ ((((π β V β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) =
π« π)) β§ π₯ β π) β {π₯} β (topGenβπ)) |
60 | | vsnid 4624 |
. . . . . . . . . . . . 13
β’ π₯ β {π₯} |
61 | | tg2 22331 |
. . . . . . . . . . . . 13
β’ (({π₯} β (topGenβπ) β§ π₯ β {π₯}) β βπ¦ β π (π₯ β π¦ β§ π¦ β {π₯})) |
62 | 59, 60, 61 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((((π β V β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) =
π« π)) β§ π₯ β π) β βπ¦ β π (π₯ β π¦ β§ π¦ β {π₯})) |
63 | | simprrl 780 |
. . . . . . . . . . . . . . 15
β’
(((((π β V
β§ π β TopBases)
β§ (π βΌ Ο
β§ (topGenβπ) =
π« π)) β§ π₯ β π) β§ (π¦ β π β§ (π₯ β π¦ β§ π¦ β {π₯}))) β π₯ β π¦) |
64 | 63 | snssd 4770 |
. . . . . . . . . . . . . 14
β’
(((((π β V
β§ π β TopBases)
β§ (π βΌ Ο
β§ (topGenβπ) =
π« π)) β§ π₯ β π) β§ (π¦ β π β§ (π₯ β π¦ β§ π¦ β {π₯}))) β {π₯} β π¦) |
65 | | simprrr 781 |
. . . . . . . . . . . . . 14
β’
(((((π β V
β§ π β TopBases)
β§ (π βΌ Ο
β§ (topGenβπ) =
π« π)) β§ π₯ β π) β§ (π¦ β π β§ (π₯ β π¦ β§ π¦ β {π₯}))) β π¦ β {π₯}) |
66 | 64, 65 | eqssd 3962 |
. . . . . . . . . . . . 13
β’
(((((π β V
β§ π β TopBases)
β§ (π βΌ Ο
β§ (topGenβπ) =
π« π)) β§ π₯ β π) β§ (π¦ β π β§ (π₯ β π¦ β§ π¦ β {π₯}))) β {π₯} = π¦) |
67 | | simprl 770 |
. . . . . . . . . . . . 13
β’
(((((π β V
β§ π β TopBases)
β§ (π βΌ Ο
β§ (topGenβπ) =
π« π)) β§ π₯ β π) β§ (π¦ β π β§ (π₯ β π¦ β§ π¦ β {π₯}))) β π¦ β π) |
68 | 66, 67 | eqeltrd 2834 |
. . . . . . . . . . . 12
β’
(((((π β V
β§ π β TopBases)
β§ (π βΌ Ο
β§ (topGenβπ) =
π« π)) β§ π₯ β π) β§ (π¦ β π β§ (π₯ β π¦ β§ π¦ β {π₯}))) β {π₯} β π) |
69 | 62, 68 | rexlimddv 3155 |
. . . . . . . . . . 11
β’ ((((π β V β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) =
π« π)) β§ π₯ β π) β {π₯} β π) |
70 | 69 | fmpttd 7064 |
. . . . . . . . . 10
β’ (((π β V β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) =
π« π)) β (π₯ β π β¦ {π₯}):πβΆπ) |
71 | 70 | frnd 6677 |
. . . . . . . . 9
β’ (((π β V β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) =
π« π)) β ran
(π₯ β π β¦ {π₯}) β π) |
72 | | ssdomg 8943 |
. . . . . . . . 9
β’ (π β V β (ran (π₯ β π β¦ {π₯}) β π β ran (π₯ β π β¦ {π₯}) βΌ π)) |
73 | 55, 71, 72 | mpsyl 68 |
. . . . . . . 8
β’ (((π β V β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) =
π« π)) β ran
(π₯ β π β¦ {π₯}) βΌ π) |
74 | | simprl 770 |
. . . . . . . 8
β’ (((π β V β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) =
π« π)) β π βΌ
Ο) |
75 | | domtr 8950 |
. . . . . . . 8
β’ ((ran
(π₯ β π β¦ {π₯}) βΌ π β§ π βΌ Ο) β ran (π₯ β π β¦ {π₯}) βΌ Ο) |
76 | 73, 74, 75 | syl2anc 585 |
. . . . . . 7
β’ (((π β V β§ π β TopBases) β§ (π βΌ Ο β§
(topGenβπ) =
π« π)) β ran
(π₯ β π β¦ {π₯}) βΌ Ο) |
77 | 76 | rexlimdva2 3151 |
. . . . . 6
β’ (π β V β (βπ β TopBases (π βΌ Ο β§
(topGenβπ) =
π« π) β ran
(π₯ β π β¦ {π₯}) βΌ Ο)) |
78 | 54, 77 | biimtrid 241 |
. . . . 5
β’ (π β V β (π«
π β
2ndΟ β ran (π₯ β π β¦ {π₯}) βΌ Ο)) |
79 | 78 | imp 408 |
. . . 4
β’ ((π β V β§ π« π β 2ndΟ)
β ran (π₯ β π β¦ {π₯}) βΌ Ο) |
80 | 53, 79 | impbida 800 |
. . 3
β’ (π β V β (ran (π₯ β π β¦ {π₯}) βΌ Ο β π« π β
2ndΟ)) |
81 | 16, 80 | bitrd 279 |
. 2
β’ (π β V β (π βΌ Ο β
π« π β
2ndΟ)) |
82 | 1, 2, 81 | pm5.21nii 380 |
1
β’ (π βΌ Ο β
π« π β
2ndΟ) |