Step | Hyp | Ref
| Expression |
1 | | ppttop 22373 |
. . . 4
β’ ((π΄ β π β§ π β π΄) β {π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)} β (TopOnβπ΄)) |
2 | | topontop 22278 |
. . . 4
β’ ({π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)} β (TopOnβπ΄) β {π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)} β Top) |
3 | 1, 2 | syl 17 |
. . 3
β’ ((π΄ β π β§ π β π΄) β {π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)} β Top) |
4 | | eleq2 2823 |
. . . . . . 7
β’ (π¦ = {π₯, π} β (π β π¦ β π β {π₯, π})) |
5 | | eqeq1 2737 |
. . . . . . 7
β’ (π¦ = {π₯, π} β (π¦ = β
β {π₯, π} = β
)) |
6 | 4, 5 | orbi12d 918 |
. . . . . 6
β’ (π¦ = {π₯, π} β ((π β π¦ β¨ π¦ = β
) β (π β {π₯, π} β¨ {π₯, π} = β
))) |
7 | | simpr 486 |
. . . . . . . 8
β’ (((π΄ β π β§ π β π΄) β§ π₯ β π΄) β π₯ β π΄) |
8 | | simplr 768 |
. . . . . . . 8
β’ (((π΄ β π β§ π β π΄) β§ π₯ β π΄) β π β π΄) |
9 | 7, 8 | prssd 4783 |
. . . . . . 7
β’ (((π΄ β π β§ π β π΄) β§ π₯ β π΄) β {π₯, π} β π΄) |
10 | | prex 5390 |
. . . . . . . 8
β’ {π₯, π} β V |
11 | 10 | elpw 4565 |
. . . . . . 7
β’ ({π₯, π} β π« π΄ β {π₯, π} β π΄) |
12 | 9, 11 | sylibr 233 |
. . . . . 6
β’ (((π΄ β π β§ π β π΄) β§ π₯ β π΄) β {π₯, π} β π« π΄) |
13 | | prid2g 4723 |
. . . . . . . 8
β’ (π β π΄ β π β {π₯, π}) |
14 | 13 | ad2antlr 726 |
. . . . . . 7
β’ (((π΄ β π β§ π β π΄) β§ π₯ β π΄) β π β {π₯, π}) |
15 | 14 | orcd 872 |
. . . . . 6
β’ (((π΄ β π β§ π β π΄) β§ π₯ β π΄) β (π β {π₯, π} β¨ {π₯, π} = β
)) |
16 | 6, 12, 15 | elrabd 3648 |
. . . . 5
β’ (((π΄ β π β§ π β π΄) β§ π₯ β π΄) β {π₯, π} β {π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)}) |
17 | 16 | fmpttd 7064 |
. . . 4
β’ ((π΄ β π β§ π β π΄) β (π₯ β π΄ β¦ {π₯, π}):π΄βΆ{π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)}) |
18 | 17 | frnd 6677 |
. . 3
β’ ((π΄ β π β§ π β π΄) β ran (π₯ β π΄ β¦ {π₯, π}) β {π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)}) |
19 | | eleq2 2823 |
. . . . . . 7
β’ (π¦ = π§ β (π β π¦ β π β π§)) |
20 | | eqeq1 2737 |
. . . . . . 7
β’ (π¦ = π§ β (π¦ = β
β π§ = β
)) |
21 | 19, 20 | orbi12d 918 |
. . . . . 6
β’ (π¦ = π§ β ((π β π¦ β¨ π¦ = β
) β (π β π§ β¨ π§ = β
))) |
22 | 21 | elrab 3646 |
. . . . 5
β’ (π§ β {π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)} β (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
))) |
23 | | elpwi 4568 |
. . . . . . . . . . 11
β’ (π§ β π« π΄ β π§ β π΄) |
24 | 23 | ad2antrl 727 |
. . . . . . . . . 10
β’ (((π΄ β π β§ π β π΄) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
))) β π§ β π΄) |
25 | 24 | sselda 3945 |
. . . . . . . . 9
β’ ((((π΄ β π β§ π β π΄) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
))) β§ π€ β π§) β π€ β π΄) |
26 | | prid1g 4722 |
. . . . . . . . . 10
β’ (π€ β π§ β π€ β {π€, π}) |
27 | 26 | adantl 483 |
. . . . . . . . 9
β’ ((((π΄ β π β§ π β π΄) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
))) β§ π€ β π§) β π€ β {π€, π}) |
28 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π΄ β π β§ π β π΄) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
))) β§ π€ β π§) β π€ β π§) |
29 | | n0i 4294 |
. . . . . . . . . . . 12
β’ (π€ β π§ β Β¬ π§ = β
) |
30 | 29 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π΄ β π β§ π β π΄) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
))) β§ π€ β π§) β Β¬ π§ = β
) |
31 | | simplrr 777 |
. . . . . . . . . . . 12
β’ ((((π΄ β π β§ π β π΄) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
))) β§ π€ β π§) β (π β π§ β¨ π§ = β
)) |
32 | 31 | ord 863 |
. . . . . . . . . . 11
β’ ((((π΄ β π β§ π β π΄) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
))) β§ π€ β π§) β (Β¬ π β π§ β π§ = β
)) |
33 | 30, 32 | mt3d 148 |
. . . . . . . . . 10
β’ ((((π΄ β π β§ π β π΄) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
))) β§ π€ β π§) β π β π§) |
34 | 28, 33 | prssd 4783 |
. . . . . . . . 9
β’ ((((π΄ β π β§ π β π΄) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
))) β§ π€ β π§) β {π€, π} β π§) |
35 | | preq1 4695 |
. . . . . . . . . . . 12
β’ (π₯ = π€ β {π₯, π} = {π€, π}) |
36 | 35 | eleq2d 2820 |
. . . . . . . . . . 11
β’ (π₯ = π€ β (π€ β {π₯, π} β π€ β {π€, π})) |
37 | 35 | sseq1d 3976 |
. . . . . . . . . . 11
β’ (π₯ = π€ β ({π₯, π} β π§ β {π€, π} β π§)) |
38 | 36, 37 | anbi12d 632 |
. . . . . . . . . 10
β’ (π₯ = π€ β ((π€ β {π₯, π} β§ {π₯, π} β π§) β (π€ β {π€, π} β§ {π€, π} β π§))) |
39 | 38 | rspcev 3580 |
. . . . . . . . 9
β’ ((π€ β π΄ β§ (π€ β {π€, π} β§ {π€, π} β π§)) β βπ₯ β π΄ (π€ β {π₯, π} β§ {π₯, π} β π§)) |
40 | 25, 27, 34, 39 | syl12anc 836 |
. . . . . . . 8
β’ ((((π΄ β π β§ π β π΄) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
))) β§ π€ β π§) β βπ₯ β π΄ (π€ β {π₯, π} β§ {π₯, π} β π§)) |
41 | 10 | rgenw 3065 |
. . . . . . . . 9
β’
βπ₯ β
π΄ {π₯, π} β V |
42 | | eqid 2733 |
. . . . . . . . . 10
β’ (π₯ β π΄ β¦ {π₯, π}) = (π₯ β π΄ β¦ {π₯, π}) |
43 | | eleq2 2823 |
. . . . . . . . . . 11
β’ (π£ = {π₯, π} β (π€ β π£ β π€ β {π₯, π})) |
44 | | sseq1 3970 |
. . . . . . . . . . 11
β’ (π£ = {π₯, π} β (π£ β π§ β {π₯, π} β π§)) |
45 | 43, 44 | anbi12d 632 |
. . . . . . . . . 10
β’ (π£ = {π₯, π} β ((π€ β π£ β§ π£ β π§) β (π€ β {π₯, π} β§ {π₯, π} β π§))) |
46 | 42, 45 | rexrnmptw 7046 |
. . . . . . . . 9
β’
(βπ₯ β
π΄ {π₯, π} β V β (βπ£ β ran (π₯ β π΄ β¦ {π₯, π})(π€ β π£ β§ π£ β π§) β βπ₯ β π΄ (π€ β {π₯, π} β§ {π₯, π} β π§))) |
47 | 41, 46 | ax-mp 5 |
. . . . . . . 8
β’
(βπ£ β ran
(π₯ β π΄ β¦ {π₯, π})(π€ β π£ β§ π£ β π§) β βπ₯ β π΄ (π€ β {π₯, π} β§ {π₯, π} β π§)) |
48 | 40, 47 | sylibr 233 |
. . . . . . 7
β’ ((((π΄ β π β§ π β π΄) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
))) β§ π€ β π§) β βπ£ β ran (π₯ β π΄ β¦ {π₯, π})(π€ β π£ β§ π£ β π§)) |
49 | 48 | ralrimiva 3140 |
. . . . . 6
β’ (((π΄ β π β§ π β π΄) β§ (π§ β π« π΄ β§ (π β π§ β¨ π§ = β
))) β βπ€ β π§ βπ£ β ran (π₯ β π΄ β¦ {π₯, π})(π€ β π£ β§ π£ β π§)) |
50 | 49 | ex 414 |
. . . . 5
β’ ((π΄ β π β§ π β π΄) β ((π§ β π« π΄ β§ (π β π§ β¨ π§ = β
)) β βπ€ β π§ βπ£ β ran (π₯ β π΄ β¦ {π₯, π})(π€ β π£ β§ π£ β π§))) |
51 | 22, 50 | biimtrid 241 |
. . . 4
β’ ((π΄ β π β§ π β π΄) β (π§ β {π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)} β βπ€ β π§ βπ£ β ran (π₯ β π΄ β¦ {π₯, π})(π€ β π£ β§ π£ β π§))) |
52 | 51 | ralrimiv 3139 |
. . 3
β’ ((π΄ β π β§ π β π΄) β βπ§ β {π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)}βπ€ β π§ βπ£ β ran (π₯ β π΄ β¦ {π₯, π})(π€ β π£ β§ π£ β π§)) |
53 | | basgen2 22355 |
. . 3
β’ (({π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)} β Top β§ ran (π₯ β π΄ β¦ {π₯, π}) β {π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)} β§ βπ§ β {π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)}βπ€ β π§ βπ£ β ran (π₯ β π΄ β¦ {π₯, π})(π€ β π£ β§ π£ β π§)) β (topGenβran (π₯ β π΄ β¦ {π₯, π})) = {π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)}) |
54 | 3, 18, 52, 53 | syl3anc 1372 |
. 2
β’ ((π΄ β π β§ π β π΄) β (topGenβran (π₯ β π΄ β¦ {π₯, π})) = {π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)}) |
55 | | eleq2 2823 |
. . . 4
β’ (π¦ = π₯ β (π β π¦ β π β π₯)) |
56 | | eqeq1 2737 |
. . . 4
β’ (π¦ = π₯ β (π¦ = β
β π₯ = β
)) |
57 | 55, 56 | orbi12d 918 |
. . 3
β’ (π¦ = π₯ β ((π β π¦ β¨ π¦ = β
) β (π β π₯ β¨ π₯ = β
))) |
58 | 57 | cbvrabv 3416 |
. 2
β’ {π¦ β π« π΄ β£ (π β π¦ β¨ π¦ = β
)} = {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} |
59 | 54, 58 | eqtr2di 2790 |
1
β’ ((π΄ β π β§ π β π΄) β {π₯ β π« π΄ β£ (π β π₯ β¨ π₯ = β
)} = (topGenβran (π₯ β π΄ β¦ {π₯, π}))) |