Step | Hyp | Ref
| Expression |
1 | | toponsspwpw 22644 |
. . 3
β’
(TopOnβπ΅)
β π« π« π΅ |
2 | 1 | a1i 11 |
. 2
β’ (π΅ β π β (TopOnβπ΅) β π« π« π΅) |
3 | | distopon 22720 |
. 2
β’ (π΅ β π β π« π΅ β (TopOnβπ΅)) |
4 | | simpl 481 |
. . . . . . . . . . . . . 14
β’ ((π β (TopOnβπ΅) β§ π β β
) β π β (TopOnβπ΅)) |
5 | 4 | sselda 3981 |
. . . . . . . . . . . . 13
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ π₯ β π) β π₯ β (TopOnβπ΅)) |
6 | 5 | adantrl 712 |
. . . . . . . . . . . 12
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β π)) β π₯ β (TopOnβπ΅)) |
7 | | topontop 22635 |
. . . . . . . . . . . 12
β’ (π₯ β (TopOnβπ΅) β π₯ β Top) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . 11
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β π)) β π₯ β Top) |
9 | | simpl 481 |
. . . . . . . . . . . . 13
β’ ((π β β© π
β§ π₯ β π) β π β β© π) |
10 | | intss1 4966 |
. . . . . . . . . . . . . 14
β’ (π₯ β π β β© π β π₯) |
11 | 10 | adantl 480 |
. . . . . . . . . . . . 13
β’ ((π β β© π
β§ π₯ β π) β β© π
β π₯) |
12 | 9, 11 | sstrd 3991 |
. . . . . . . . . . . 12
β’ ((π β β© π
β§ π₯ β π) β π β π₯) |
13 | 12 | adantl 480 |
. . . . . . . . . . 11
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β π)) β π β π₯) |
14 | | uniopn 22619 |
. . . . . . . . . . 11
β’ ((π₯ β Top β§ π β π₯) β βͺ π β π₯) |
15 | 8, 13, 14 | syl2anc 582 |
. . . . . . . . . 10
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β π)) β βͺ π β π₯) |
16 | 15 | expr 455 |
. . . . . . . . 9
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ π β β© π) β (π₯ β π β βͺ π β π₯)) |
17 | 16 | ralrimiv 3143 |
. . . . . . . 8
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ π β β© π) β βπ₯ β π βͺ π β π₯) |
18 | | vuniex 7731 |
. . . . . . . . 9
β’ βͺ π
β V |
19 | 18 | elint2 4956 |
. . . . . . . 8
β’ (βͺ π
β β© π β βπ₯ β π βͺ π β π₯) |
20 | 17, 19 | sylibr 233 |
. . . . . . 7
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ π β β© π) β βͺ π
β β© π) |
21 | 20 | ex 411 |
. . . . . 6
β’ ((π β (TopOnβπ΅) β§ π β β
) β (π β β© π β βͺ π
β β© π)) |
22 | 21 | alrimiv 1928 |
. . . . 5
β’ ((π β (TopOnβπ΅) β§ π β β
) β βπ(π β β© π β βͺ π
β β© π)) |
23 | | simpll 763 |
. . . . . . . . . . 11
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β β© π)) β π β (TopOnβπ΅)) |
24 | 23 | sselda 3981 |
. . . . . . . . . 10
β’ ((((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β β© π)) β§ π¦ β π) β π¦ β (TopOnβπ΅)) |
25 | | topontop 22635 |
. . . . . . . . . 10
β’ (π¦ β (TopOnβπ΅) β π¦ β Top) |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
β’ ((((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β β© π)) β§ π¦ β π) β π¦ β Top) |
27 | | intss1 4966 |
. . . . . . . . . . 11
β’ (π¦ β π β β© π β π¦) |
28 | 27 | adantl 480 |
. . . . . . . . . 10
β’ ((((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β β© π)) β§ π¦ β π) β β© π β π¦) |
29 | | simplrl 773 |
. . . . . . . . . 10
β’ ((((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β β© π)) β§ π¦ β π) β π β β© π) |
30 | 28, 29 | sseldd 3982 |
. . . . . . . . 9
β’ ((((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β β© π)) β§ π¦ β π) β π β π¦) |
31 | | simplrr 774 |
. . . . . . . . . 10
β’ ((((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β β© π)) β§ π¦ β π) β π₯ β β© π) |
32 | 28, 31 | sseldd 3982 |
. . . . . . . . 9
β’ ((((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β β© π)) β§ π¦ β π) β π₯ β π¦) |
33 | | inopn 22621 |
. . . . . . . . 9
β’ ((π¦ β Top β§ π β π¦ β§ π₯ β π¦) β (π β© π₯) β π¦) |
34 | 26, 30, 32, 33 | syl3anc 1369 |
. . . . . . . 8
β’ ((((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β β© π)) β§ π¦ β π) β (π β© π₯) β π¦) |
35 | 34 | ralrimiva 3144 |
. . . . . . 7
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β β© π)) β βπ¦ β π (π β© π₯) β π¦) |
36 | | vex 3476 |
. . . . . . . . 9
β’ π β V |
37 | 36 | inex1 5316 |
. . . . . . . 8
β’ (π β© π₯) β V |
38 | 37 | elint2 4956 |
. . . . . . 7
β’ ((π β© π₯) β β© π β βπ¦ β π (π β© π₯) β π¦) |
39 | 35, 38 | sylibr 233 |
. . . . . 6
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β β© π)) β (π β© π₯) β β© π) |
40 | 39 | ralrimivva 3198 |
. . . . 5
β’ ((π β (TopOnβπ΅) β§ π β β
) β βπ β β© πβπ₯ β β© π(π β© π₯) β β© π) |
41 | | intex 5336 |
. . . . . . . 8
β’ (π β β
β β© π
β V) |
42 | 41 | biimpi 215 |
. . . . . . 7
β’ (π β β
β β© π
β V) |
43 | 42 | adantl 480 |
. . . . . 6
β’ ((π β (TopOnβπ΅) β§ π β β
) β β© π
β V) |
44 | | istopg 22617 |
. . . . . 6
β’ (β© π
β V β (β© π β Top β (βπ(π β β© π β βͺ π
β β© π) β§ βπ β β© πβπ₯ β β© π(π β© π₯) β β© π))) |
45 | 43, 44 | syl 17 |
. . . . 5
β’ ((π β (TopOnβπ΅) β§ π β β
) β (β© π
β Top β (βπ(π β β© π β βͺ π
β β© π) β§ βπ β β© πβπ₯ β β© π(π β© π₯) β β© π))) |
46 | 22, 40, 45 | mpbir2and 709 |
. . . 4
β’ ((π β (TopOnβπ΅) β§ π β β
) β β© π
β Top) |
47 | 46 | 3adant1 1128 |
. . 3
β’ ((π΅ β π β§ π β (TopOnβπ΅) β§ π β β
) β β© π
β Top) |
48 | | n0 4345 |
. . . . . . . . . . 11
β’ (π β β
β
βπ₯ π₯ β π) |
49 | 48 | biimpi 215 |
. . . . . . . . . 10
β’ (π β β
β
βπ₯ π₯ β π) |
50 | 49 | ad2antlr 723 |
. . . . . . . . 9
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ π β β© π) β βπ₯ π₯ β π) |
51 | 10 | sselda 3981 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β π β§ π β β© π) β π β π₯) |
52 | 51 | ancoms 457 |
. . . . . . . . . . . . . 14
β’ ((π β β© π
β§ π₯ β π) β π β π₯) |
53 | | elssuni 4940 |
. . . . . . . . . . . . . 14
β’ (π β π₯ β π β βͺ π₯) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β β© π
β§ π₯ β π) β π β βͺ π₯) |
55 | 54 | adantl 480 |
. . . . . . . . . . . 12
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β π)) β π β βͺ π₯) |
56 | 5 | adantrl 712 |
. . . . . . . . . . . . 13
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β π)) β π₯ β (TopOnβπ΅)) |
57 | | toponuni 22636 |
. . . . . . . . . . . . 13
β’ (π₯ β (TopOnβπ΅) β π΅ = βͺ π₯) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β π)) β π΅ = βͺ π₯) |
59 | 55, 58 | sseqtrrd 4022 |
. . . . . . . . . . 11
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ (π β β© π β§ π₯ β π)) β π β π΅) |
60 | 59 | expr 455 |
. . . . . . . . . 10
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ π β β© π) β (π₯ β π β π β π΅)) |
61 | 60 | exlimdv 1934 |
. . . . . . . . 9
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ π β β© π) β (βπ₯ π₯ β π β π β π΅)) |
62 | 50, 61 | mpd 15 |
. . . . . . . 8
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ π β β© π) β π β π΅) |
63 | 62 | ralrimiva 3144 |
. . . . . . 7
β’ ((π β (TopOnβπ΅) β§ π β β
) β βπ β β© ππ β π΅) |
64 | | unissb 4942 |
. . . . . . 7
β’ (βͺ β© π β π΅ β βπ β β© ππ β π΅) |
65 | 63, 64 | sylibr 233 |
. . . . . 6
β’ ((π β (TopOnβπ΅) β§ π β β
) β βͺ β© π β π΅) |
66 | 65 | 3adant1 1128 |
. . . . 5
β’ ((π΅ β π β§ π β (TopOnβπ΅) β§ π β β
) β βͺ β© π β π΅) |
67 | 4 | sselda 3981 |
. . . . . . . . . 10
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ π β π) β π β (TopOnβπ΅)) |
68 | | toponuni 22636 |
. . . . . . . . . 10
β’ (π β (TopOnβπ΅) β π΅ = βͺ π) |
69 | 67, 68 | syl 17 |
. . . . . . . . 9
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ π β π) β π΅ = βͺ π) |
70 | | topontop 22635 |
. . . . . . . . . 10
β’ (π β (TopOnβπ΅) β π β Top) |
71 | | eqid 2730 |
. . . . . . . . . . 11
β’ βͺ π =
βͺ π |
72 | 71 | topopn 22628 |
. . . . . . . . . 10
β’ (π β Top β βͺ π
β π) |
73 | 67, 70, 72 | 3syl 18 |
. . . . . . . . 9
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ π β π) β βͺ π β π) |
74 | 69, 73 | eqeltrd 2831 |
. . . . . . . 8
β’ (((π β (TopOnβπ΅) β§ π β β
) β§ π β π) β π΅ β π) |
75 | 74 | ralrimiva 3144 |
. . . . . . 7
β’ ((π β (TopOnβπ΅) β§ π β β
) β βπ β π π΅ β π) |
76 | 75 | 3adant1 1128 |
. . . . . 6
β’ ((π΅ β π β§ π β (TopOnβπ΅) β§ π β β
) β βπ β π π΅ β π) |
77 | | elintg 4957 |
. . . . . . 7
β’ (π΅ β π β (π΅ β β© π β βπ β π π΅ β π)) |
78 | 77 | 3ad2ant1 1131 |
. . . . . 6
β’ ((π΅ β π β§ π β (TopOnβπ΅) β§ π β β
) β (π΅ β β© π β βπ β π π΅ β π)) |
79 | 76, 78 | mpbird 256 |
. . . . 5
β’ ((π΅ β π β§ π β (TopOnβπ΅) β§ π β β
) β π΅ β β© π) |
80 | | unissel 4941 |
. . . . 5
β’ ((βͺ β© π β π΅ β§ π΅ β β© π) β βͺ β© π = π΅) |
81 | 66, 79, 80 | syl2anc 582 |
. . . 4
β’ ((π΅ β π β§ π β (TopOnβπ΅) β§ π β β
) β βͺ β© π = π΅) |
82 | 81 | eqcomd 2736 |
. . 3
β’ ((π΅ β π β§ π β (TopOnβπ΅) β§ π β β
) β π΅ = βͺ β© π) |
83 | | istopon 22634 |
. . 3
β’ (β© π
β (TopOnβπ΅)
β (β© π β Top β§ π΅ = βͺ β© π)) |
84 | 47, 82, 83 | sylanbrc 581 |
. 2
β’ ((π΅ β π β§ π β (TopOnβπ΅) β§ π β β
) β β© π
β (TopOnβπ΅)) |
85 | 2, 3, 84 | ismred 17550 |
1
β’ (π΅ β π β (TopOnβπ΅) β (Mooreβπ« π΅)) |