Step | Hyp | Ref
| Expression |
1 | | qtophaus.1 |
. . . 4
β’ (π β π½ β Haus) |
2 | | haustop 22698 |
. . . 4
β’ (π½ β Haus β π½ β Top) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β π½ β Top) |
4 | | qtophaus.2 |
. . . 4
β’ (π β πΉ:πβontoβπ) |
5 | | fofn 6759 |
. . . 4
β’ (πΉ:πβontoβπ β πΉ Fn π) |
6 | 4, 5 | syl 17 |
. . 3
β’ (π β πΉ Fn π) |
7 | | qtophaus.x |
. . . 4
β’ π = βͺ
π½ |
8 | 7 | qtoptop 23067 |
. . 3
β’ ((π½ β Top β§ πΉ Fn π) β (π½ qTop πΉ) β Top) |
9 | 3, 6, 8 | syl2anc 585 |
. 2
β’ (π β (π½ qTop πΉ) β Top) |
10 | | txtop 22936 |
. . . 4
β’ (((π½ qTop πΉ) β Top β§ (π½ qTop πΉ) β Top) β ((π½ qTop πΉ) Γt (π½ qTop πΉ)) β Top) |
11 | 9, 9, 10 | syl2anc 585 |
. . 3
β’ (π β ((π½ qTop πΉ) Γt (π½ qTop πΉ)) β Top) |
12 | | idssxp 6003 |
. . . 4
β’ ( I
βΎ βͺ (π½ qTop πΉ)) β (βͺ
(π½ qTop πΉ) Γ βͺ
(π½ qTop πΉ)) |
13 | | eqid 2733 |
. . . . . 6
β’ βͺ (π½
qTop πΉ) = βͺ (π½
qTop πΉ) |
14 | 13, 13 | txuni 22959 |
. . . . 5
β’ (((π½ qTop πΉ) β Top β§ (π½ qTop πΉ) β Top) β (βͺ (π½
qTop πΉ) Γ βͺ (π½
qTop πΉ)) = βͺ ((π½
qTop πΉ) Γt
(π½ qTop πΉ))) |
15 | 9, 9, 14 | syl2anc 585 |
. . . 4
β’ (π β (βͺ (π½
qTop πΉ) Γ βͺ (π½
qTop πΉ)) = βͺ ((π½
qTop πΉ) Γt
(π½ qTop πΉ))) |
16 | 12, 15 | sseqtrid 3997 |
. . 3
β’ (π β ( I βΎ βͺ (π½
qTop πΉ)) β βͺ ((π½
qTop πΉ) Γt
(π½ qTop πΉ))) |
17 | 7 | qtopuni 23069 |
. . . . . . . 8
β’ ((π½ β Top β§ πΉ:πβontoβπ) β π = βͺ (π½ qTop πΉ)) |
18 | 3, 4, 17 | syl2anc 585 |
. . . . . . 7
β’ (π β π = βͺ (π½ qTop πΉ)) |
19 | 18 | sqxpeqd 5666 |
. . . . . 6
β’ (π β (π Γ π) = (βͺ (π½ qTop πΉ) Γ βͺ
(π½ qTop πΉ))) |
20 | 19, 15 | eqtr2d 2774 |
. . . . 5
β’ (π β βͺ ((π½
qTop πΉ) Γt
(π½ qTop πΉ)) = (π Γ π)) |
21 | 18 | eqcomd 2739 |
. . . . . 6
β’ (π β βͺ (π½
qTop πΉ) = π) |
22 | 21 | reseq2d 5938 |
. . . . 5
β’ (π β ( I βΎ βͺ (π½
qTop πΉ)) = ( I βΎ
π)) |
23 | 20, 22 | difeq12d 4084 |
. . . 4
β’ (π β (βͺ ((π½
qTop πΉ) Γt
(π½ qTop πΉ)) β ( I βΎ βͺ (π½
qTop πΉ))) = ((π Γ π) β ( I βΎ π))) |
24 | | qtophaus.h |
. . . . . . . . . 10
β’ π» = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) |
25 | | opex 5422 |
. . . . . . . . . 10
β’
β¨(πΉβπ₯), (πΉβπ¦)β© β V |
26 | 24, 25 | fnmpoi 8003 |
. . . . . . . . 9
β’ π» Fn (π Γ π) |
27 | | difss 4092 |
. . . . . . . . 9
β’ ((π Γ π) β βΌ ) β (π Γ π) |
28 | | fvelimab 6915 |
. . . . . . . . 9
β’ ((π» Fn (π Γ π) β§ ((π Γ π) β βΌ ) β (π Γ π)) β (π β (π» β ((π Γ π) β βΌ )) β
βπ§ β ((π Γ π) β βΌ )(π»βπ§) = π)) |
29 | 26, 27, 28 | mp2an 691 |
. . . . . . . 8
β’ (π β (π» β ((π Γ π) β βΌ )) β
βπ§ β ((π Γ π) β βΌ )(π»βπ§) = π) |
30 | | simp-4r 783 |
. . . . . . . . . . . . . . . 16
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β π₯ β π) |
31 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β π¦ β π) |
32 | | opelxpi 5671 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β π β§ π¦ β π) β β¨π₯, π¦β© β (π Γ π)) |
33 | 30, 31, 32 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β β¨π₯, π¦β© β (π Γ π)) |
34 | | df-br 5107 |
. . . . . . . . . . . . . . 15
β’ (π₯(π Γ π)π¦ β β¨π₯, π¦β© β (π Γ π)) |
35 | 33, 34 | sylibr 233 |
. . . . . . . . . . . . . 14
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β π₯(π Γ π)π¦) |
36 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β (πΉβπ₯) = π) |
37 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β (πΉβπ¦) = π) |
38 | 36, 37 | opeq12d 4839 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β β¨(πΉβπ₯), (πΉβπ¦)β© = β¨π, πβ©) |
39 | | simp-5r 785 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β π = β¨π, πβ©) |
40 | | simp-8r 791 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β π β ((π Γ π) β I )) |
41 | 39, 40 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β β¨π, πβ© β ((π Γ π) β I )) |
42 | 38, 41 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . 17
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β β¨(πΉβπ₯), (πΉβπ¦)β© β ((π Γ π) β I )) |
43 | | relxp 5652 |
. . . . . . . . . . . . . . . . . 18
β’ Rel
(π Γ π) |
44 | | opeldifid 31563 |
. . . . . . . . . . . . . . . . . 18
β’ (Rel
(π Γ π) β (β¨(πΉβπ₯), (πΉβπ¦)β© β ((π Γ π) β I ) β (β¨(πΉβπ₯), (πΉβπ¦)β© β (π Γ π) β§ (πΉβπ₯) β (πΉβπ¦)))) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’
(β¨(πΉβπ₯), (πΉβπ¦)β© β ((π Γ π) β I ) β (β¨(πΉβπ₯), (πΉβπ¦)β© β (π Γ π) β§ (πΉβπ₯) β (πΉβπ¦))) |
46 | 42, 45 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β (β¨(πΉβπ₯), (πΉβπ¦)β© β (π Γ π) β§ (πΉβπ₯) β (πΉβπ¦))) |
47 | 46 | simprd 497 |
. . . . . . . . . . . . . . 15
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β (πΉβπ₯) β (πΉβπ¦)) |
48 | 6 | ad8antr 739 |
. . . . . . . . . . . . . . . . 17
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β πΉ Fn π) |
49 | | qtophaus.e |
. . . . . . . . . . . . . . . . . 18
β’ βΌ =
(β‘πΉ β πΉ) |
50 | 49 | fcoinvbr 31572 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ Fn π β§ π₯ β π β§ π¦ β π) β (π₯ βΌ π¦ β (πΉβπ₯) = (πΉβπ¦))) |
51 | 48, 30, 31, 50 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β (π₯ βΌ π¦ β (πΉβπ₯) = (πΉβπ¦))) |
52 | 51 | necon3bbid 2978 |
. . . . . . . . . . . . . . 15
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β (Β¬ π₯ βΌ π¦ β (πΉβπ₯) β (πΉβπ¦))) |
53 | 47, 52 | mpbird 257 |
. . . . . . . . . . . . . 14
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β Β¬ π₯ βΌ π¦) |
54 | | df-br 5107 |
. . . . . . . . . . . . . . 15
β’ (π₯((π Γ π) β βΌ )π¦ β β¨π₯, π¦β© β ((π Γ π) β βΌ )) |
55 | | brdif 5159 |
. . . . . . . . . . . . . . 15
β’ (π₯((π Γ π) β βΌ )π¦ β (π₯(π Γ π)π¦ β§ Β¬ π₯ βΌ π¦)) |
56 | 54, 55 | bitr3i 277 |
. . . . . . . . . . . . . 14
β’
(β¨π₯, π¦β© β ((π Γ π) β βΌ ) β (π₯(π Γ π)π¦ β§ Β¬ π₯ βΌ π¦)) |
57 | 35, 53, 56 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β β¨π₯, π¦β© β ((π Γ π) β βΌ )) |
58 | 24, 30, 31 | fvproj 8067 |
. . . . . . . . . . . . . 14
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β (π»ββ¨π₯, π¦β©) = β¨(πΉβπ₯), (πΉβπ¦)β©) |
59 | 38, 58, 39 | 3eqtr4d 2783 |
. . . . . . . . . . . . 13
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β (π»ββ¨π₯, π¦β©) = π) |
60 | | fveqeq2 6852 |
. . . . . . . . . . . . . 14
β’ (π§ = β¨π₯, π¦β© β ((π»βπ§) = π β (π»ββ¨π₯, π¦β©) = π)) |
61 | 60 | rspcev 3580 |
. . . . . . . . . . . . 13
β’
((β¨π₯, π¦β© β ((π Γ π) β βΌ ) β§ (π»ββ¨π₯, π¦β©) = π) β βπ§ β ((π Γ π) β βΌ )(π»βπ§) = π) |
62 | 57, 59, 61 | syl2anc 585 |
. . . . . . . . . . . 12
β’
(((((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β§ π¦ β π) β§ (πΉβπ¦) = π) β βπ§ β ((π Γ π) β βΌ )(π»βπ§) = π) |
63 | | fofun 6758 |
. . . . . . . . . . . . . . . 16
β’ (πΉ:πβontoβπ β Fun πΉ) |
64 | 4, 63 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β Fun πΉ) |
65 | 64 | ad4antr 731 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β Fun πΉ) |
66 | 65 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β Fun πΉ) |
67 | | simp-4r 783 |
. . . . . . . . . . . . . 14
β’
(((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β π β π) |
68 | | foima 6762 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ:πβontoβπ β (πΉ β π) = π) |
69 | 4, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΉ β π) = π) |
70 | 69 | ad4antr 731 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β (πΉ β π) = π) |
71 | 70 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β (πΉ β π) = π) |
72 | 67, 71 | eleqtrrd 2837 |
. . . . . . . . . . . . 13
β’
(((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β π β (πΉ β π)) |
73 | | fvelima 6909 |
. . . . . . . . . . . . 13
β’ ((Fun
πΉ β§ π β (πΉ β π)) β βπ¦ β π (πΉβπ¦) = π) |
74 | 66, 72, 73 | syl2anc 585 |
. . . . . . . . . . . 12
β’
(((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β βπ¦ β π (πΉβπ¦) = π) |
75 | 62, 74 | r19.29a 3156 |
. . . . . . . . . . 11
β’
(((((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β§ π₯ β π) β§ (πΉβπ₯) = π) β βπ§ β ((π Γ π) β βΌ )(π»βπ§) = π) |
76 | | simpllr 775 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β π β π) |
77 | 76, 70 | eleqtrrd 2837 |
. . . . . . . . . . . 12
β’
(((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β π β (πΉ β π)) |
78 | | fvelima 6909 |
. . . . . . . . . . . 12
β’ ((Fun
πΉ β§ π β (πΉ β π)) β βπ₯ β π (πΉβπ₯) = π) |
79 | 65, 77, 78 | syl2anc 585 |
. . . . . . . . . . 11
β’
(((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β βπ₯ β π (πΉβπ₯) = π) |
80 | 75, 79 | r19.29a 3156 |
. . . . . . . . . 10
β’
(((((π β§ π β ((π Γ π) β I )) β§ π β π) β§ π β π) β§ π = β¨π, πβ©) β βπ§ β ((π Γ π) β βΌ )(π»βπ§) = π) |
81 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((π Γ π) β I )) β π β ((π Γ π) β I )) |
82 | 81 | eldifad 3923 |
. . . . . . . . . . 11
β’ ((π β§ π β ((π Γ π) β I )) β π β (π Γ π)) |
83 | | elxp2 5658 |
. . . . . . . . . . 11
β’ (π β (π Γ π) β βπ β π βπ β π π = β¨π, πβ©) |
84 | 82, 83 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π β ((π Γ π) β I )) β βπ β π βπ β π π = β¨π, πβ©) |
85 | 80, 84 | r19.29vva 3204 |
. . . . . . . . 9
β’ ((π β§ π β ((π Γ π) β I )) β βπ§ β ((π Γ π) β βΌ )(π»βπ§) = π) |
86 | | simpr 486 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β π§ = β¨π₯, π¦β©) |
87 | 86 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β (π»βπ§) = (π»ββ¨π₯, π¦β©)) |
88 | | simp-4r 783 |
. . . . . . . . . . . . 13
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β (π»βπ§) = π) |
89 | | simpllr 775 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β π₯ β π) |
90 | | simplr 768 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β π¦ β π) |
91 | 24, 89, 90 | fvproj 8067 |
. . . . . . . . . . . . 13
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β (π»ββ¨π₯, π¦β©) = β¨(πΉβπ₯), (πΉβπ¦)β©) |
92 | 87, 88, 91 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β π = β¨(πΉβπ₯), (πΉβπ¦)β©) |
93 | | fof 6757 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ:πβontoβπ β πΉ:πβΆπ) |
94 | 4, 93 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ:πβΆπ) |
95 | 94 | ad5antr 733 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β πΉ:πβΆπ) |
96 | 95, 89 | ffvelcdmd 7037 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β (πΉβπ₯) β π) |
97 | 95, 90 | ffvelcdmd 7037 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β (πΉβπ¦) β π) |
98 | | opelxp 5670 |
. . . . . . . . . . . . . 14
β’
(β¨(πΉβπ₯), (πΉβπ¦)β© β (π Γ π) β ((πΉβπ₯) β π β§ (πΉβπ¦) β π)) |
99 | 96, 97, 98 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β β¨(πΉβπ₯), (πΉβπ¦)β© β (π Γ π)) |
100 | | simp-5r 785 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β π§ β ((π Γ π) β βΌ )) |
101 | 86, 100 | eqeltrrd 2835 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β β¨π₯, π¦β© β ((π Γ π) β βΌ )) |
102 | 56 | simprbi 498 |
. . . . . . . . . . . . . . 15
β’
(β¨π₯, π¦β© β ((π Γ π) β βΌ ) β Β¬
π₯ βΌ π¦) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β Β¬ π₯ βΌ π¦) |
104 | 6 | ad5antr 733 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β πΉ Fn π) |
105 | 104, 89, 90, 50 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β (π₯ βΌ π¦ β (πΉβπ₯) = (πΉβπ¦))) |
106 | 105 | necon3bbid 2978 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β (Β¬ π₯ βΌ π¦ β (πΉβπ₯) β (πΉβπ¦))) |
107 | 103, 106 | mpbid 231 |
. . . . . . . . . . . . 13
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β (πΉβπ₯) β (πΉβπ¦)) |
108 | 99, 107, 45 | sylanbrc 584 |
. . . . . . . . . . . 12
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β β¨(πΉβπ₯), (πΉβπ¦)β© β ((π Γ π) β I )) |
109 | 92, 108 | eqeltrd 2834 |
. . . . . . . . . . 11
β’
((((((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β§ π₯ β π) β§ π¦ β π) β§ π§ = β¨π₯, π¦β©) β π β ((π Γ π) β I )) |
110 | | eldifi 4087 |
. . . . . . . . . . . . . 14
β’ (π§ β ((π Γ π) β βΌ ) β π§ β (π Γ π)) |
111 | 110 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β ((π Γ π) β βΌ )) β π§ β (π Γ π)) |
112 | | elxp2 5658 |
. . . . . . . . . . . . 13
β’ (π§ β (π Γ π) β βπ₯ β π βπ¦ β π π§ = β¨π₯, π¦β©) |
113 | 111, 112 | sylib 217 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β ((π Γ π) β βΌ )) β
βπ₯ β π βπ¦ β π π§ = β¨π₯, π¦β©) |
114 | 113 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β βπ₯ β π βπ¦ β π π§ = β¨π₯, π¦β©) |
115 | 109, 114 | r19.29vva 3204 |
. . . . . . . . . 10
β’ (((π β§ π§ β ((π Γ π) β βΌ )) β§ (π»βπ§) = π) β π β ((π Γ π) β I )) |
116 | 115 | r19.29an 3152 |
. . . . . . . . 9
β’ ((π β§ βπ§ β ((π Γ π) β βΌ )(π»βπ§) = π) β π β ((π Γ π) β I )) |
117 | 85, 116 | impbida 800 |
. . . . . . . 8
β’ (π β (π β ((π Γ π) β I ) β βπ§ β ((π Γ π) β βΌ )(π»βπ§) = π)) |
118 | 29, 117 | bitr4id 290 |
. . . . . . 7
β’ (π β (π β (π» β ((π Γ π) β βΌ )) β π β ((π Γ π) β I ))) |
119 | 118 | eqrdv 2731 |
. . . . . 6
β’ (π β (π» β ((π Γ π) β βΌ )) = ((π Γ π) β I )) |
120 | | ssv 3969 |
. . . . . . 7
β’ π β V |
121 | | xpss2 5654 |
. . . . . . 7
β’ (π β V β (π Γ π) β (π Γ V)) |
122 | | difres 31564 |
. . . . . . 7
β’ ((π Γ π) β (π Γ V) β ((π Γ π) β ( I βΎ π)) = ((π Γ π) β I )) |
123 | 120, 121,
122 | mp2b 10 |
. . . . . 6
β’ ((π Γ π) β ( I βΎ π)) = ((π Γ π) β I ) |
124 | 119, 123 | eqtr4di 2791 |
. . . . 5
β’ (π β (π» β ((π Γ π) β βΌ )) = ((π Γ π) β ( I βΎ π))) |
125 | 7 | toptopon 22282 |
. . . . . . 7
β’ (π½ β Top β π½ β (TopOnβπ)) |
126 | 3, 125 | sylib 217 |
. . . . . 6
β’ (π β π½ β (TopOnβπ)) |
127 | | qtoptopon 23071 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π½ qTop πΉ) β (TopOnβπ)) |
128 | 126, 4, 127 | syl2anc 585 |
. . . . . 6
β’ (π β (π½ qTop πΉ) β (TopOnβπ)) |
129 | | qtophaus.3 |
. . . . . 6
β’ ((π β§ π₯ β π½) β (πΉ β π₯) β (π½ qTop πΉ)) |
130 | 129 | ralrimiva 3140 |
. . . . . . . 8
β’ (π β βπ₯ β π½ (πΉ β π₯) β (π½ qTop πΉ)) |
131 | | imaeq2 6010 |
. . . . . . . . . 10
β’ (π₯ = π¦ β (πΉ β π₯) = (πΉ β π¦)) |
132 | 131 | eleq1d 2819 |
. . . . . . . . 9
β’ (π₯ = π¦ β ((πΉ β π₯) β (π½ qTop πΉ) β (πΉ β π¦) β (π½ qTop πΉ))) |
133 | 132 | cbvralvw 3224 |
. . . . . . . 8
β’
(βπ₯ β
π½ (πΉ β π₯) β (π½ qTop πΉ) β βπ¦ β π½ (πΉ β π¦) β (π½ qTop πΉ)) |
134 | 130, 133 | sylib 217 |
. . . . . . 7
β’ (π β βπ¦ β π½ (πΉ β π¦) β (π½ qTop πΉ)) |
135 | 134 | r19.21bi 3233 |
. . . . . 6
β’ ((π β§ π¦ β π½) β (πΉ β π¦) β (π½ qTop πΉ)) |
136 | 7, 7 | txuni 22959 |
. . . . . . . . 9
β’ ((π½ β Top β§ π½ β Top) β (π Γ π) = βͺ (π½ Γt π½)) |
137 | 3, 3, 136 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π Γ π) = βͺ (π½ Γt π½)) |
138 | 137 | difeq1d 4082 |
. . . . . . 7
β’ (π β ((π Γ π) β βΌ ) = (βͺ (π½
Γt π½)
β βΌ )) |
139 | | qtophaus.4 |
. . . . . . . 8
β’ (π β βΌ β
(Clsdβ(π½
Γt π½))) |
140 | | txtop 22936 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π½ β Top) β (π½ Γt π½) β Top) |
141 | 3, 3, 140 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π½ Γt π½) β Top) |
142 | | fcoinver 31571 |
. . . . . . . . . . . . 13
β’ (πΉ Fn π β (β‘πΉ β πΉ) Er π) |
143 | 6, 142 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (β‘πΉ β πΉ) Er π) |
144 | | ereq1 8658 |
. . . . . . . . . . . . 13
β’ ( βΌ =
(β‘πΉ β πΉ) β ( βΌ Er π β (β‘πΉ β πΉ) Er π)) |
145 | 49, 144 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ( βΌ Er
π β (β‘πΉ β πΉ) Er π) |
146 | 143, 145 | sylibr 233 |
. . . . . . . . . . 11
β’ (π β βΌ Er π) |
147 | | erssxp 8674 |
. . . . . . . . . . 11
β’ ( βΌ Er
π β βΌ β (π Γ π)) |
148 | 146, 147 | syl 17 |
. . . . . . . . . 10
β’ (π β βΌ β (π Γ π)) |
149 | 148, 137 | sseqtrd 3985 |
. . . . . . . . 9
β’ (π β βΌ β βͺ (π½
Γt π½)) |
150 | | eqid 2733 |
. . . . . . . . . 10
β’ βͺ (π½
Γt π½) =
βͺ (π½ Γt π½) |
151 | 150 | iscld2 22395 |
. . . . . . . . 9
β’ (((π½ Γt π½) β Top β§ βΌ
β βͺ (π½ Γt π½)) β ( βΌ β
(Clsdβ(π½
Γt π½))
β (βͺ (π½ Γt π½) β βΌ ) β (π½ Γt π½))) |
152 | 141, 149,
151 | syl2anc 585 |
. . . . . . . 8
β’ (π β ( βΌ β
(Clsdβ(π½
Γt π½))
β (βͺ (π½ Γt π½) β βΌ ) β (π½ Γt π½))) |
153 | 139, 152 | mpbid 231 |
. . . . . . 7
β’ (π β (βͺ (π½
Γt π½)
β βΌ ) β (π½ Γt π½)) |
154 | 138, 153 | eqeltrd 2834 |
. . . . . 6
β’ (π β ((π Γ π) β βΌ ) β (π½ Γt π½)) |
155 | 94, 94, 126, 126, 128, 128, 129, 135, 154, 24 | txomap 32472 |
. . . . 5
β’ (π β (π» β ((π Γ π) β βΌ )) β ((π½ qTop πΉ) Γt (π½ qTop πΉ))) |
156 | 124, 155 | eqeltrrd 2835 |
. . . 4
β’ (π β ((π Γ π) β ( I βΎ π)) β ((π½ qTop πΉ) Γt (π½ qTop πΉ))) |
157 | 23, 156 | eqeltrd 2834 |
. . 3
β’ (π β (βͺ ((π½
qTop πΉ) Γt
(π½ qTop πΉ)) β ( I βΎ βͺ (π½
qTop πΉ))) β ((π½ qTop πΉ) Γt (π½ qTop πΉ))) |
158 | | eqid 2733 |
. . . . 5
β’ βͺ ((π½
qTop πΉ) Γt
(π½ qTop πΉ)) = βͺ ((π½ qTop πΉ) Γt (π½ qTop πΉ)) |
159 | 158 | iscld2 22395 |
. . . 4
β’ ((((π½ qTop πΉ) Γt (π½ qTop πΉ)) β Top β§ ( I βΎ βͺ (π½
qTop πΉ)) β βͺ ((π½
qTop πΉ) Γt
(π½ qTop πΉ))) β (( I βΎ βͺ (π½
qTop πΉ)) β
(Clsdβ((π½ qTop πΉ) Γt (π½ qTop πΉ))) β (βͺ
((π½ qTop πΉ) Γt (π½ qTop πΉ)) β ( I βΎ βͺ (π½
qTop πΉ))) β ((π½ qTop πΉ) Γt (π½ qTop πΉ)))) |
160 | 159 | biimpar 479 |
. . 3
β’
(((((π½ qTop πΉ) Γt (π½ qTop πΉ)) β Top β§ ( I βΎ βͺ (π½
qTop πΉ)) β βͺ ((π½
qTop πΉ) Γt
(π½ qTop πΉ))) β§ (βͺ
((π½ qTop πΉ) Γt (π½ qTop πΉ)) β ( I βΎ βͺ (π½
qTop πΉ))) β ((π½ qTop πΉ) Γt (π½ qTop πΉ))) β ( I βΎ βͺ (π½
qTop πΉ)) β
(Clsdβ((π½ qTop πΉ) Γt (π½ qTop πΉ)))) |
161 | 11, 16, 157, 160 | syl21anc 837 |
. 2
β’ (π β ( I βΎ βͺ (π½
qTop πΉ)) β
(Clsdβ((π½ qTop πΉ) Γt (π½ qTop πΉ)))) |
162 | 13 | hausdiag 23012 |
. 2
β’ ((π½ qTop πΉ) β Haus β ((π½ qTop πΉ) β Top β§ ( I βΎ βͺ (π½
qTop πΉ)) β
(Clsdβ((π½ qTop πΉ) Γt (π½ qTop πΉ))))) |
163 | 9, 161, 162 | sylanbrc 584 |
1
β’ (π β (π½ qTop πΉ) β Haus) |