Step | Hyp | Ref
| Expression |
1 | | df-htpy 24285 |
. . . . . 6
β’ Htpy =
(π β Top, π β Top β¦ (π β (π Cn π), π β (π Cn π) β¦ {β β ((π Γt II) Cn π) β£ βπ β βͺ π((π β0) = (πβπ ) β§ (π β1) = (πβπ ))})) |
2 | 1 | a1i 11 |
. . . . 5
β’ (π β Htpy = (π β Top, π β Top β¦ (π β (π Cn π), π β (π Cn π) β¦ {β β ((π Γt II) Cn π) β£ βπ β βͺ π((π β0) = (πβπ ) β§ (π β1) = (πβπ ))}))) |
3 | | simprl 769 |
. . . . . . 7
β’ ((π β§ (π = π½ β§ π = πΎ)) β π = π½) |
4 | | simprr 771 |
. . . . . . 7
β’ ((π β§ (π = π½ β§ π = πΎ)) β π = πΎ) |
5 | 3, 4 | oveq12d 7369 |
. . . . . 6
β’ ((π β§ (π = π½ β§ π = πΎ)) β (π Cn π) = (π½ Cn πΎ)) |
6 | 3 | oveq1d 7366 |
. . . . . . . 8
β’ ((π β§ (π = π½ β§ π = πΎ)) β (π Γt II) = (π½ Γt II)) |
7 | 6, 4 | oveq12d 7369 |
. . . . . . 7
β’ ((π β§ (π = π½ β§ π = πΎ)) β ((π Γt II) Cn π) = ((π½ Γt II) Cn πΎ)) |
8 | 3 | unieqd 4877 |
. . . . . . . . 9
β’ ((π β§ (π = π½ β§ π = πΎ)) β βͺ π = βͺ
π½) |
9 | | ishtpy.1 |
. . . . . . . . . . 11
β’ (π β π½ β (TopOnβπ)) |
10 | | toponuni 22215 |
. . . . . . . . . . 11
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
β’ (π β π = βͺ π½) |
12 | 11 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (π = π½ β§ π = πΎ)) β π = βͺ π½) |
13 | 8, 12 | eqtr4d 2780 |
. . . . . . . 8
β’ ((π β§ (π = π½ β§ π = πΎ)) β βͺ π = π) |
14 | 13 | raleqdv 3311 |
. . . . . . 7
β’ ((π β§ (π = π½ β§ π = πΎ)) β (βπ β βͺ π((π β0) = (πβπ ) β§ (π β1) = (πβπ )) β βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ )))) |
15 | 7, 14 | rabeqbidv 3422 |
. . . . . 6
β’ ((π β§ (π = π½ β§ π = πΎ)) β {β β ((π Γt II) Cn π) β£ βπ β βͺ π((π β0) = (πβπ ) β§ (π β1) = (πβπ ))} = {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))}) |
16 | 5, 5, 15 | mpoeq123dv 7426 |
. . . . 5
β’ ((π β§ (π = π½ β§ π = πΎ)) β (π β (π Cn π), π β (π Cn π) β¦ {β β ((π Γt II) Cn π) β£ βπ β βͺ π((π β0) = (πβπ ) β§ (π β1) = (πβπ ))}) = (π β (π½ Cn πΎ), π β (π½ Cn πΎ) β¦ {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))})) |
17 | | topontop 22214 |
. . . . . 6
β’ (π½ β (TopOnβπ) β π½ β Top) |
18 | 9, 17 | syl 17 |
. . . . 5
β’ (π β π½ β Top) |
19 | | ishtpy.3 |
. . . . . 6
β’ (π β πΉ β (π½ Cn πΎ)) |
20 | | cntop2 22544 |
. . . . . 6
β’ (πΉ β (π½ Cn πΎ) β πΎ β Top) |
21 | 19, 20 | syl 17 |
. . . . 5
β’ (π β πΎ β Top) |
22 | | ovex 7384 |
. . . . . . . . . 10
β’ ((π½ Γt II) Cn
πΎ) β
V |
23 | | ssrab2 4035 |
. . . . . . . . . 10
β’ {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))} β ((π½ Γt II) Cn πΎ) |
24 | 22, 23 | elpwi2 5301 |
. . . . . . . . 9
β’ {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))} β π« ((π½ Γt II) Cn πΎ) |
25 | 24 | rgen2w 3067 |
. . . . . . . 8
β’
βπ β
(π½ Cn πΎ)βπ β (π½ Cn πΎ){β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))} β π« ((π½ Γt II) Cn πΎ) |
26 | | eqid 2737 |
. . . . . . . . 9
β’ (π β (π½ Cn πΎ), π β (π½ Cn πΎ) β¦ {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))}) = (π β (π½ Cn πΎ), π β (π½ Cn πΎ) β¦ {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))}) |
27 | 26 | fmpo 7992 |
. . . . . . . 8
β’
(βπ β
(π½ Cn πΎ)βπ β (π½ Cn πΎ){β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))} β π« ((π½ Γt II) Cn πΎ) β (π β (π½ Cn πΎ), π β (π½ Cn πΎ) β¦ {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))}):((π½ Cn πΎ) Γ (π½ Cn πΎ))βΆπ« ((π½ Γt II) Cn πΎ)) |
28 | 25, 27 | mpbi 229 |
. . . . . . 7
β’ (π β (π½ Cn πΎ), π β (π½ Cn πΎ) β¦ {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))}):((π½ Cn πΎ) Γ (π½ Cn πΎ))βΆπ« ((π½ Γt II) Cn πΎ) |
29 | | ovex 7384 |
. . . . . . . 8
β’ (π½ Cn πΎ) β V |
30 | 29, 29 | xpex 7679 |
. . . . . . 7
β’ ((π½ Cn πΎ) Γ (π½ Cn πΎ)) β V |
31 | 22 | pwex 5333 |
. . . . . . 7
β’ π«
((π½ Γt II)
Cn πΎ) β
V |
32 | | fex2 7862 |
. . . . . . 7
β’ (((π β (π½ Cn πΎ), π β (π½ Cn πΎ) β¦ {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))}):((π½ Cn πΎ) Γ (π½ Cn πΎ))βΆπ« ((π½ Γt II) Cn πΎ) β§ ((π½ Cn πΎ) Γ (π½ Cn πΎ)) β V β§ π« ((π½ Γt II) Cn
πΎ) β V) β (π β (π½ Cn πΎ), π β (π½ Cn πΎ) β¦ {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))}) β V) |
33 | 28, 30, 31, 32 | mp3an 1461 |
. . . . . 6
β’ (π β (π½ Cn πΎ), π β (π½ Cn πΎ) β¦ {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))}) β V |
34 | 33 | a1i 11 |
. . . . 5
β’ (π β (π β (π½ Cn πΎ), π β (π½ Cn πΎ) β¦ {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))}) β V) |
35 | 2, 16, 18, 21, 34 | ovmpod 7501 |
. . . 4
β’ (π β (π½ Htpy πΎ) = (π β (π½ Cn πΎ), π β (π½ Cn πΎ) β¦ {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))})) |
36 | | fveq1 6838 |
. . . . . . . . 9
β’ (π = πΉ β (πβπ ) = (πΉβπ )) |
37 | 36 | eqeq2d 2748 |
. . . . . . . 8
β’ (π = πΉ β ((π β0) = (πβπ ) β (π β0) = (πΉβπ ))) |
38 | | fveq1 6838 |
. . . . . . . . 9
β’ (π = πΊ β (πβπ ) = (πΊβπ )) |
39 | 38 | eqeq2d 2748 |
. . . . . . . 8
β’ (π = πΊ β ((π β1) = (πβπ ) β (π β1) = (πΊβπ ))) |
40 | 37, 39 | bi2anan9 637 |
. . . . . . 7
β’ ((π = πΉ β§ π = πΊ) β (((π β0) = (πβπ ) β§ (π β1) = (πβπ )) β ((π β0) = (πΉβπ ) β§ (π β1) = (πΊβπ )))) |
41 | 40 | adantl 482 |
. . . . . 6
β’ ((π β§ (π = πΉ β§ π = πΊ)) β (((π β0) = (πβπ ) β§ (π β1) = (πβπ )) β ((π β0) = (πΉβπ ) β§ (π β1) = (πΊβπ )))) |
42 | 41 | ralbidv 3172 |
. . . . 5
β’ ((π β§ (π = πΉ β§ π = πΊ)) β (βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ )) β βπ β π ((π β0) = (πΉβπ ) β§ (π β1) = (πΊβπ )))) |
43 | 42 | rabbidv 3413 |
. . . 4
β’ ((π β§ (π = πΉ β§ π = πΊ)) β {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πβπ ) β§ (π β1) = (πβπ ))} = {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πΉβπ ) β§ (π β1) = (πΊβπ ))}) |
44 | | ishtpy.4 |
. . . 4
β’ (π β πΊ β (π½ Cn πΎ)) |
45 | 22 | rabex 5287 |
. . . . 5
β’ {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πΉβπ ) β§ (π β1) = (πΊβπ ))} β V |
46 | 45 | a1i 11 |
. . . 4
β’ (π β {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πΉβπ ) β§ (π β1) = (πΊβπ ))} β V) |
47 | 35, 43, 19, 44, 46 | ovmpod 7501 |
. . 3
β’ (π β (πΉ(π½ Htpy πΎ)πΊ) = {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πΉβπ ) β§ (π β1) = (πΊβπ ))}) |
48 | 47 | eleq2d 2823 |
. 2
β’ (π β (π» β (πΉ(π½ Htpy πΎ)πΊ) β π» β {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πΉβπ ) β§ (π β1) = (πΊβπ ))})) |
49 | | oveq 7357 |
. . . . . 6
β’ (β = π» β (π β0) = (π π»0)) |
50 | 49 | eqeq1d 2739 |
. . . . 5
β’ (β = π» β ((π β0) = (πΉβπ ) β (π π»0) = (πΉβπ ))) |
51 | | oveq 7357 |
. . . . . 6
β’ (β = π» β (π β1) = (π π»1)) |
52 | 51 | eqeq1d 2739 |
. . . . 5
β’ (β = π» β ((π β1) = (πΊβπ ) β (π π»1) = (πΊβπ ))) |
53 | 50, 52 | anbi12d 631 |
. . . 4
β’ (β = π» β (((π β0) = (πΉβπ ) β§ (π β1) = (πΊβπ )) β ((π π»0) = (πΉβπ ) β§ (π π»1) = (πΊβπ )))) |
54 | 53 | ralbidv 3172 |
. . 3
β’ (β = π» β (βπ β π ((π β0) = (πΉβπ ) β§ (π β1) = (πΊβπ )) β βπ β π ((π π»0) = (πΉβπ ) β§ (π π»1) = (πΊβπ )))) |
55 | 54 | elrab 3643 |
. 2
β’ (π» β {β β ((π½ Γt II) Cn πΎ) β£ βπ β π ((π β0) = (πΉβπ ) β§ (π β1) = (πΊβπ ))} β (π» β ((π½ Γt II) Cn πΎ) β§ βπ β π ((π π»0) = (πΉβπ ) β§ (π π»1) = (πΊβπ )))) |
56 | 48, 55 | bitrdi 286 |
1
β’ (π β (π» β (πΉ(π½ Htpy πΎ)πΊ) β (π» β ((π½ Γt II) Cn πΎ) β§ βπ β π ((π π»0) = (πΉβπ ) β§ (π π»1) = (πΊβπ ))))) |