Step | Hyp | Ref
| Expression |
1 | | stoweidlem50.1 |
. . 3
β’
β²π‘π |
2 | | stoweidlem50.4 |
. . . 4
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} |
3 | | nfrab1 3425 |
. . . 4
β’
β²β{β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} |
4 | 2, 3 | nfcxfr 2902 |
. . 3
β’
β²βπ |
5 | | nfv 1918 |
. . 3
β’
β²ππ |
6 | | stoweidlem50.2 |
. . 3
β’
β²π‘π |
7 | | stoweidlem50.3 |
. . 3
β’ πΎ = (topGenβran
(,)) |
8 | | stoweidlem50.5 |
. . 3
β’ π = {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} |
9 | | stoweidlem50.6 |
. . 3
β’ π = βͺ
π½ |
10 | | stoweidlem50.8 |
. . 3
β’ (π β π½ β Comp) |
11 | | stoweidlem50.9 |
. . . 4
β’ (π β π΄ β πΆ) |
12 | | stoweidlem50.7 |
. . . 4
β’ πΆ = (π½ Cn πΎ) |
13 | 11, 12 | sseqtrdi 3995 |
. . 3
β’ (π β π΄ β (π½ Cn πΎ)) |
14 | | stoweidlem50.10 |
. . 3
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
15 | | stoweidlem50.11 |
. . 3
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
16 | | stoweidlem50.12 |
. . 3
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
17 | | stoweidlem50.13 |
. . 3
β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) |
18 | | stoweidlem50.14 |
. . 3
β’ (π β π β π½) |
19 | | stoweidlem50.15 |
. . 3
β’ (π β π β π) |
20 | 10 | uniexd 7680 |
. . . 4
β’ (π β βͺ π½
β V) |
21 | 9, 20 | eqeltrid 2838 |
. . 3
β’ (π β π β V) |
22 | 1, 4, 5, 6, 7, 2, 8, 9, 10, 13, 14, 15, 16, 17, 18, 19, 21 | stoweidlem46 44373 |
. 2
β’ (π β (π β π) β βͺ π) |
23 | | dfin4 4228 |
. . . . . . . . . . 11
β’ (π β© π) = (π β (π β π)) |
24 | | elssuni 4899 |
. . . . . . . . . . . . . 14
β’ (π β π½ β π β βͺ π½) |
25 | 18, 24 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β βͺ π½) |
26 | 25, 9 | sseqtrrdi 3996 |
. . . . . . . . . . . 12
β’ (π β π β π) |
27 | | sseqin2 4176 |
. . . . . . . . . . . 12
β’ (π β π β (π β© π) = π) |
28 | 26, 27 | sylib 217 |
. . . . . . . . . . 11
β’ (π β (π β© π) = π) |
29 | 23, 28 | eqtr3id 2787 |
. . . . . . . . . 10
β’ (π β (π β (π β π)) = π) |
30 | 29, 18 | eqeltrd 2834 |
. . . . . . . . 9
β’ (π β (π β (π β π)) β π½) |
31 | | cmptop 22762 |
. . . . . . . . . . 11
β’ (π½ β Comp β π½ β Top) |
32 | 10, 31 | syl 17 |
. . . . . . . . . 10
β’ (π β π½ β Top) |
33 | | difssd 4093 |
. . . . . . . . . 10
β’ (π β (π β π) β π) |
34 | 9 | iscld2 22395 |
. . . . . . . . . 10
β’ ((π½ β Top β§ (π β π) β π) β ((π β π) β (Clsdβπ½) β (π β (π β π)) β π½)) |
35 | 32, 33, 34 | syl2anc 585 |
. . . . . . . . 9
β’ (π β ((π β π) β (Clsdβπ½) β (π β (π β π)) β π½)) |
36 | 30, 35 | mpbird 257 |
. . . . . . . 8
β’ (π β (π β π) β (Clsdβπ½)) |
37 | | cmpcld 22769 |
. . . . . . . 8
β’ ((π½ β Comp β§ (π β π) β (Clsdβπ½)) β (π½ βΎt (π β π)) β Comp) |
38 | 10, 36, 37 | syl2anc 585 |
. . . . . . 7
β’ (π β (π½ βΎt (π β π)) β Comp) |
39 | 9 | cmpsub 22767 |
. . . . . . . 8
β’ ((π½ β Top β§ (π β π) β π) β ((π½ βΎt (π β π)) β Comp β βπ β π« π½((π β π) β βͺ π β βπ’ β (π« π β© Fin)(π β π) β βͺ π’))) |
40 | 32, 33, 39 | syl2anc 585 |
. . . . . . 7
β’ (π β ((π½ βΎt (π β π)) β Comp β βπ β π« π½((π β π) β βͺ π β βπ’ β (π« π β© Fin)(π β π) β βͺ π’))) |
41 | 38, 40 | mpbid 231 |
. . . . . 6
β’ (π β βπ β π« π½((π β π) β βͺ π β βπ’ β (π« π β© Fin)(π β π) β βͺ π’)) |
42 | | ssrab2 4038 |
. . . . . . . 8
β’ {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} β π½ |
43 | 8, 42 | eqsstri 3979 |
. . . . . . 7
β’ π β π½ |
44 | 8, 10 | rabexd 5291 |
. . . . . . . 8
β’ (π β π β V) |
45 | | elpwg 4564 |
. . . . . . . 8
β’ (π β V β (π β π« π½ β π β π½)) |
46 | 44, 45 | syl 17 |
. . . . . . 7
β’ (π β (π β π« π½ β π β π½)) |
47 | 43, 46 | mpbiri 258 |
. . . . . 6
β’ (π β π β π« π½) |
48 | | unieq 4877 |
. . . . . . . . 9
β’ (π = π β βͺ π = βͺ
π) |
49 | 48 | sseq2d 3977 |
. . . . . . . 8
β’ (π = π β ((π β π) β βͺ π β (π β π) β βͺ π)) |
50 | | pweq 4575 |
. . . . . . . . . 10
β’ (π = π β π« π = π« π) |
51 | 50 | ineq1d 4172 |
. . . . . . . . 9
β’ (π = π β (π« π β© Fin) = (π« π β© Fin)) |
52 | 51 | rexeqdv 3313 |
. . . . . . . 8
β’ (π = π β (βπ’ β (π« π β© Fin)(π β π) β βͺ π’ β βπ’ β (π« π β© Fin)(π β π) β βͺ π’)) |
53 | 49, 52 | imbi12d 345 |
. . . . . . 7
β’ (π = π β (((π β π) β βͺ π β βπ’ β (π« π β© Fin)(π β π) β βͺ π’) β ((π β π) β βͺ π β βπ’ β (π« π β© Fin)(π β π) β βͺ π’))) |
54 | 53 | rspccva 3579 |
. . . . . 6
β’
((βπ β
π« π½((π β π) β βͺ π β βπ’ β (π« π β© Fin)(π β π) β βͺ π’) β§ π β π« π½) β ((π β π) β βͺ π β βπ’ β (π« π β© Fin)(π β π) β βͺ π’)) |
55 | 41, 47, 54 | syl2anc 585 |
. . . . 5
β’ (π β ((π β π) β βͺ π β βπ’ β (π« π β© Fin)(π β π) β βͺ π’)) |
56 | 55 | imp 408 |
. . . 4
β’ ((π β§ (π β π) β βͺ π) β βπ’ β (π« π β© Fin)(π β π) β βͺ π’) |
57 | | df-rex 3071 |
. . . 4
β’
(βπ’ β
(π« π β©
Fin)(π β π) β βͺ π’
β βπ’(π’ β (π« π β© Fin) β§ (π β π) β βͺ π’)) |
58 | 56, 57 | sylib 217 |
. . 3
β’ ((π β§ (π β π) β βͺ π) β βπ’(π’ β (π« π β© Fin) β§ (π β π) β βͺ π’)) |
59 | | elinel2 4157 |
. . . . . . 7
β’ (π’ β (π« π β© Fin) β π’ β Fin) |
60 | 59 | ad2antrl 727 |
. . . . . 6
β’ (((π β§ (π β π) β βͺ π) β§ (π’ β (π« π β© Fin) β§ (π β π) β βͺ π’)) β π’ β Fin) |
61 | | elinel1 4156 |
. . . . . . . 8
β’ (π’ β (π« π β© Fin) β π’ β π« π) |
62 | 61 | ad2antrl 727 |
. . . . . . 7
β’ (((π β§ (π β π) β βͺ π) β§ (π’ β (π« π β© Fin) β§ (π β π) β βͺ π’)) β π’ β π« π) |
63 | 62 | elpwid 4570 |
. . . . . 6
β’ (((π β§ (π β π) β βͺ π) β§ (π’ β (π« π β© Fin) β§ (π β π) β βͺ π’)) β π’ β π) |
64 | | simprr 772 |
. . . . . 6
β’ (((π β§ (π β π) β βͺ π) β§ (π’ β (π« π β© Fin) β§ (π β π) β βͺ π’)) β (π β π) β βͺ π’) |
65 | 60, 63, 64 | 3jca 1129 |
. . . . 5
β’ (((π β§ (π β π) β βͺ π) β§ (π’ β (π« π β© Fin) β§ (π β π) β βͺ π’)) β (π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’)) |
66 | 65 | ex 414 |
. . . 4
β’ ((π β§ (π β π) β βͺ π) β ((π’ β (π« π β© Fin) β§ (π β π) β βͺ π’) β (π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’))) |
67 | 66 | eximdv 1921 |
. . 3
β’ ((π β§ (π β π) β βͺ π) β (βπ’(π’ β (π« π β© Fin) β§ (π β π) β βͺ π’) β βπ’(π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’))) |
68 | 58, 67 | mpd 15 |
. 2
β’ ((π β§ (π β π) β βͺ π) β βπ’(π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’)) |
69 | 22, 68 | mpdan 686 |
1
β’ (π β βπ’(π’ β Fin β§ π’ β π β§ (π β π) β βͺ π’)) |