Step | Hyp | Ref
| Expression |
1 | | xpstopnlem1.f |
. . 3
β’ πΉ = (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©}) |
2 | | xpstopnlem1.j |
. . . . . . . . . 10
β’ (π β π½ β (TopOnβπ)) |
3 | | xpstopnlem1.k |
. . . . . . . . . 10
β’ (π β πΎ β (TopOnβπ)) |
4 | | txtopon 22894 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
5 | 2, 3, 4 | syl2anc 584 |
. . . . . . . . 9
β’ (π β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
6 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(βtβ{β¨β
, π½β©}) =
(βtβ{β¨β
, π½β©}) |
7 | | 0ex 5262 |
. . . . . . . . . . . . . 14
β’ β
β V |
8 | 7 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β β
β
V) |
9 | 6, 8, 2 | pt1hmeo 23109 |
. . . . . . . . . . . 12
β’ (π β (π§ β π β¦ {β¨β
, π§β©}) β (π½Homeo(βtβ{β¨β
,
π½β©}))) |
10 | | hmeocn 23063 |
. . . . . . . . . . . 12
β’ ((π§ β π β¦ {β¨β
, π§β©}) β (π½Homeo(βtβ{β¨β
,
π½β©})) β (π§ β π β¦ {β¨β
, π§β©}) β (π½ Cn (βtβ{β¨β
,
π½β©}))) |
11 | | cntop2 22544 |
. . . . . . . . . . . 12
β’ ((π§ β π β¦ {β¨β
, π§β©}) β (π½ Cn
(βtβ{β¨β
, π½β©})) β
(βtβ{β¨β
, π½β©}) β Top) |
12 | 9, 10, 11 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β
(βtβ{β¨β
, π½β©}) β Top) |
13 | | toptopon2 22219 |
. . . . . . . . . . 11
β’
((βtβ{β¨β
, π½β©}) β Top β
(βtβ{β¨β
, π½β©}) β (TopOnββͺ (βtβ{β¨β
, π½β©}))) |
14 | 12, 13 | sylib 217 |
. . . . . . . . . 10
β’ (π β
(βtβ{β¨β
, π½β©}) β (TopOnββͺ (βtβ{β¨β
, π½β©}))) |
15 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(βtβ{β¨1o, πΎβ©}) =
(βtβ{β¨1o, πΎβ©}) |
16 | | 1on 8416 |
. . . . . . . . . . . . . 14
β’
1o β On |
17 | 16 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β 1o β
On) |
18 | 15, 17, 3 | pt1hmeo 23109 |
. . . . . . . . . . . 12
β’ (π β (π§ β π β¦ {β¨1o, π§β©}) β (πΎHomeo(βtβ{β¨1o,
πΎβ©}))) |
19 | | hmeocn 23063 |
. . . . . . . . . . . 12
β’ ((π§ β π β¦ {β¨1o, π§β©}) β (πΎHomeo(βtβ{β¨1o,
πΎβ©})) β (π§ β π β¦ {β¨1o, π§β©}) β (πΎ Cn (βtβ{β¨1o,
πΎβ©}))) |
20 | | cntop2 22544 |
. . . . . . . . . . . 12
β’ ((π§ β π β¦ {β¨1o, π§β©}) β (πΎ Cn
(βtβ{β¨1o, πΎβ©})) β
(βtβ{β¨1o, πΎβ©}) β Top) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β
(βtβ{β¨1o, πΎβ©}) β Top) |
22 | | toptopon2 22219 |
. . . . . . . . . . 11
β’
((βtβ{β¨1o, πΎβ©}) β Top β
(βtβ{β¨1o, πΎβ©}) β (TopOnββͺ (βtβ{β¨1o, πΎβ©}))) |
23 | 21, 22 | sylib 217 |
. . . . . . . . . 10
β’ (π β
(βtβ{β¨1o, πΎβ©}) β (TopOnββͺ (βtβ{β¨1o, πΎβ©}))) |
24 | | txtopon 22894 |
. . . . . . . . . 10
β’
(((βtβ{β¨β
, π½β©}) β (TopOnββͺ (βtβ{β¨β
, π½β©})) β§
(βtβ{β¨1o, πΎβ©}) β (TopOnββͺ (βtβ{β¨1o, πΎβ©}))) β
((βtβ{β¨β
, π½β©}) Γt
(βtβ{β¨1o, πΎβ©})) β (TopOnβ(βͺ (βtβ{β¨β
, π½β©}) Γ βͺ (βtβ{β¨1o, πΎβ©})))) |
25 | 14, 23, 24 | syl2anc 584 |
. . . . . . . . 9
β’ (π β
((βtβ{β¨β
, π½β©}) Γt
(βtβ{β¨1o, πΎβ©})) β (TopOnβ(βͺ (βtβ{β¨β
, π½β©}) Γ βͺ (βtβ{β¨1o, πΎβ©})))) |
26 | | opeq2 4829 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π₯ β β¨β
, π§β© = β¨β
, π₯β©) |
27 | 26 | sneqd 4596 |
. . . . . . . . . . . . . . 15
β’ (π§ = π₯ β {β¨β
, π§β©} = {β¨β
, π₯β©}) |
28 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ (π§ β π β¦ {β¨β
, π§β©}) = (π§ β π β¦ {β¨β
, π§β©}) |
29 | | snex 5386 |
. . . . . . . . . . . . . . 15
β’
{β¨β
, π₯β©} β V |
30 | 27, 28, 29 | fvmpt 6945 |
. . . . . . . . . . . . . 14
β’ (π₯ β π β ((π§ β π β¦ {β¨β
, π§β©})βπ₯) = {β¨β
, π₯β©}) |
31 | | opeq2 4829 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π¦ β β¨1o, π§β© = β¨1o,
π¦β©) |
32 | 31 | sneqd 4596 |
. . . . . . . . . . . . . . 15
β’ (π§ = π¦ β {β¨1o, π§β©} = {β¨1o,
π¦β©}) |
33 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ (π§ β π β¦ {β¨1o, π§β©}) = (π§ β π β¦ {β¨1o, π§β©}) |
34 | | snex 5386 |
. . . . . . . . . . . . . . 15
β’
{β¨1o, π¦β©} β V |
35 | 32, 33, 34 | fvmpt 6945 |
. . . . . . . . . . . . . 14
β’ (π¦ β π β ((π§ β π β¦ {β¨1o, π§β©})βπ¦) = {β¨1o, π¦β©}) |
36 | | opeq12 4830 |
. . . . . . . . . . . . . 14
β’ ((((π§ β π β¦ {β¨β
, π§β©})βπ₯) = {β¨β
, π₯β©} β§ ((π§ β π β¦ {β¨1o, π§β©})βπ¦) = {β¨1o, π¦β©}) β β¨((π§ β π β¦ {β¨β
, π§β©})βπ₯), ((π§ β π β¦ {β¨1o, π§β©})βπ¦)β© = β¨{β¨β
,
π₯β©},
{β¨1o, π¦β©}β©) |
37 | 30, 35, 36 | syl2an 596 |
. . . . . . . . . . . . 13
β’ ((π₯ β π β§ π¦ β π) β β¨((π§ β π β¦ {β¨β
, π§β©})βπ₯), ((π§ β π β¦ {β¨1o, π§β©})βπ¦)β© = β¨{β¨β
,
π₯β©},
{β¨1o, π¦β©}β©) |
38 | 37 | mpoeq3ia 7429 |
. . . . . . . . . . . 12
β’ (π₯ β π, π¦ β π β¦ β¨((π§ β π β¦ {β¨β
, π§β©})βπ₯), ((π§ β π β¦ {β¨1o, π§β©})βπ¦)β©) = (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©) |
39 | | toponuni 22215 |
. . . . . . . . . . . . . 14
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
40 | 2, 39 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π = βͺ π½) |
41 | | toponuni 22215 |
. . . . . . . . . . . . . 14
β’ (πΎ β (TopOnβπ) β π = βͺ πΎ) |
42 | 3, 41 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π = βͺ πΎ) |
43 | | mpoeq12 7424 |
. . . . . . . . . . . . 13
β’ ((π = βͺ
π½ β§ π = βͺ πΎ) β (π₯ β π, π¦ β π β¦ β¨((π§ β π β¦ {β¨β
, π§β©})βπ₯), ((π§ β π β¦ {β¨1o, π§β©})βπ¦)β©) = (π₯ β βͺ π½, π¦ β βͺ πΎ β¦ β¨((π§ β π β¦ {β¨β
, π§β©})βπ₯), ((π§ β π β¦ {β¨1o, π§β©})βπ¦)β©)) |
44 | 40, 42, 43 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (π β (π₯ β π, π¦ β π β¦ β¨((π§ β π β¦ {β¨β
, π§β©})βπ₯), ((π§ β π β¦ {β¨1o, π§β©})βπ¦)β©) = (π₯ β βͺ π½, π¦ β βͺ πΎ β¦ β¨((π§ β π β¦ {β¨β
, π§β©})βπ₯), ((π§ β π β¦ {β¨1o, π§β©})βπ¦)β©)) |
45 | 38, 44 | eqtr3id 2791 |
. . . . . . . . . . 11
β’ (π β (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©) = (π₯ β βͺ π½,
π¦ β βͺ πΎ
β¦ β¨((π§ β
π β¦ {β¨β
,
π§β©})βπ₯), ((π§ β π β¦ {β¨1o, π§β©})βπ¦)β©)) |
46 | | eqid 2737 |
. . . . . . . . . . . 12
β’ βͺ π½ =
βͺ π½ |
47 | | eqid 2737 |
. . . . . . . . . . . 12
β’ βͺ πΎ =
βͺ πΎ |
48 | 46, 47, 9, 18 | txhmeo 23106 |
. . . . . . . . . . 11
β’ (π β (π₯ β βͺ π½, π¦ β βͺ πΎ β¦ β¨((π§ β π β¦ {β¨β
, π§β©})βπ₯), ((π§ β π β¦ {β¨1o, π§β©})βπ¦)β©) β ((π½ Γt πΎ)Homeo((βtβ{β¨β
,
π½β©}) Γt
(βtβ{β¨1o, πΎβ©})))) |
49 | 45, 48 | eqeltrd 2838 |
. . . . . . . . . 10
β’ (π β (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©) β
((π½ Γt
πΎ)Homeo((βtβ{β¨β
,
π½β©}) Γt
(βtβ{β¨1o, πΎβ©})))) |
50 | | hmeocn 23063 |
. . . . . . . . . 10
β’ ((π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©) β
((π½ Γt
πΎ)Homeo((βtβ{β¨β
,
π½β©}) Γt
(βtβ{β¨1o, πΎβ©}))) β (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o, π¦β©}β©) β ((π½ Γt πΎ) Cn
((βtβ{β¨β
, π½β©}) Γt
(βtβ{β¨1o, πΎβ©})))) |
51 | 49, 50 | syl 17 |
. . . . . . . . 9
β’ (π β (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©) β
((π½ Γt
πΎ) Cn
((βtβ{β¨β
, π½β©}) Γt
(βtβ{β¨1o, πΎβ©})))) |
52 | | cnf2 22552 |
. . . . . . . . 9
β’ (((π½ Γt πΎ) β (TopOnβ(π Γ π)) β§
((βtβ{β¨β
, π½β©}) Γt
(βtβ{β¨1o, πΎβ©})) β (TopOnβ(βͺ (βtβ{β¨β
, π½β©}) Γ βͺ (βtβ{β¨1o, πΎβ©}))) β§ (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©) β
((π½ Γt
πΎ) Cn
((βtβ{β¨β
, π½β©}) Γt
(βtβ{β¨1o, πΎβ©})))) β (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©):(π Γ π)βΆ(βͺ
(βtβ{β¨β
, π½β©}) Γ βͺ (βtβ{β¨1o, πΎβ©}))) |
53 | 5, 25, 51, 52 | syl3anc 1371 |
. . . . . . . 8
β’ (π β (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©):(π Γ π)βΆ(βͺ
(βtβ{β¨β
, π½β©}) Γ βͺ (βtβ{β¨1o, πΎβ©}))) |
54 | | eqid 2737 |
. . . . . . . . 9
β’ (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©) = (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©) |
55 | 54 | fmpo 7992 |
. . . . . . . 8
β’
(βπ₯ β
π βπ¦ β π β¨{β¨β
, π₯β©}, {β¨1o, π¦β©}β© β (βͺ (βtβ{β¨β
, π½β©}) Γ βͺ (βtβ{β¨1o, πΎβ©})) β (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©):(π Γ π)βΆ(βͺ
(βtβ{β¨β
, π½β©}) Γ βͺ (βtβ{β¨1o, πΎβ©}))) |
56 | 53, 55 | sylibr 233 |
. . . . . . 7
β’ (π β βπ₯ β π βπ¦ β π β¨{β¨β
, π₯β©}, {β¨1o, π¦β©}β© β (βͺ (βtβ{β¨β
, π½β©}) Γ βͺ (βtβ{β¨1o, πΎβ©}))) |
57 | 56 | r19.21bi 3232 |
. . . . . 6
β’ ((π β§ π₯ β π) β βπ¦ β π β¨{β¨β
, π₯β©}, {β¨1o, π¦β©}β© β (βͺ (βtβ{β¨β
, π½β©}) Γ βͺ (βtβ{β¨1o, πΎβ©}))) |
58 | 57 | r19.21bi 3232 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π¦ β π) β β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β© β
(βͺ (βtβ{β¨β
, π½β©}) Γ βͺ (βtβ{β¨1o, πΎβ©}))) |
59 | 58 | anasss 467 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π)) β β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β© β
(βͺ (βtβ{β¨β
, π½β©}) Γ βͺ (βtβ{β¨1o, πΎβ©}))) |
60 | | eqidd 2738 |
. . . 4
β’ (π β (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©) = (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©)) |
61 | | vex 3447 |
. . . . . . . . 9
β’ π₯ β V |
62 | | vex 3447 |
. . . . . . . . 9
β’ π¦ β V |
63 | 61, 62 | op1std 7923 |
. . . . . . . 8
β’ (π§ = β¨π₯, π¦β© β (1st βπ§) = π₯) |
64 | 61, 62 | op2ndd 7924 |
. . . . . . . 8
β’ (π§ = β¨π₯, π¦β© β (2nd βπ§) = π¦) |
65 | 63, 64 | uneq12d 4122 |
. . . . . . 7
β’ (π§ = β¨π₯, π¦β© β ((1st βπ§) βͺ (2nd
βπ§)) = (π₯ βͺ π¦)) |
66 | 65 | mpompt 7464 |
. . . . . 6
β’ (π§ β (βͺ (βtβ{β¨β
, π½β©}) Γ βͺ (βtβ{β¨1o, πΎβ©})) β¦
((1st βπ§)
βͺ (2nd βπ§))) = (π₯ β βͺ
(βtβ{β¨β
, π½β©}), π¦ β βͺ
(βtβ{β¨1o, πΎβ©}) β¦ (π₯ βͺ π¦)) |
67 | 66 | eqcomi 2746 |
. . . . 5
β’ (π₯ β βͺ (βtβ{β¨β
, π½β©}), π¦ β βͺ
(βtβ{β¨1o, πΎβ©}) β¦ (π₯ βͺ π¦)) = (π§ β (βͺ
(βtβ{β¨β
, π½β©}) Γ βͺ (βtβ{β¨1o, πΎβ©})) β¦
((1st βπ§)
βͺ (2nd βπ§))) |
68 | 67 | a1i 11 |
. . . 4
β’ (π β (π₯ β βͺ
(βtβ{β¨β
, π½β©}), π¦ β βͺ
(βtβ{β¨1o, πΎβ©}) β¦ (π₯ βͺ π¦)) = (π§ β (βͺ
(βtβ{β¨β
, π½β©}) Γ βͺ (βtβ{β¨1o, πΎβ©})) β¦
((1st βπ§)
βͺ (2nd βπ§)))) |
69 | 29, 34 | op1std 7923 |
. . . . . 6
β’ (π§ = β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β© β
(1st βπ§) =
{β¨β
, π₯β©}) |
70 | 29, 34 | op2ndd 7924 |
. . . . . 6
β’ (π§ = β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β© β
(2nd βπ§) =
{β¨1o, π¦β©}) |
71 | 69, 70 | uneq12d 4122 |
. . . . 5
β’ (π§ = β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β© β
((1st βπ§)
βͺ (2nd βπ§)) = ({β¨β
, π₯β©} βͺ {β¨1o, π¦β©})) |
72 | | df-pr 4587 |
. . . . 5
β’
{β¨β
, π₯β©, β¨1o, π¦β©} = ({β¨β
, π₯β©} βͺ
{β¨1o, π¦β©}) |
73 | 71, 72 | eqtr4di 2795 |
. . . 4
β’ (π§ = β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β© β
((1st βπ§)
βͺ (2nd βπ§)) = {β¨β
, π₯β©, β¨1o, π¦β©}) |
74 | 59, 60, 68, 73 | fmpoco 8019 |
. . 3
β’ (π β ((π₯ β βͺ
(βtβ{β¨β
, π½β©}), π¦ β βͺ
(βtβ{β¨1o, πΎβ©}) β¦ (π₯ βͺ π¦)) β (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©)) = (π₯ β π, π¦ β π β¦ {β¨β
, π₯β©, β¨1o, π¦β©})) |
75 | 1, 74 | eqtr4id 2796 |
. 2
β’ (π β πΉ = ((π₯ β βͺ
(βtβ{β¨β
, π½β©}), π¦ β βͺ
(βtβ{β¨1o, πΎβ©}) β¦ (π₯ βͺ π¦)) β (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©))) |
76 | | eqid 2737 |
. . . . 5
β’ βͺ (βtβ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ
{β
})) = βͺ
(βtβ({β¨β
, π½β©, β¨1o, πΎβ©} βΎ
{β
})) |
77 | | eqid 2737 |
. . . . 5
β’ βͺ (βtβ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ
{1o})) = βͺ
(βtβ({β¨β
, π½β©, β¨1o, πΎβ©} βΎ
{1o})) |
78 | | eqid 2737 |
. . . . 5
β’
(βtβ{β¨β
, π½β©, β¨1o, πΎβ©}) =
(βtβ{β¨β
, π½β©, β¨1o, πΎβ©}) |
79 | | eqid 2737 |
. . . . 5
β’
(βtβ({β¨β
, π½β©, β¨1o, πΎβ©} βΎ {β
})) =
(βtβ({β¨β
, π½β©, β¨1o, πΎβ©} βΎ
{β
})) |
80 | | eqid 2737 |
. . . . 5
β’
(βtβ({β¨β
, π½β©, β¨1o, πΎβ©} βΎ
{1o})) = (βtβ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ
{1o})) |
81 | | eqid 2737 |
. . . . 5
β’ (π₯ β βͺ (βtβ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ
{β
})), π¦ β βͺ (βtβ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ
{1o})) β¦ (π₯ βͺ π¦)) = (π₯ β βͺ
(βtβ({β¨β
, π½β©, β¨1o, πΎβ©} βΎ {β
})),
π¦ β βͺ (βtβ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ
{1o})) β¦ (π₯ βͺ π¦)) |
82 | | 2on 8418 |
. . . . . 6
β’
2o β On |
83 | 82 | a1i 11 |
. . . . 5
β’ (π β 2o β
On) |
84 | | topontop 22214 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β π½ β Top) |
85 | 2, 84 | syl 17 |
. . . . . 6
β’ (π β π½ β Top) |
86 | | topontop 22214 |
. . . . . . 7
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
87 | 3, 86 | syl 17 |
. . . . . 6
β’ (π β πΎ β Top) |
88 | | xpscf 17407 |
. . . . . 6
β’
({β¨β
, π½β©, β¨1o, πΎβ©}:2oβΆTop
β (π½ β Top β§
πΎ β
Top)) |
89 | 85, 87, 88 | sylanbrc 583 |
. . . . 5
β’ (π β {β¨β
, π½β©, β¨1o,
πΎβ©}:2oβΆTop) |
90 | | df2o3 8412 |
. . . . . . 7
β’
2o = {β
, 1o} |
91 | | df-pr 4587 |
. . . . . . 7
β’ {β
,
1o} = ({β
} βͺ {1o}) |
92 | 90, 91 | eqtri 2765 |
. . . . . 6
β’
2o = ({β
} βͺ {1o}) |
93 | 92 | a1i 11 |
. . . . 5
β’ (π β 2o = ({β
}
βͺ {1o})) |
94 | | 1n0 8426 |
. . . . . . 7
β’
1o β β
|
95 | 94 | necomi 2996 |
. . . . . 6
β’ β
β 1o |
96 | | disjsn2 4671 |
. . . . . 6
β’ (β
β 1o β ({β
} β© {1o}) =
β
) |
97 | 95, 96 | mp1i 13 |
. . . . 5
β’ (π β ({β
} β©
{1o}) = β
) |
98 | 76, 77, 78, 79, 80, 81, 83, 89, 93, 97 | ptunhmeo 23111 |
. . . 4
β’ (π β (π₯ β βͺ
(βtβ({β¨β
, π½β©, β¨1o, πΎβ©} βΎ {β
})),
π¦ β βͺ (βtβ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ
{1o})) β¦ (π₯ βͺ π¦)) β
(((βtβ({β¨β
, π½β©, β¨1o, πΎβ©} βΎ {β
}))
Γt (βtβ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ
{1o})))Homeo(βtβ{β¨β
, π½β©, β¨1o,
πΎβ©}))) |
99 | | fnpr2o 17399 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β {β¨β
, π½β©, β¨1o, πΎβ©} Fn
2o) |
100 | 2, 3, 99 | syl2anc 584 |
. . . . . . . . 9
β’ (π β {β¨β
, π½β©, β¨1o,
πΎβ©} Fn
2o) |
101 | 7 | prid1 4721 |
. . . . . . . . . 10
β’ β
β {β
, 1o} |
102 | 101, 90 | eleqtrri 2837 |
. . . . . . . . 9
β’ β
β 2o |
103 | | fnressn 7100 |
. . . . . . . . 9
β’
(({β¨β
, π½β©, β¨1o, πΎβ©} Fn 2o β§
β
β 2o) β ({β¨β
, π½β©, β¨1o, πΎβ©} βΎ {β
}) =
{β¨β
, ({β¨β
, π½β©, β¨1o, πΎβ©}ββ
)β©}) |
104 | 100, 102,
103 | sylancl 586 |
. . . . . . . 8
β’ (π β ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ {β
})
= {β¨β
, ({β¨β
, π½β©, β¨1o, πΎβ©}ββ
)β©}) |
105 | | fvpr0o 17401 |
. . . . . . . . . . 11
β’ (π½ β (TopOnβπ) β ({β¨β
, π½β©, β¨1o,
πΎβ©}ββ
) =
π½) |
106 | 2, 105 | syl 17 |
. . . . . . . . . 10
β’ (π β ({β¨β
, π½β©, β¨1o,
πΎβ©}ββ
) =
π½) |
107 | 106 | opeq2d 4835 |
. . . . . . . . 9
β’ (π β β¨β
,
({β¨β
, π½β©,
β¨1o, πΎβ©}ββ
)β© =
β¨β
, π½β©) |
108 | 107 | sneqd 4596 |
. . . . . . . 8
β’ (π β {β¨β
,
({β¨β
, π½β©,
β¨1o, πΎβ©}ββ
)β©} =
{β¨β
, π½β©}) |
109 | 104, 108 | eqtrd 2777 |
. . . . . . 7
β’ (π β ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ {β
})
= {β¨β
, π½β©}) |
110 | 109 | fveq2d 6843 |
. . . . . 6
β’ (π β
(βtβ({β¨β
, π½β©, β¨1o, πΎβ©} βΎ {β
})) =
(βtβ{β¨β
, π½β©})) |
111 | 110 | unieqd 4877 |
. . . . 5
β’ (π β βͺ (βtβ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ
{β
})) = βͺ
(βtβ{β¨β
, π½β©})) |
112 | | 1oex 8414 |
. . . . . . . . . . 11
β’
1o β V |
113 | 112 | prid2 4722 |
. . . . . . . . . 10
β’
1o β {β
, 1o} |
114 | 113, 90 | eleqtrri 2837 |
. . . . . . . . 9
β’
1o β 2o |
115 | | fnressn 7100 |
. . . . . . . . 9
β’
(({β¨β
, π½β©, β¨1o, πΎβ©} Fn 2o β§
1o β 2o) β ({β¨β
, π½β©, β¨1o, πΎβ©} βΎ {1o})
= {β¨1o, ({β¨β
, π½β©, β¨1o, πΎβ©}β1o)β©}) |
116 | 100, 114,
115 | sylancl 586 |
. . . . . . . 8
β’ (π β ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ
{1o}) = {β¨1o, ({β¨β
, π½β©, β¨1o, πΎβ©}β1o)β©}) |
117 | | fvpr1o 17402 |
. . . . . . . . . . 11
β’ (πΎ β (TopOnβπ) β ({β¨β
, π½β©, β¨1o,
πΎβ©}β1o) = πΎ) |
118 | 3, 117 | syl 17 |
. . . . . . . . . 10
β’ (π β ({β¨β
, π½β©, β¨1o,
πΎβ©}β1o) = πΎ) |
119 | 118 | opeq2d 4835 |
. . . . . . . . 9
β’ (π β β¨1o,
({β¨β
, π½β©,
β¨1o, πΎβ©}β1o)β© =
β¨1o, πΎβ©) |
120 | 119 | sneqd 4596 |
. . . . . . . 8
β’ (π β {β¨1o,
({β¨β
, π½β©,
β¨1o, πΎβ©}β1o)β©} =
{β¨1o, πΎβ©}) |
121 | 116, 120 | eqtrd 2777 |
. . . . . . 7
β’ (π β ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ
{1o}) = {β¨1o, πΎβ©}) |
122 | 121 | fveq2d 6843 |
. . . . . 6
β’ (π β
(βtβ({β¨β
, π½β©, β¨1o, πΎβ©} βΎ
{1o})) = (βtβ{β¨1o, πΎβ©})) |
123 | 122 | unieqd 4877 |
. . . . 5
β’ (π β βͺ (βtβ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ
{1o})) = βͺ
(βtβ{β¨1o, πΎβ©})) |
124 | | eqidd 2738 |
. . . . 5
β’ (π β (π₯ βͺ π¦) = (π₯ βͺ π¦)) |
125 | 111, 123,
124 | mpoeq123dv 7426 |
. . . 4
β’ (π β (π₯ β βͺ
(βtβ({β¨β
, π½β©, β¨1o, πΎβ©} βΎ {β
})),
π¦ β βͺ (βtβ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ
{1o})) β¦ (π₯ βͺ π¦)) = (π₯ β βͺ
(βtβ{β¨β
, π½β©}), π¦ β βͺ
(βtβ{β¨1o, πΎβ©}) β¦ (π₯ βͺ π¦))) |
126 | 110, 122 | oveq12d 7369 |
. . . . 5
β’ (π β
((βtβ({β¨β
, π½β©, β¨1o, πΎβ©} βΎ {β
}))
Γt (βtβ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ
{1o}))) = ((βtβ{β¨β
, π½β©}) Γt
(βtβ{β¨1o, πΎβ©}))) |
127 | 126 | oveq1d 7366 |
. . . 4
β’ (π β
(((βtβ({β¨β
, π½β©, β¨1o, πΎβ©} βΎ {β
}))
Γt (βtβ({β¨β
, π½β©, β¨1o,
πΎβ©} βΎ
{1o})))Homeo(βtβ{β¨β
, π½β©, β¨1o,
πΎβ©})) =
(((βtβ{β¨β
, π½β©}) Γt
(βtβ{β¨1o, πΎβ©}))Homeo(βtβ{β¨β
,
π½β©, β¨1o, πΎβ©}))) |
128 | 98, 125, 127 | 3eltr3d 2852 |
. . 3
β’ (π β (π₯ β βͺ
(βtβ{β¨β
, π½β©}), π¦ β βͺ
(βtβ{β¨1o, πΎβ©}) β¦ (π₯ βͺ π¦)) β
(((βtβ{β¨β
, π½β©}) Γt
(βtβ{β¨1o, πΎβ©}))Homeo(βtβ{β¨β
,
π½β©, β¨1o, πΎβ©}))) |
129 | | hmeoco 23075 |
. . 3
β’ (((π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©) β
((π½ Γt
πΎ)Homeo((βtβ{β¨β
,
π½β©}) Γt
(βtβ{β¨1o, πΎβ©}))) β§ (π₯ β βͺ
(βtβ{β¨β
, π½β©}), π¦ β βͺ
(βtβ{β¨1o, πΎβ©}) β¦ (π₯ βͺ π¦)) β
(((βtβ{β¨β
, π½β©}) Γt
(βtβ{β¨1o, πΎβ©}))Homeo(βtβ{β¨β
,
π½β©, β¨1o, πΎβ©}))) β ((π₯ β βͺ
(βtβ{β¨β
, π½β©}), π¦ β βͺ
(βtβ{β¨1o, πΎβ©}) β¦ (π₯ βͺ π¦)) β (π₯ β π, π¦
β π β¦ β¨{β¨β
,
π₯β©}, {β¨1o, π¦β©}β©)) β ((π½ Γt πΎ)Homeo(βtβ{β¨β
, π½β©, β¨1o, πΎβ©}))) |
130 | 49, 128, 129 | syl2anc 584 |
. 2
β’ (π β ((π₯ β βͺ
(βtβ{β¨β
, π½β©}), π¦ β βͺ
(βtβ{β¨1o, πΎβ©}) β¦ (π₯ βͺ π¦)) β (π₯ β π, π¦ β π β¦ β¨{β¨β
, π₯β©}, {β¨1o,
π¦β©}β©)) β
((π½ Γt
πΎ)Homeo(βtβ{β¨β
,
π½β©, β¨1o,
πΎβ©}))) |
131 | 75, 130 | eqeltrd 2838 |
1
β’ (π β πΉ β ((π½ Γt πΎ)Homeo(βtβ{β¨β
,
π½β©, β¨1o,
πΎβ©}))) |