Step | Hyp | Ref
| Expression |
1 | | lmcnp.4 |
. . . . . 6
β’ (π β πΊ β ((π½ CnP πΎ)βπ)) |
2 | | eqid 2733 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
3 | | eqid 2733 |
. . . . . . 7
β’ βͺ πΎ =
βͺ πΎ |
4 | 2, 3 | cnpf 22751 |
. . . . . 6
β’ (πΊ β ((π½ CnP πΎ)βπ) β πΊ:βͺ π½βΆβͺ πΎ) |
5 | 1, 4 | syl 17 |
. . . . 5
β’ (π β πΊ:βͺ π½βΆβͺ πΎ) |
6 | | lmcnp.3 |
. . . . . . . . 9
β’ (π β πΉ(βπ‘βπ½)π) |
7 | | cnptop1 22746 |
. . . . . . . . . . . 12
β’ (πΊ β ((π½ CnP πΎ)βπ) β π½ β Top) |
8 | 1, 7 | syl 17 |
. . . . . . . . . . 11
β’ (π β π½ β Top) |
9 | | toptopon2 22420 |
. . . . . . . . . . 11
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
10 | 8, 9 | sylib 217 |
. . . . . . . . . 10
β’ (π β π½ β (TopOnββͺ π½)) |
11 | | nnuz 12865 |
. . . . . . . . . 10
β’ β =
(β€β₯β1) |
12 | | 1zzd 12593 |
. . . . . . . . . 10
β’ (π β 1 β
β€) |
13 | 10, 11, 12 | lmbr2 22763 |
. . . . . . . . 9
β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (βͺ π½ βpm β)
β§ π β βͺ π½
β§ βπ£ β
π½ (π β π£ β βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£))))) |
14 | 6, 13 | mpbid 231 |
. . . . . . . 8
β’ (π β (πΉ β (βͺ π½ βpm β)
β§ π β βͺ π½
β§ βπ£ β
π½ (π β π£ β βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£)))) |
15 | 14 | simp1d 1143 |
. . . . . . 7
β’ (π β πΉ β (βͺ π½ βpm
β)) |
16 | 8 | uniexd 7732 |
. . . . . . . 8
β’ (π β βͺ π½
β V) |
17 | | cnex 11191 |
. . . . . . . 8
β’ β
β V |
18 | | elpm2g 8838 |
. . . . . . . 8
β’ ((βͺ π½
β V β§ β β V) β (πΉ β (βͺ π½ βpm β)
β (πΉ:dom πΉβΆβͺ π½
β§ dom πΉ β
β))) |
19 | 16, 17, 18 | sylancl 587 |
. . . . . . 7
β’ (π β (πΉ β (βͺ π½ βpm β)
β (πΉ:dom πΉβΆβͺ π½
β§ dom πΉ β
β))) |
20 | 15, 19 | mpbid 231 |
. . . . . 6
β’ (π β (πΉ:dom πΉβΆβͺ π½ β§ dom πΉ β β)) |
21 | 20 | simpld 496 |
. . . . 5
β’ (π β πΉ:dom πΉβΆβͺ π½) |
22 | | fco 6742 |
. . . . 5
β’ ((πΊ:βͺ
π½βΆβͺ πΎ
β§ πΉ:dom πΉβΆβͺ π½)
β (πΊ β πΉ):dom πΉβΆβͺ πΎ) |
23 | 5, 21, 22 | syl2anc 585 |
. . . 4
β’ (π β (πΊ β πΉ):dom πΉβΆβͺ πΎ) |
24 | 23 | ffdmd 6749 |
. . 3
β’ (π β (πΊ β πΉ):dom (πΊ β πΉ)βΆβͺ πΎ) |
25 | 23 | fdmd 6729 |
. . . 4
β’ (π β dom (πΊ β πΉ) = dom πΉ) |
26 | 20 | simprd 497 |
. . . 4
β’ (π β dom πΉ β β) |
27 | 25, 26 | eqsstrd 4021 |
. . 3
β’ (π β dom (πΊ β πΉ) β β) |
28 | | cnptop2 22747 |
. . . . . 6
β’ (πΊ β ((π½ CnP πΎ)βπ) β πΎ β Top) |
29 | 1, 28 | syl 17 |
. . . . 5
β’ (π β πΎ β Top) |
30 | 29 | uniexd 7732 |
. . . 4
β’ (π β βͺ πΎ
β V) |
31 | | elpm2g 8838 |
. . . 4
β’ ((βͺ πΎ
β V β§ β β V) β ((πΊ β πΉ) β (βͺ πΎ βpm β)
β ((πΊ β πΉ):dom (πΊ β πΉ)βΆβͺ πΎ β§ dom (πΊ β πΉ) β β))) |
32 | 30, 17, 31 | sylancl 587 |
. . 3
β’ (π β ((πΊ β πΉ) β (βͺ πΎ βpm β)
β ((πΊ β πΉ):dom (πΊ β πΉ)βΆβͺ πΎ β§ dom (πΊ β πΉ) β β))) |
33 | 24, 27, 32 | mpbir2and 712 |
. 2
β’ (π β (πΊ β πΉ) β (βͺ πΎ βpm
β)) |
34 | 14 | simp2d 1144 |
. . 3
β’ (π β π β βͺ π½) |
35 | 5, 34 | ffvelcdmd 7088 |
. 2
β’ (π β (πΊβπ) β βͺ πΎ) |
36 | 14 | simp3d 1145 |
. . . . . 6
β’ (π β βπ£ β π½ (π β π£ β βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£))) |
37 | 36 | adantr 482 |
. . . . 5
β’ ((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β βπ£ β π½ (π β π£ β βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£))) |
38 | | cnpimaex 22760 |
. . . . . . 7
β’ ((πΊ β ((π½ CnP πΎ)βπ) β§ π’ β πΎ β§ (πΊβπ) β π’) β βπ£ β π½ (π β π£ β§ (πΊ β π£) β π’)) |
39 | 38 | 3expb 1121 |
. . . . . 6
β’ ((πΊ β ((π½ CnP πΎ)βπ) β§ (π’ β πΎ β§ (πΊβπ) β π’)) β βπ£ β π½ (π β π£ β§ (πΊ β π£) β π’)) |
40 | 1, 39 | sylan 581 |
. . . . 5
β’ ((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β βπ£ β π½ (π β π£ β§ (πΊ β π£) β π’)) |
41 | | r19.29 3115 |
. . . . . . 7
β’
((βπ£ β
π½ (π β π£ β βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£)) β§ βπ£ β π½ (π β π£ β§ (πΊ β π£) β π’)) β βπ£ β π½ ((π β π£ β βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£)) β§ (π β π£ β§ (πΊ β π£) β π’))) |
42 | | pm3.45 623 |
. . . . . . . . 9
β’ ((π β π£ β βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£)) β ((π β π£ β§ (πΊ β π£) β π’) β (βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£) β§ (πΊ β π£) β π’))) |
43 | 42 | imp 408 |
. . . . . . . 8
β’ (((π β π£ β βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£)) β§ (π β π£ β§ (πΊ β π£) β π’)) β (βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£) β§ (πΊ β π£) β π’)) |
44 | 43 | reximi 3085 |
. . . . . . 7
β’
(βπ£ β
π½ ((π β π£ β βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£)) β§ (π β π£ β§ (πΊ β π£) β π’)) β βπ£ β π½ (βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£) β§ (πΊ β π£) β π’)) |
45 | 41, 44 | syl 17 |
. . . . . 6
β’
((βπ£ β
π½ (π β π£ β βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£)) β§ βπ£ β π½ (π β π£ β§ (πΊ β π£) β π’)) β βπ£ β π½ (βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£) β§ (πΊ β π£) β π’)) |
46 | 5 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β§ π β dom πΉ) β πΊ:βͺ π½βΆβͺ πΎ) |
47 | 46 | ffnd 6719 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β§ π β dom πΉ) β πΊ Fn βͺ π½) |
48 | | simplrl 776 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β§ π β dom πΉ) β π£ β π½) |
49 | | elssuni 4942 |
. . . . . . . . . . . . . . . . 17
β’ (π£ β π½ β π£ β βͺ π½) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β§ π β dom πΉ) β π£ β βͺ π½) |
51 | | fnfvima 7235 |
. . . . . . . . . . . . . . . . 17
β’ ((πΊ Fn βͺ
π½ β§ π£ β βͺ π½ β§ (πΉβπ) β π£) β (πΊβ(πΉβπ)) β (πΊ β π£)) |
52 | 51 | 3expia 1122 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ Fn βͺ
π½ β§ π£ β βͺ π½) β ((πΉβπ) β π£ β (πΊβ(πΉβπ)) β (πΊ β π£))) |
53 | 47, 50, 52 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β§ π β dom πΉ) β ((πΉβπ) β π£ β (πΊβ(πΉβπ)) β (πΊ β π£))) |
54 | 21 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β πΉ:dom πΉβΆβͺ π½) |
55 | | fvco3 6991 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ:dom πΉβΆβͺ π½ β§ π β dom πΉ) β ((πΊ β πΉ)βπ) = (πΊβ(πΉβπ))) |
56 | 54, 55 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β§ π β dom πΉ) β ((πΊ β πΉ)βπ) = (πΊβ(πΉβπ))) |
57 | 56 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β§ π β dom πΉ) β (((πΊ β πΉ)βπ) β (πΊ β π£) β (πΊβ(πΉβπ)) β (πΊ β π£))) |
58 | 53, 57 | sylibrd 259 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β§ π β dom πΉ) β ((πΉβπ) β π£ β ((πΊ β πΉ)βπ) β (πΊ β π£))) |
59 | | simplrr 777 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β§ π β dom πΉ) β (πΊ β π£) β π’) |
60 | 59 | sseld 3982 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β§ π β dom πΉ) β (((πΊ β πΉ)βπ) β (πΊ β π£) β ((πΊ β πΉ)βπ) β π’)) |
61 | 58, 60 | syld 47 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β§ π β dom πΉ) β ((πΉβπ) β π£ β ((πΊ β πΉ)βπ) β π’)) |
62 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β§ π β dom πΉ) β π β dom πΉ) |
63 | 25 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β§ π β dom πΉ) β dom (πΊ β πΉ) = dom πΉ) |
64 | 62, 63 | eleqtrrd 2837 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β§ π β dom πΉ) β π β dom (πΊ β πΉ)) |
65 | 61, 64 | jctild 527 |
. . . . . . . . . . . 12
β’ ((((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β§ π β dom πΉ) β ((πΉβπ) β π£ β (π β dom (πΊ β πΉ) β§ ((πΊ β πΉ)βπ) β π’))) |
66 | 65 | expimpd 455 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β ((π β dom πΉ β§ (πΉβπ) β π£) β (π β dom (πΊ β πΉ) β§ ((πΊ β πΉ)βπ) β π’))) |
67 | 66 | ralimdv 3170 |
. . . . . . . . . 10
β’ (((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β (βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£) β βπ β (β€β₯βπ)(π β dom (πΊ β πΉ) β§ ((πΊ β πΉ)βπ) β π’))) |
68 | 67 | reximdv 3171 |
. . . . . . . . 9
β’ (((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ (π£ β π½ β§ (πΊ β π£) β π’)) β (βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£) β βπ β β βπ β (β€β₯βπ)(π β dom (πΊ β πΉ) β§ ((πΊ β πΉ)βπ) β π’))) |
69 | 68 | expr 458 |
. . . . . . . 8
β’ (((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ π£ β π½) β ((πΊ β π£) β π’ β (βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£) β βπ β β βπ β (β€β₯βπ)(π β dom (πΊ β πΉ) β§ ((πΊ β πΉ)βπ) β π’)))) |
70 | 69 | impcomd 413 |
. . . . . . 7
β’ (((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β§ π£ β π½) β ((βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£) β§ (πΊ β π£) β π’) β βπ β β βπ β (β€β₯βπ)(π β dom (πΊ β πΉ) β§ ((πΊ β πΉ)βπ) β π’))) |
71 | 70 | rexlimdva 3156 |
. . . . . 6
β’ ((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β (βπ£ β π½ (βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£) β§ (πΊ β π£) β π’) β βπ β β βπ β (β€β₯βπ)(π β dom (πΊ β πΉ) β§ ((πΊ β πΉ)βπ) β π’))) |
72 | 45, 71 | syl5 34 |
. . . . 5
β’ ((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β ((βπ£ β π½ (π β π£ β βπ β β βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π£)) β§ βπ£ β π½ (π β π£ β§ (πΊ β π£) β π’)) β βπ β β βπ β (β€β₯βπ)(π β dom (πΊ β πΉ) β§ ((πΊ β πΉ)βπ) β π’))) |
73 | 37, 40, 72 | mp2and 698 |
. . . 4
β’ ((π β§ (π’ β πΎ β§ (πΊβπ) β π’)) β βπ β β βπ β (β€β₯βπ)(π β dom (πΊ β πΉ) β§ ((πΊ β πΉ)βπ) β π’)) |
74 | 73 | expr 458 |
. . 3
β’ ((π β§ π’ β πΎ) β ((πΊβπ) β π’ β βπ β β βπ β (β€β₯βπ)(π β dom (πΊ β πΉ) β§ ((πΊ β πΉ)βπ) β π’))) |
75 | 74 | ralrimiva 3147 |
. 2
β’ (π β βπ’ β πΎ ((πΊβπ) β π’ β βπ β β βπ β (β€β₯βπ)(π β dom (πΊ β πΉ) β§ ((πΊ β πΉ)βπ) β π’))) |
76 | | toptopon2 22420 |
. . . 4
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
77 | 29, 76 | sylib 217 |
. . 3
β’ (π β πΎ β (TopOnββͺ πΎ)) |
78 | 77, 11, 12 | lmbr2 22763 |
. 2
β’ (π β ((πΊ β πΉ)(βπ‘βπΎ)(πΊβπ) β ((πΊ β πΉ) β (βͺ πΎ βpm β)
β§ (πΊβπ) β βͺ πΎ
β§ βπ’ β
πΎ ((πΊβπ) β π’ β βπ β β βπ β (β€β₯βπ)(π β dom (πΊ β πΉ) β§ ((πΊ β πΉ)βπ) β π’))))) |
79 | 33, 35, 75, 78 | mpbir3and 1343 |
1
β’ (π β (πΊ β πΉ)(βπ‘βπΎ)(πΊβπ)) |