Step | Hyp | Ref
| Expression |
1 | | f1stres 7946 |
. . . . . . . . 9
β’
(1st βΎ (βͺ π½ Γ βͺ πΎ)):(βͺ
π½ Γ βͺ πΎ)βΆβͺ π½ |
2 | | ffn 6669 |
. . . . . . . . 9
β’
((1st βΎ (βͺ π½ Γ βͺ πΎ)):(βͺ
π½ Γ βͺ πΎ)βΆβͺ π½ β (1st βΎ
(βͺ π½ Γ βͺ πΎ)) Fn (βͺ π½
Γ βͺ πΎ)) |
3 | 1, 2 | ax-mp 5 |
. . . . . . . 8
β’
(1st βΎ (βͺ π½ Γ βͺ πΎ)) Fn (βͺ π½
Γ βͺ πΎ) |
4 | | fvco2 6939 |
. . . . . . . 8
β’
(((1st βΎ (βͺ π½ Γ βͺ πΎ))
Fn (βͺ π½ Γ βͺ πΎ) β§ π β (βͺ π½ Γ βͺ πΎ))
β ((πΉ β
(1st βΎ (βͺ π½ Γ βͺ πΎ)))βπ) = (πΉβ((1st βΎ (βͺ π½
Γ βͺ πΎ))βπ))) |
5 | 3, 4 | mpan 689 |
. . . . . . 7
β’ (π β (βͺ π½
Γ βͺ πΎ) β ((πΉ β (1st βΎ (βͺ π½
Γ βͺ πΎ)))βπ) = (πΉβ((1st βΎ (βͺ π½
Γ βͺ πΎ))βπ))) |
6 | 5 | adantl 483 |
. . . . . 6
β’ (((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ π β (βͺ π½ Γ βͺ πΎ))
β ((πΉ β
(1st βΎ (βͺ π½ Γ βͺ πΎ)))βπ) = (πΉβ((1st βΎ (βͺ π½
Γ βͺ πΎ))βπ))) |
7 | | fvres 6862 |
. . . . . . . 8
β’ (π β (βͺ π½
Γ βͺ πΎ) β ((1st βΎ (βͺ π½
Γ βͺ πΎ))βπ) = (1st βπ)) |
8 | 7 | fveq2d 6847 |
. . . . . . 7
β’ (π β (βͺ π½
Γ βͺ πΎ) β (πΉβ((1st βΎ (βͺ π½
Γ βͺ πΎ))βπ)) = (πΉβ(1st βπ))) |
9 | 8 | adantl 483 |
. . . . . 6
β’ (((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ π β (βͺ π½ Γ βͺ πΎ))
β (πΉβ((1st βΎ (βͺ π½
Γ βͺ πΎ))βπ)) = (πΉβ(1st βπ))) |
10 | 6, 9 | eqtrd 2773 |
. . . . 5
β’ (((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ π β (βͺ π½ Γ βͺ πΎ))
β ((πΉ β
(1st βΎ (βͺ π½ Γ βͺ πΎ)))βπ) = (πΉβ(1st βπ))) |
11 | | fvres 6862 |
. . . . . 6
β’ (π β (βͺ π½
Γ βͺ πΎ) β ((2nd βΎ (βͺ π½
Γ βͺ πΎ))βπ) = (2nd βπ)) |
12 | 11 | adantl 483 |
. . . . 5
β’ (((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ π β (βͺ π½ Γ βͺ πΎ))
β ((2nd βΎ (βͺ π½ Γ βͺ πΎ))βπ) = (2nd βπ)) |
13 | 10, 12 | eqeq12d 2749 |
. . . 4
β’ (((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ π β (βͺ π½ Γ βͺ πΎ))
β (((πΉ β
(1st βΎ (βͺ π½ Γ βͺ πΎ)))βπ) = ((2nd βΎ (βͺ π½
Γ βͺ πΎ))βπ) β (πΉβ(1st βπ)) = (2nd
βπ))) |
14 | 13 | rabbidva 3413 |
. . 3
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β {π β (βͺ π½ Γ βͺ πΎ)
β£ ((πΉ β
(1st βΎ (βͺ π½ Γ βͺ πΎ)))βπ) = ((2nd βΎ (βͺ π½
Γ βͺ πΎ))βπ)} = {π β (βͺ π½ Γ βͺ πΎ)
β£ (πΉβ(1st βπ)) = (2nd
βπ)}) |
15 | | eqid 2733 |
. . . . . . . 8
β’ βͺ π½ =
βͺ π½ |
16 | | eqid 2733 |
. . . . . . . 8
β’ βͺ πΎ =
βͺ πΎ |
17 | 15, 16 | cnf 22613 |
. . . . . . 7
β’ (πΉ β (π½ Cn πΎ) β πΉ:βͺ π½βΆβͺ πΎ) |
18 | 17 | adantl 483 |
. . . . . 6
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β πΉ:βͺ π½βΆβͺ πΎ) |
19 | | fco 6693 |
. . . . . 6
β’ ((πΉ:βͺ
π½βΆβͺ πΎ
β§ (1st βΎ (βͺ π½ Γ βͺ πΎ)):(βͺ
π½ Γ βͺ πΎ)βΆβͺ π½) β (πΉ β (1st βΎ (βͺ π½
Γ βͺ πΎ))):(βͺ π½ Γ βͺ πΎ)βΆβͺ πΎ) |
20 | 18, 1, 19 | sylancl 587 |
. . . . 5
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β (πΉ β (1st βΎ (βͺ π½
Γ βͺ πΎ))):(βͺ π½ Γ βͺ πΎ)βΆβͺ πΎ) |
21 | 20 | ffnd 6670 |
. . . 4
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β (πΉ β (1st βΎ (βͺ π½
Γ βͺ πΎ))) Fn (βͺ π½ Γ βͺ πΎ)) |
22 | | f2ndres 7947 |
. . . . 5
β’
(2nd βΎ (βͺ π½ Γ βͺ πΎ)):(βͺ
π½ Γ βͺ πΎ)βΆβͺ πΎ |
23 | | ffn 6669 |
. . . . 5
β’
((2nd βΎ (βͺ π½ Γ βͺ πΎ)):(βͺ
π½ Γ βͺ πΎ)βΆβͺ πΎ β (2nd βΎ
(βͺ π½ Γ βͺ πΎ)) Fn (βͺ π½
Γ βͺ πΎ)) |
24 | 22, 23 | ax-mp 5 |
. . . 4
β’
(2nd βΎ (βͺ π½ Γ βͺ πΎ)) Fn (βͺ π½
Γ βͺ πΎ) |
25 | | fndmin 6996 |
. . . 4
β’ (((πΉ β (1st βΎ
(βͺ π½ Γ βͺ πΎ))) Fn (βͺ π½
Γ βͺ πΎ) β§ (2nd βΎ (βͺ π½
Γ βͺ πΎ)) Fn (βͺ π½ Γ βͺ πΎ))
β dom ((πΉ β
(1st βΎ (βͺ π½ Γ βͺ πΎ))) β© (2nd
βΎ (βͺ π½ Γ βͺ πΎ))) = {π β (βͺ π½ Γ βͺ πΎ)
β£ ((πΉ β
(1st βΎ (βͺ π½ Γ βͺ πΎ)))βπ) = ((2nd βΎ (βͺ π½
Γ βͺ πΎ))βπ)}) |
26 | 21, 24, 25 | sylancl 587 |
. . 3
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β dom ((πΉ β (1st βΎ (βͺ π½
Γ βͺ πΎ))) β© (2nd βΎ (βͺ π½
Γ βͺ πΎ))) = {π β (βͺ π½ Γ βͺ πΎ)
β£ ((πΉ β
(1st βΎ (βͺ π½ Γ βͺ πΎ)))βπ) = ((2nd βΎ (βͺ π½
Γ βͺ πΎ))βπ)}) |
27 | | fgraphxp 41581 |
. . . 4
β’ (πΉ:βͺ
π½βΆβͺ πΎ
β πΉ = {π β (βͺ π½
Γ βͺ πΎ) β£ (πΉβ(1st βπ)) = (2nd
βπ)}) |
28 | 18, 27 | syl 17 |
. . 3
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β πΉ = {π β (βͺ π½ Γ βͺ πΎ)
β£ (πΉβ(1st βπ)) = (2nd
βπ)}) |
29 | 14, 26, 28 | 3eqtr4rd 2784 |
. 2
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β πΉ = dom ((πΉ β (1st βΎ (βͺ π½
Γ βͺ πΎ))) β© (2nd βΎ (βͺ π½
Γ βͺ πΎ)))) |
30 | | simpl 484 |
. . 3
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β πΎ β Haus) |
31 | | cntop1 22607 |
. . . . . . 7
β’ (πΉ β (π½ Cn πΎ) β π½ β Top) |
32 | 31 | adantl 483 |
. . . . . 6
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β π½ β Top) |
33 | 15 | toptopon 22282 |
. . . . . 6
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
34 | 32, 33 | sylib 217 |
. . . . 5
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β π½ β (TopOnββͺ π½)) |
35 | | haustop 22698 |
. . . . . . 7
β’ (πΎ β Haus β πΎ β Top) |
36 | 30, 35 | syl 17 |
. . . . . 6
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β πΎ β Top) |
37 | 16 | toptopon 22282 |
. . . . . 6
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
38 | 36, 37 | sylib 217 |
. . . . 5
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β πΎ β (TopOnββͺ πΎ)) |
39 | | tx1cn 22976 |
. . . . 5
β’ ((π½ β (TopOnββͺ π½)
β§ πΎ β
(TopOnββͺ πΎ)) β (1st βΎ (βͺ π½
Γ βͺ πΎ)) β ((π½ Γt πΎ) Cn π½)) |
40 | 34, 38, 39 | syl2anc 585 |
. . . 4
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β (1st βΎ (βͺ π½
Γ βͺ πΎ)) β ((π½ Γt πΎ) Cn π½)) |
41 | | cnco 22633 |
. . . 4
β’
(((1st βΎ (βͺ π½ Γ βͺ πΎ))
β ((π½
Γt πΎ) Cn
π½) β§ πΉ β (π½ Cn πΎ)) β (πΉ β (1st βΎ (βͺ π½
Γ βͺ πΎ))) β ((π½ Γt πΎ) Cn πΎ)) |
42 | 40, 41 | sylancom 589 |
. . 3
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β (πΉ β (1st βΎ (βͺ π½
Γ βͺ πΎ))) β ((π½ Γt πΎ) Cn πΎ)) |
43 | | tx2cn 22977 |
. . . 4
β’ ((π½ β (TopOnββͺ π½)
β§ πΎ β
(TopOnββͺ πΎ)) β (2nd βΎ (βͺ π½
Γ βͺ πΎ)) β ((π½ Γt πΎ) Cn πΎ)) |
44 | 34, 38, 43 | syl2anc 585 |
. . 3
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β (2nd βΎ (βͺ π½
Γ βͺ πΎ)) β ((π½ Γt πΎ) Cn πΎ)) |
45 | 30, 42, 44 | hauseqlcld 23013 |
. 2
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β dom ((πΉ β (1st βΎ (βͺ π½
Γ βͺ πΎ))) β© (2nd βΎ (βͺ π½
Γ βͺ πΎ))) β (Clsdβ(π½ Γt πΎ))) |
46 | 29, 45 | eqeltrd 2834 |
1
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β πΉ β (Clsdβ(π½ Γt πΎ))) |