Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
β’ βͺ π½ =
βͺ π½ |
2 | 1 | qtopres 23065 |
. . 3
β’ (πΉ β π β (π½ qTop πΉ) = (π½ qTop (πΉ βΎ βͺ π½))) |
3 | 2 | 3ad2ant2 1135 |
. 2
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (π½ qTop πΉ) = (π½ qTop (πΉ βΎ βͺ π½))) |
4 | | simp1 1137 |
. . . . . . . . . . . . 13
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β π½ β Top) |
5 | | funres 6548 |
. . . . . . . . . . . . . . 15
β’ (Fun
πΉ β Fun (πΉ βΎ βͺ π½)) |
6 | 5 | 3ad2ant3 1136 |
. . . . . . . . . . . . . 14
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β Fun (πΉ βΎ βͺ π½)) |
7 | | funforn 6768 |
. . . . . . . . . . . . . 14
β’ (Fun
(πΉ βΎ βͺ π½)
β (πΉ βΎ βͺ π½):dom (πΉ βΎ βͺ π½)βontoβran (πΉ βΎ βͺ π½)) |
8 | 6, 7 | sylib 217 |
. . . . . . . . . . . . 13
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (πΉ βΎ βͺ π½):dom (πΉ βΎ βͺ π½)βontoβran (πΉ βΎ βͺ π½)) |
9 | | dmres 5964 |
. . . . . . . . . . . . . . 15
β’ dom
(πΉ βΎ βͺ π½) =
(βͺ π½ β© dom πΉ) |
10 | | inss1 4193 |
. . . . . . . . . . . . . . 15
β’ (βͺ π½
β© dom πΉ) β βͺ π½ |
11 | 9, 10 | eqsstri 3983 |
. . . . . . . . . . . . . 14
β’ dom
(πΉ βΎ βͺ π½)
β βͺ π½ |
12 | 11 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β dom (πΉ βΎ βͺ π½) β βͺ π½) |
13 | 1 | elqtop 23064 |
. . . . . . . . . . . . 13
β’ ((π½ β Top β§ (πΉ βΎ βͺ π½):dom (πΉ βΎ βͺ π½)βontoβran (πΉ βΎ βͺ π½) β§ dom (πΉ βΎ βͺ π½) β βͺ π½)
β (π¦ β (π½ qTop (πΉ βΎ βͺ π½)) β (π¦ β ran (πΉ βΎ βͺ π½) β§ (β‘(πΉ βΎ βͺ π½) β π¦) β π½))) |
14 | 4, 8, 12, 13 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (π¦ β (π½ qTop (πΉ βΎ βͺ π½)) β (π¦ β ran (πΉ βΎ βͺ π½) β§ (β‘(πΉ βΎ βͺ π½) β π¦) β π½))) |
15 | 14 | simprbda 500 |
. . . . . . . . . . 11
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ π¦ β (π½ qTop (πΉ βΎ βͺ π½))) β π¦ β ran (πΉ βΎ βͺ π½)) |
16 | | velpw 4570 |
. . . . . . . . . . 11
β’ (π¦ β π« ran (πΉ βΎ βͺ π½)
β π¦ β ran (πΉ βΎ βͺ π½)) |
17 | 15, 16 | sylibr 233 |
. . . . . . . . . 10
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ π¦ β (π½ qTop (πΉ βΎ βͺ π½))) β π¦ β π« ran (πΉ βΎ βͺ π½)) |
18 | 17 | ex 414 |
. . . . . . . . 9
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (π¦ β (π½ qTop (πΉ βΎ βͺ π½)) β π¦ β π« ran (πΉ βΎ βͺ π½))) |
19 | 18 | ssrdv 3955 |
. . . . . . . 8
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (π½ qTop (πΉ βΎ βͺ π½)) β π« ran (πΉ βΎ βͺ π½)) |
20 | | sstr2 3956 |
. . . . . . . 8
β’ (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β ((π½ qTop (πΉ βΎ βͺ π½)) β π« ran (πΉ βΎ βͺ π½)
β π₯ β π«
ran (πΉ βΎ βͺ π½))) |
21 | 19, 20 | syl5com 31 |
. . . . . . 7
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β π₯ β π« ran (πΉ βΎ βͺ π½))) |
22 | | sspwuni 5065 |
. . . . . . 7
β’ (π₯ β π« ran (πΉ βΎ βͺ π½)
β βͺ π₯ β ran (πΉ βΎ βͺ π½)) |
23 | 21, 22 | syl6ib 251 |
. . . . . 6
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β βͺ π₯
β ran (πΉ βΎ
βͺ π½))) |
24 | | imauni 7198 |
. . . . . . . 8
β’ (β‘(πΉ βΎ βͺ π½) β βͺ π₯) =
βͺ π¦ β π₯ (β‘(πΉ βΎ βͺ π½) β π¦) |
25 | 14 | simplbda 501 |
. . . . . . . . . . 11
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ π¦ β (π½ qTop (πΉ βΎ βͺ π½))) β (β‘(πΉ βΎ βͺ π½) β π¦) β π½) |
26 | 25 | ralrimiva 3144 |
. . . . . . . . . 10
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β βπ¦ β (π½ qTop (πΉ βΎ βͺ π½))(β‘(πΉ βΎ βͺ π½) β π¦) β π½) |
27 | | ssralv 4015 |
. . . . . . . . . 10
β’ (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β (βπ¦ β (π½ qTop (πΉ βΎ βͺ π½))(β‘(πΉ βΎ βͺ π½) β π¦) β π½ β βπ¦ β π₯ (β‘(πΉ βΎ βͺ π½) β π¦) β π½)) |
28 | 26, 27 | mpan9 508 |
. . . . . . . . 9
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ π₯ β (π½ qTop (πΉ βΎ βͺ π½))) β βπ¦ β π₯ (β‘(πΉ βΎ βͺ π½) β π¦) β π½) |
29 | | iunopn 22263 |
. . . . . . . . 9
β’ ((π½ β Top β§ βπ¦ β π₯ (β‘(πΉ βΎ βͺ π½) β π¦) β π½) β βͺ
π¦ β π₯ (β‘(πΉ βΎ βͺ π½) β π¦) β π½) |
30 | 4, 28, 29 | syl2an2r 684 |
. . . . . . . 8
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ π₯ β (π½ qTop (πΉ βΎ βͺ π½))) β βͺ π¦ β π₯ (β‘(πΉ βΎ βͺ π½) β π¦) β π½) |
31 | 24, 30 | eqeltrid 2842 |
. . . . . . 7
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ π₯ β (π½ qTop (πΉ βΎ βͺ π½))) β (β‘(πΉ βΎ βͺ π½) β βͺ π₯)
β π½) |
32 | 31 | ex 414 |
. . . . . 6
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β (β‘(πΉ βΎ βͺ π½) β βͺ π₯)
β π½)) |
33 | 23, 32 | jcad 514 |
. . . . 5
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β (βͺ π₯
β ran (πΉ βΎ
βͺ π½) β§ (β‘(πΉ βΎ βͺ π½) β βͺ π₯)
β π½))) |
34 | 1 | elqtop 23064 |
. . . . . 6
β’ ((π½ β Top β§ (πΉ βΎ βͺ π½):dom (πΉ βΎ βͺ π½)βontoβran (πΉ βΎ βͺ π½) β§ dom (πΉ βΎ βͺ π½) β βͺ π½)
β (βͺ π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β (βͺ π₯
β ran (πΉ βΎ
βͺ π½) β§ (β‘(πΉ βΎ βͺ π½) β βͺ π₯)
β π½))) |
35 | 4, 8, 12, 34 | syl3anc 1372 |
. . . . 5
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (βͺ π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β (βͺ π₯
β ran (πΉ βΎ
βͺ π½) β§ (β‘(πΉ βΎ βͺ π½) β βͺ π₯)
β π½))) |
36 | 33, 35 | sylibrd 259 |
. . . 4
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β βͺ π₯
β (π½ qTop (πΉ βΎ βͺ π½)))) |
37 | 36 | alrimiv 1931 |
. . 3
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β βπ₯(π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β βͺ π₯
β (π½ qTop (πΉ βΎ βͺ π½)))) |
38 | | inss1 4193 |
. . . . . 6
β’ (π₯ β© π¦) β π₯ |
39 | 1 | elqtop 23064 |
. . . . . . . . . 10
β’ ((π½ β Top β§ (πΉ βΎ βͺ π½):dom (πΉ βΎ βͺ π½)βontoβran (πΉ βΎ βͺ π½) β§ dom (πΉ βΎ βͺ π½) β βͺ π½)
β (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β (π₯ β ran (πΉ βΎ βͺ π½) β§ (β‘(πΉ βΎ βͺ π½) β π₯) β π½))) |
40 | 4, 8, 12, 39 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β (π₯ β ran (πΉ βΎ βͺ π½) β§ (β‘(πΉ βΎ βͺ π½) β π₯) β π½))) |
41 | 40 | biimpa 478 |
. . . . . . . 8
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ π₯ β (π½ qTop (πΉ βΎ βͺ π½))) β (π₯ β ran (πΉ βΎ βͺ π½) β§ (β‘(πΉ βΎ βͺ π½) β π₯) β π½)) |
42 | 41 | adantrr 716 |
. . . . . . 7
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β§ π¦ β (π½ qTop (πΉ βΎ βͺ π½)))) β (π₯ β ran (πΉ βΎ βͺ π½) β§ (β‘(πΉ βΎ βͺ π½) β π₯) β π½)) |
43 | 42 | simpld 496 |
. . . . . 6
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β§ π¦ β (π½ qTop (πΉ βΎ βͺ π½)))) β π₯ β ran (πΉ βΎ βͺ π½)) |
44 | 38, 43 | sstrid 3960 |
. . . . 5
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β§ π¦ β (π½ qTop (πΉ βΎ βͺ π½)))) β (π₯ β© π¦) β ran (πΉ βΎ βͺ π½)) |
45 | 6 | adantr 482 |
. . . . . . 7
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β§ π¦ β (π½ qTop (πΉ βΎ βͺ π½)))) β Fun (πΉ βΎ βͺ π½)) |
46 | | inpreima 7019 |
. . . . . . 7
β’ (Fun
(πΉ βΎ βͺ π½)
β (β‘(πΉ βΎ βͺ π½) β (π₯ β© π¦)) = ((β‘(πΉ βΎ βͺ π½) β π₯) β© (β‘(πΉ βΎ βͺ π½) β π¦))) |
47 | 45, 46 | syl 17 |
. . . . . 6
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β§ π¦ β (π½ qTop (πΉ βΎ βͺ π½)))) β (β‘(πΉ βΎ βͺ π½) β (π₯ β© π¦)) = ((β‘(πΉ βΎ βͺ π½) β π₯) β© (β‘(πΉ βΎ βͺ π½) β π¦))) |
48 | 4 | adantr 482 |
. . . . . . 7
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β§ π¦ β (π½ qTop (πΉ βΎ βͺ π½)))) β π½ β Top) |
49 | 42 | simprd 497 |
. . . . . . 7
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β§ π¦ β (π½ qTop (πΉ βΎ βͺ π½)))) β (β‘(πΉ βΎ βͺ π½) β π₯) β π½) |
50 | 25 | adantrl 715 |
. . . . . . 7
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β§ π¦ β (π½ qTop (πΉ βΎ βͺ π½)))) β (β‘(πΉ βΎ βͺ π½) β π¦) β π½) |
51 | | inopn 22264 |
. . . . . . 7
β’ ((π½ β Top β§ (β‘(πΉ βΎ βͺ π½) β π₯) β π½ β§ (β‘(πΉ βΎ βͺ π½) β π¦) β π½) β ((β‘(πΉ βΎ βͺ π½) β π₯) β© (β‘(πΉ βΎ βͺ π½) β π¦)) β π½) |
52 | 48, 49, 50, 51 | syl3anc 1372 |
. . . . . 6
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β§ π¦ β (π½ qTop (πΉ βΎ βͺ π½)))) β ((β‘(πΉ βΎ βͺ π½) β π₯) β© (β‘(πΉ βΎ βͺ π½) β π¦)) β π½) |
53 | 47, 52 | eqeltrd 2838 |
. . . . 5
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β§ π¦ β (π½ qTop (πΉ βΎ βͺ π½)))) β (β‘(πΉ βΎ βͺ π½) β (π₯ β© π¦)) β π½) |
54 | 1 | elqtop 23064 |
. . . . . . 7
β’ ((π½ β Top β§ (πΉ βΎ βͺ π½):dom (πΉ βΎ βͺ π½)βontoβran (πΉ βΎ βͺ π½) β§ dom (πΉ βΎ βͺ π½) β βͺ π½)
β ((π₯ β© π¦) β (π½ qTop (πΉ βΎ βͺ π½)) β ((π₯ β© π¦) β ran (πΉ βΎ βͺ π½) β§ (β‘(πΉ βΎ βͺ π½) β (π₯ β© π¦)) β π½))) |
55 | 4, 8, 12, 54 | syl3anc 1372 |
. . . . . 6
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β ((π₯ β© π¦) β (π½ qTop (πΉ βΎ βͺ π½)) β ((π₯ β© π¦) β ran (πΉ βΎ βͺ π½) β§ (β‘(πΉ βΎ βͺ π½) β (π₯ β© π¦)) β π½))) |
56 | 55 | adantr 482 |
. . . . 5
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β§ π¦ β (π½ qTop (πΉ βΎ βͺ π½)))) β ((π₯ β© π¦) β (π½ qTop (πΉ βΎ βͺ π½)) β ((π₯ β© π¦) β ran (πΉ βΎ βͺ π½) β§ (β‘(πΉ βΎ βͺ π½) β (π₯ β© π¦)) β π½))) |
57 | 44, 53, 56 | mpbir2and 712 |
. . . 4
β’ (((π½ β Top β§ πΉ β π β§ Fun πΉ) β§ (π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β§ π¦ β (π½ qTop (πΉ βΎ βͺ π½)))) β (π₯ β© π¦) β (π½ qTop (πΉ βΎ βͺ π½))) |
58 | 57 | ralrimivva 3198 |
. . 3
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β βπ₯ β (π½ qTop (πΉ βΎ βͺ π½))βπ¦ β (π½ qTop (πΉ βΎ βͺ π½))(π₯ β© π¦) β (π½ qTop (πΉ βΎ βͺ π½))) |
59 | | ovex 7395 |
. . . 4
β’ (π½ qTop (πΉ βΎ βͺ π½)) β V |
60 | | istopg 22260 |
. . . 4
β’ ((π½ qTop (πΉ βΎ βͺ π½)) β V β ((π½ qTop (πΉ βΎ βͺ π½)) β Top β
(βπ₯(π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β βͺ π₯
β (π½ qTop (πΉ βΎ βͺ π½)))
β§ βπ₯ β
(π½ qTop (πΉ βΎ βͺ π½))βπ¦ β (π½ qTop (πΉ βΎ βͺ π½))(π₯ β© π¦) β (π½ qTop (πΉ βΎ βͺ π½))))) |
61 | 59, 60 | ax-mp 5 |
. . 3
β’ ((π½ qTop (πΉ βΎ βͺ π½)) β Top β
(βπ₯(π₯ β (π½ qTop (πΉ βΎ βͺ π½)) β βͺ π₯
β (π½ qTop (πΉ βΎ βͺ π½)))
β§ βπ₯ β
(π½ qTop (πΉ βΎ βͺ π½))βπ¦ β (π½ qTop (πΉ βΎ βͺ π½))(π₯ β© π¦) β (π½ qTop (πΉ βΎ βͺ π½)))) |
62 | 37, 58, 61 | sylanbrc 584 |
. 2
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (π½ qTop (πΉ βΎ βͺ π½)) β Top) |
63 | 3, 62 | eqeltrd 2838 |
1
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (π½ qTop πΉ) β Top) |