Step | Hyp | Ref
| Expression |
1 | | nn0ex 12427 |
. . . . . 6
β’
β0 β V |
2 | | fvex 6859 |
. . . . . . 7
β’ (πΉβπ‘) β V |
3 | | vsnex 5390 |
. . . . . . 7
β’ {π‘} β V |
4 | 2, 3 | xpex 7691 |
. . . . . 6
β’ ((πΉβπ‘) Γ {π‘}) β V |
5 | 1, 4 | iunex 7905 |
. . . . 5
β’ βͺ π‘ β β0 ((πΉβπ‘) Γ {π‘}) β V |
6 | | heibor.4 |
. . . . . . . . 9
β’ πΊ = {β¨π¦, πβ© β£ (π β β0 β§ π¦ β (πΉβπ) β§ (π¦π΅π) β πΎ)} |
7 | 6 | relopabiv 5780 |
. . . . . . . 8
β’ Rel πΊ |
8 | | 1st2nd 7975 |
. . . . . . . 8
β’ ((Rel
πΊ β§ π₯ β πΊ) β π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) |
9 | 7, 8 | mpan 689 |
. . . . . . 7
β’ (π₯ β πΊ β π₯ = β¨(1st βπ₯), (2nd βπ₯)β©) |
10 | 9 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (π₯ β πΊ β (π₯ β πΊ β β¨(1st βπ₯), (2nd βπ₯)β© β πΊ)) |
11 | | df-br 5110 |
. . . . . . . . . . 11
β’
((1st βπ₯)πΊ(2nd βπ₯) β β¨(1st βπ₯), (2nd βπ₯)β© β πΊ) |
12 | 10, 11 | bitr4di 289 |
. . . . . . . . . 10
β’ (π₯ β πΊ β (π₯ β πΊ β (1st βπ₯)πΊ(2nd βπ₯))) |
13 | | heibor.1 |
. . . . . . . . . . 11
β’ π½ = (MetOpenβπ·) |
14 | | heibor.3 |
. . . . . . . . . . 11
β’ πΎ = {π’ β£ Β¬ βπ£ β (π« π β© Fin)π’ β βͺ π£} |
15 | | fvex 6859 |
. . . . . . . . . . 11
β’
(1st βπ₯) β V |
16 | | fvex 6859 |
. . . . . . . . . . 11
β’
(2nd βπ₯) β V |
17 | 13, 14, 6, 15, 16 | heiborlem2 36321 |
. . . . . . . . . 10
β’
((1st βπ₯)πΊ(2nd βπ₯) β ((2nd βπ₯) β β0
β§ (1st βπ₯) β (πΉβ(2nd βπ₯)) β§ ((1st
βπ₯)π΅(2nd βπ₯)) β πΎ)) |
18 | 12, 17 | bitrdi 287 |
. . . . . . . . 9
β’ (π₯ β πΊ β (π₯ β πΊ β ((2nd βπ₯) β β0
β§ (1st βπ₯) β (πΉβ(2nd βπ₯)) β§ ((1st
βπ₯)π΅(2nd βπ₯)) β πΎ))) |
19 | 18 | ibi 267 |
. . . . . . . 8
β’ (π₯ β πΊ β ((2nd βπ₯) β β0
β§ (1st βπ₯) β (πΉβ(2nd βπ₯)) β§ ((1st
βπ₯)π΅(2nd βπ₯)) β πΎ)) |
20 | 16 | snid 4626 |
. . . . . . . . . . . 12
β’
(2nd βπ₯) β {(2nd βπ₯)} |
21 | | opelxp 5673 |
. . . . . . . . . . . 12
β’
(β¨(1st βπ₯), (2nd βπ₯)β© β ((πΉβ(2nd βπ₯)) Γ {(2nd
βπ₯)}) β
((1st βπ₯)
β (πΉβ(2nd βπ₯)) β§ (2nd
βπ₯) β
{(2nd βπ₯)})) |
22 | 20, 21 | mpbiran2 709 |
. . . . . . . . . . 11
β’
(β¨(1st βπ₯), (2nd βπ₯)β© β ((πΉβ(2nd βπ₯)) Γ {(2nd
βπ₯)}) β
(1st βπ₯)
β (πΉβ(2nd βπ₯))) |
23 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π‘ = (2nd βπ₯) β (πΉβπ‘) = (πΉβ(2nd βπ₯))) |
24 | | sneq 4600 |
. . . . . . . . . . . . . 14
β’ (π‘ = (2nd βπ₯) β {π‘} = {(2nd βπ₯)}) |
25 | 23, 24 | xpeq12d 5668 |
. . . . . . . . . . . . 13
β’ (π‘ = (2nd βπ₯) β ((πΉβπ‘) Γ {π‘}) = ((πΉβ(2nd βπ₯)) Γ {(2nd
βπ₯)})) |
26 | 25 | eleq2d 2820 |
. . . . . . . . . . . 12
β’ (π‘ = (2nd βπ₯) β (β¨(1st
βπ₯), (2nd
βπ₯)β© β
((πΉβπ‘) Γ {π‘}) β β¨(1st βπ₯), (2nd βπ₯)β© β ((πΉβ(2nd
βπ₯)) Γ
{(2nd βπ₯)}))) |
27 | 26 | rspcev 3583 |
. . . . . . . . . . 11
β’
(((2nd βπ₯) β β0 β§
β¨(1st βπ₯), (2nd βπ₯)β© β ((πΉβ(2nd βπ₯)) Γ {(2nd
βπ₯)})) β
βπ‘ β
β0 β¨(1st βπ₯), (2nd βπ₯)β© β ((πΉβπ‘) Γ {π‘})) |
28 | 22, 27 | sylan2br 596 |
. . . . . . . . . 10
β’
(((2nd βπ₯) β β0 β§
(1st βπ₯)
β (πΉβ(2nd βπ₯))) β βπ‘ β β0
β¨(1st βπ₯), (2nd βπ₯)β© β ((πΉβπ‘) Γ {π‘})) |
29 | | eliun 4962 |
. . . . . . . . . 10
β’
(β¨(1st βπ₯), (2nd βπ₯)β© β βͺ π‘ β β0 ((πΉβπ‘) Γ {π‘}) β βπ‘ β β0
β¨(1st βπ₯), (2nd βπ₯)β© β ((πΉβπ‘) Γ {π‘})) |
30 | 28, 29 | sylibr 233 |
. . . . . . . . 9
β’
(((2nd βπ₯) β β0 β§
(1st βπ₯)
β (πΉβ(2nd βπ₯))) β β¨(1st
βπ₯), (2nd
βπ₯)β© β
βͺ π‘ β β0 ((πΉβπ‘) Γ {π‘})) |
31 | 30 | 3adant3 1133 |
. . . . . . . 8
β’
(((2nd βπ₯) β β0 β§
(1st βπ₯)
β (πΉβ(2nd βπ₯)) β§ ((1st
βπ₯)π΅(2nd βπ₯)) β πΎ) β β¨(1st βπ₯), (2nd βπ₯)β© β βͺ π‘ β β0 ((πΉβπ‘) Γ {π‘})) |
32 | 19, 31 | syl 17 |
. . . . . . 7
β’ (π₯ β πΊ β β¨(1st βπ₯), (2nd βπ₯)β© β βͺ π‘ β β0 ((πΉβπ‘) Γ {π‘})) |
33 | 9, 32 | eqeltrd 2834 |
. . . . . 6
β’ (π₯ β πΊ β π₯ β βͺ
π‘ β
β0 ((πΉβπ‘) Γ {π‘})) |
34 | 33 | ssriv 3952 |
. . . . 5
β’ πΊ β βͺ π‘ β β0 ((πΉβπ‘) Γ {π‘}) |
35 | | ssdomg 8946 |
. . . . 5
β’ (βͺ π‘ β β0 ((πΉβπ‘) Γ {π‘}) β V β (πΊ β βͺ
π‘ β
β0 ((πΉβπ‘) Γ {π‘}) β πΊ βΌ βͺ
π‘ β
β0 ((πΉβπ‘) Γ {π‘}))) |
36 | 5, 34, 35 | mp2 9 |
. . . 4
β’ πΊ βΌ βͺ π‘ β β0 ((πΉβπ‘) Γ {π‘}) |
37 | | nn0ennn 13893 |
. . . . . . 7
β’
β0 β β |
38 | | nnenom 13894 |
. . . . . . 7
β’ β
β Ο |
39 | 37, 38 | entri 8954 |
. . . . . 6
β’
β0 β Ο |
40 | | endom 8925 |
. . . . . 6
β’
(β0 β Ο β β0 βΌ
Ο) |
41 | 39, 40 | ax-mp 5 |
. . . . 5
β’
β0 βΌ Ο |
42 | | vex 3451 |
. . . . . . . 8
β’ π‘ β V |
43 | 2, 42 | xpsnen 9005 |
. . . . . . 7
β’ ((πΉβπ‘) Γ {π‘}) β (πΉβπ‘) |
44 | | inss2 4193 |
. . . . . . . . 9
β’
(π« π β©
Fin) β Fin |
45 | | heibor.7 |
. . . . . . . . . 10
β’ (π β πΉ:β0βΆ(π« π β© Fin)) |
46 | 45 | ffvelcdmda 7039 |
. . . . . . . . 9
β’ ((π β§ π‘ β β0) β (πΉβπ‘) β (π« π β© Fin)) |
47 | 44, 46 | sselid 3946 |
. . . . . . . 8
β’ ((π β§ π‘ β β0) β (πΉβπ‘) β Fin) |
48 | | isfinite 9596 |
. . . . . . . . 9
β’ ((πΉβπ‘) β Fin β (πΉβπ‘) βΊ Ο) |
49 | | sdomdom 8926 |
. . . . . . . . 9
β’ ((πΉβπ‘) βΊ Ο β (πΉβπ‘) βΌ Ο) |
50 | 48, 49 | sylbi 216 |
. . . . . . . 8
β’ ((πΉβπ‘) β Fin β (πΉβπ‘) βΌ Ο) |
51 | 47, 50 | syl 17 |
. . . . . . 7
β’ ((π β§ π‘ β β0) β (πΉβπ‘) βΌ Ο) |
52 | | endomtr 8958 |
. . . . . . 7
β’ ((((πΉβπ‘) Γ {π‘}) β (πΉβπ‘) β§ (πΉβπ‘) βΌ Ο) β ((πΉβπ‘) Γ {π‘}) βΌ Ο) |
53 | 43, 51, 52 | sylancr 588 |
. . . . . 6
β’ ((π β§ π‘ β β0) β ((πΉβπ‘) Γ {π‘}) βΌ Ο) |
54 | 53 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ‘ β β0 ((πΉβπ‘) Γ {π‘}) βΌ Ο) |
55 | | iunctb 10518 |
. . . . 5
β’
((β0 βΌ Ο β§ βπ‘ β β0 ((πΉβπ‘) Γ {π‘}) βΌ Ο) β βͺ π‘ β β0 ((πΉβπ‘) Γ {π‘}) βΌ Ο) |
56 | 41, 54, 55 | sylancr 588 |
. . . 4
β’ (π β βͺ π‘ β β0 ((πΉβπ‘) Γ {π‘}) βΌ Ο) |
57 | | domtr 8953 |
. . . 4
β’ ((πΊ βΌ βͺ π‘ β β0 ((πΉβπ‘) Γ {π‘}) β§ βͺ
π‘ β
β0 ((πΉβπ‘) Γ {π‘}) βΌ Ο) β πΊ βΌ Ο) |
58 | 36, 56, 57 | sylancr 588 |
. . 3
β’ (π β πΊ βΌ Ο) |
59 | 19 | simp1d 1143 |
. . . . . . . . 9
β’ (π₯ β πΊ β (2nd βπ₯) β
β0) |
60 | | peano2nn0 12461 |
. . . . . . . . 9
β’
((2nd βπ₯) β β0 β
((2nd βπ₯)
+ 1) β β0) |
61 | 59, 60 | syl 17 |
. . . . . . . 8
β’ (π₯ β πΊ β ((2nd βπ₯) + 1) β
β0) |
62 | | ffvelcdm 7036 |
. . . . . . . 8
β’ ((πΉ:β0βΆ(π« π β© Fin) β§
((2nd βπ₯)
+ 1) β β0) β (πΉβ((2nd βπ₯) + 1)) β (π« π β© Fin)) |
63 | 45, 61, 62 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π₯ β πΊ) β (πΉβ((2nd βπ₯) + 1)) β (π« π β© Fin)) |
64 | 44, 63 | sselid 3946 |
. . . . . 6
β’ ((π β§ π₯ β πΊ) β (πΉβ((2nd βπ₯) + 1)) β
Fin) |
65 | | iunin2 5035 |
. . . . . . . 8
β’ βͺ π‘ β (πΉβ((2nd βπ₯) + 1))((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) = ((π΅βπ₯) β© βͺ
π‘ β (πΉβ((2nd βπ₯) + 1))(π‘π΅((2nd βπ₯) + 1))) |
66 | | heibor.8 |
. . . . . . . . . . 11
β’ (π β βπ β β0 π = βͺ π¦ β (πΉβπ)(π¦π΅π)) |
67 | | oveq1 7368 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π‘ β (π¦π΅π) = (π‘π΅π)) |
68 | 67 | cbviunv 5004 |
. . . . . . . . . . . . . . 15
β’ βͺ π¦ β (πΉβπ)(π¦π΅π) = βͺ π‘ β (πΉβπ)(π‘π΅π) |
69 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
β’ (π = ((2nd βπ₯) + 1) β (πΉβπ) = (πΉβ((2nd βπ₯) + 1))) |
70 | 69 | iuneq1d 4985 |
. . . . . . . . . . . . . . 15
β’ (π = ((2nd βπ₯) + 1) β βͺ π‘ β (πΉβπ)(π‘π΅π) = βͺ π‘ β (πΉβ((2nd βπ₯) + 1))(π‘π΅π)) |
71 | 68, 70 | eqtrid 2785 |
. . . . . . . . . . . . . 14
β’ (π = ((2nd βπ₯) + 1) β βͺ π¦ β (πΉβπ)(π¦π΅π) = βͺ π‘ β (πΉβ((2nd βπ₯) + 1))(π‘π΅π)) |
72 | | oveq2 7369 |
. . . . . . . . . . . . . . 15
β’ (π = ((2nd βπ₯) + 1) β (π‘π΅π) = (π‘π΅((2nd βπ₯) + 1))) |
73 | 72 | iuneq2d 4987 |
. . . . . . . . . . . . . 14
β’ (π = ((2nd βπ₯) + 1) β βͺ π‘ β (πΉβ((2nd βπ₯) + 1))(π‘π΅π) = βͺ π‘ β (πΉβ((2nd βπ₯) + 1))(π‘π΅((2nd βπ₯) + 1))) |
74 | 71, 73 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (π = ((2nd βπ₯) + 1) β βͺ π¦ β (πΉβπ)(π¦π΅π) = βͺ π‘ β (πΉβ((2nd βπ₯) + 1))(π‘π΅((2nd βπ₯) + 1))) |
75 | 74 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π = ((2nd βπ₯) + 1) β (π = βͺ π¦ β (πΉβπ)(π¦π΅π) β π = βͺ π‘ β (πΉβ((2nd βπ₯) + 1))(π‘π΅((2nd βπ₯) + 1)))) |
76 | 75 | rspccva 3582 |
. . . . . . . . . . 11
β’
((βπ β
β0 π =
βͺ π¦ β (πΉβπ)(π¦π΅π) β§ ((2nd βπ₯) + 1) β
β0) β π = βͺ π‘ β (πΉβ((2nd βπ₯) + 1))(π‘π΅((2nd βπ₯) + 1))) |
77 | 66, 61, 76 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΊ) β π = βͺ π‘ β (πΉβ((2nd βπ₯) + 1))(π‘π΅((2nd βπ₯) + 1))) |
78 | 77 | ineq2d 4176 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΊ) β ((π΅βπ₯) β© π) = ((π΅βπ₯) β© βͺ
π‘ β (πΉβ((2nd βπ₯) + 1))(π‘π΅((2nd βπ₯) + 1)))) |
79 | 9 | fveq2d 6850 |
. . . . . . . . . . . . . 14
β’ (π₯ β πΊ β (π΅βπ₯) = (π΅ββ¨(1st βπ₯), (2nd βπ₯)β©)) |
80 | | df-ov 7364 |
. . . . . . . . . . . . . 14
β’
((1st βπ₯)π΅(2nd βπ₯)) = (π΅ββ¨(1st βπ₯), (2nd βπ₯)β©) |
81 | 79, 80 | eqtr4di 2791 |
. . . . . . . . . . . . 13
β’ (π₯ β πΊ β (π΅βπ₯) = ((1st βπ₯)π΅(2nd βπ₯))) |
82 | 81 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β πΊ) β (π΅βπ₯) = ((1st βπ₯)π΅(2nd βπ₯))) |
83 | | inss1 4192 |
. . . . . . . . . . . . . . . 16
β’
(π« π β©
Fin) β π« π |
84 | | ffvelcdm 7036 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ:β0βΆ(π« π β© Fin) β§
(2nd βπ₯)
β β0) β (πΉβ(2nd βπ₯)) β (π« π β© Fin)) |
85 | 45, 59, 84 | syl2an 597 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β πΊ) β (πΉβ(2nd βπ₯)) β (π« π β© Fin)) |
86 | 83, 85 | sselid 3946 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β πΊ) β (πΉβ(2nd βπ₯)) β π« π) |
87 | 86 | elpwid 4573 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β πΊ) β (πΉβ(2nd βπ₯)) β π) |
88 | 19 | simp2d 1144 |
. . . . . . . . . . . . . . 15
β’ (π₯ β πΊ β (1st βπ₯) β (πΉβ(2nd βπ₯))) |
89 | 88 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β πΊ) β (1st βπ₯) β (πΉβ(2nd βπ₯))) |
90 | 87, 89 | sseldd 3949 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β πΊ) β (1st βπ₯) β π) |
91 | 59 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β πΊ) β (2nd βπ₯) β
β0) |
92 | | oveq1 7368 |
. . . . . . . . . . . . . 14
β’ (π§ = (1st βπ₯) β (π§(ballβπ·)(1 / (2βπ))) = ((1st βπ₯)(ballβπ·)(1 / (2βπ)))) |
93 | | oveq2 7369 |
. . . . . . . . . . . . . . . 16
β’ (π = (2nd βπ₯) β (2βπ) = (2β(2nd
βπ₯))) |
94 | 93 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
β’ (π = (2nd βπ₯) β (1 / (2βπ)) = (1 /
(2β(2nd βπ₯)))) |
95 | 94 | oveq2d 7377 |
. . . . . . . . . . . . . 14
β’ (π = (2nd βπ₯) β ((1st
βπ₯)(ballβπ·)(1 / (2βπ))) = ((1st βπ₯)(ballβπ·)(1 / (2β(2nd βπ₯))))) |
96 | | heibor.5 |
. . . . . . . . . . . . . 14
β’ π΅ = (π§ β π, π β β0 β¦ (π§(ballβπ·)(1 / (2βπ)))) |
97 | | ovex 7394 |
. . . . . . . . . . . . . 14
β’
((1st βπ₯)(ballβπ·)(1 / (2β(2nd βπ₯)))) β V |
98 | 92, 95, 96, 97 | ovmpo 7519 |
. . . . . . . . . . . . 13
β’
(((1st βπ₯) β π β§ (2nd βπ₯) β β0)
β ((1st βπ₯)π΅(2nd βπ₯)) = ((1st βπ₯)(ballβπ·)(1 / (2β(2nd βπ₯))))) |
99 | 90, 91, 98 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β πΊ) β ((1st βπ₯)π΅(2nd βπ₯)) = ((1st βπ₯)(ballβπ·)(1 / (2β(2nd βπ₯))))) |
100 | 82, 99 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β πΊ) β (π΅βπ₯) = ((1st βπ₯)(ballβπ·)(1 / (2β(2nd βπ₯))))) |
101 | | heibor.6 |
. . . . . . . . . . . . . . 15
β’ (π β π· β (CMetβπ)) |
102 | | cmetmet 24673 |
. . . . . . . . . . . . . . 15
β’ (π· β (CMetβπ) β π· β (Metβπ)) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π· β (Metβπ)) |
104 | | metxmet 23710 |
. . . . . . . . . . . . . 14
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π· β (βMetβπ)) |
106 | 105 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β πΊ) β π· β (βMetβπ)) |
107 | | 2nn 12234 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β |
108 | | nnexpcl 13989 |
. . . . . . . . . . . . . . . 16
β’ ((2
β β β§ (2nd βπ₯) β β0) β
(2β(2nd βπ₯)) β β) |
109 | 107, 91, 108 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β πΊ) β (2β(2nd
βπ₯)) β
β) |
110 | 109 | nnrpd 12963 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β πΊ) β (2β(2nd
βπ₯)) β
β+) |
111 | 110 | rpreccld 12975 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β πΊ) β (1 / (2β(2nd
βπ₯))) β
β+) |
112 | 111 | rpxrd 12966 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β πΊ) β (1 / (2β(2nd
βπ₯))) β
β*) |
113 | | blssm 23794 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ (1st
βπ₯) β π β§ (1 /
(2β(2nd βπ₯))) β β*) β
((1st βπ₯)(ballβπ·)(1 / (2β(2nd βπ₯)))) β π) |
114 | 106, 90, 112, 113 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β πΊ) β ((1st βπ₯)(ballβπ·)(1 / (2β(2nd βπ₯)))) β π) |
115 | 100, 114 | eqsstrd 3986 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΊ) β (π΅βπ₯) β π) |
116 | | df-ss 3931 |
. . . . . . . . . 10
β’ ((π΅βπ₯) β π β ((π΅βπ₯) β© π) = (π΅βπ₯)) |
117 | 115, 116 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΊ) β ((π΅βπ₯) β© π) = (π΅βπ₯)) |
118 | 78, 117 | eqtr3d 2775 |
. . . . . . . 8
β’ ((π β§ π₯ β πΊ) β ((π΅βπ₯) β© βͺ
π‘ β (πΉβ((2nd βπ₯) + 1))(π‘π΅((2nd βπ₯) + 1))) = (π΅βπ₯)) |
119 | 65, 118 | eqtrid 2785 |
. . . . . . 7
β’ ((π β§ π₯ β πΊ) β βͺ
π‘ β (πΉβ((2nd βπ₯) + 1))((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) = (π΅βπ₯)) |
120 | | eqimss2 4005 |
. . . . . . 7
β’ (βͺ π‘ β (πΉβ((2nd βπ₯) + 1))((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) = (π΅βπ₯) β (π΅βπ₯) β βͺ
π‘ β (πΉβ((2nd βπ₯) + 1))((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1)))) |
121 | 119, 120 | syl 17 |
. . . . . 6
β’ ((π β§ π₯ β πΊ) β (π΅βπ₯) β βͺ
π‘ β (πΉβ((2nd βπ₯) + 1))((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1)))) |
122 | 19 | simp3d 1145 |
. . . . . . . 8
β’ (π₯ β πΊ β ((1st βπ₯)π΅(2nd βπ₯)) β πΎ) |
123 | 81, 122 | eqeltrd 2834 |
. . . . . . 7
β’ (π₯ β πΊ β (π΅βπ₯) β πΎ) |
124 | 123 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ β πΊ) β (π΅βπ₯) β πΎ) |
125 | | fvex 6859 |
. . . . . . . 8
β’ (π΅βπ₯) β V |
126 | 125 | inex1 5278 |
. . . . . . 7
β’ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β V |
127 | 13, 14, 126 | heiborlem1 36320 |
. . . . . 6
β’ (((πΉβ((2nd
βπ₯) + 1)) β Fin
β§ (π΅βπ₯) β βͺ π‘ β (πΉβ((2nd βπ₯) + 1))((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β§ (π΅βπ₯) β πΎ) β βπ‘ β (πΉβ((2nd βπ₯) + 1))((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ) |
128 | 64, 121, 124, 127 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π₯ β πΊ) β βπ‘ β (πΉβ((2nd βπ₯) + 1))((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ) |
129 | 83, 63 | sselid 3946 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β πΊ) β (πΉβ((2nd βπ₯) + 1)) β π« π) |
130 | 129 | elpwid 4573 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β πΊ) β (πΉβ((2nd βπ₯) + 1)) β π) |
131 | 13 | mopnuni 23817 |
. . . . . . . . . . . . 13
β’ (π· β (βMetβπ) β π = βͺ π½) |
132 | 105, 131 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π = βͺ π½) |
133 | 132 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β πΊ) β π = βͺ π½) |
134 | 130, 133 | sseqtrd 3988 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΊ) β (πΉβ((2nd βπ₯) + 1)) β βͺ π½) |
135 | 134 | sselda 3948 |
. . . . . . . . 9
β’ (((π β§ π₯ β πΊ) β§ π‘ β (πΉβ((2nd βπ₯) + 1))) β π‘ β βͺ π½) |
136 | 135 | adantrr 716 |
. . . . . . . 8
β’ (((π β§ π₯ β πΊ) β§ (π‘ β (πΉβ((2nd βπ₯) + 1)) β§ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ)) β π‘ β βͺ π½) |
137 | 61 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β πΊ) β ((2nd βπ₯) + 1) β
β0) |
138 | | id 22 |
. . . . . . . . . 10
β’ (π‘ β (πΉβ((2nd βπ₯) + 1)) β π‘ β (πΉβ((2nd βπ₯) + 1))) |
139 | | snfi 8994 |
. . . . . . . . . . . 12
β’ {(π‘π΅((2nd βπ₯) + 1))} β Fin |
140 | | inss2 4193 |
. . . . . . . . . . . . 13
β’ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β (π‘π΅((2nd βπ₯) + 1)) |
141 | | ovex 7394 |
. . . . . . . . . . . . . . 15
β’ (π‘π΅((2nd βπ₯) + 1)) β V |
142 | 141 | unisn 4891 |
. . . . . . . . . . . . . 14
β’ βͺ {(π‘π΅((2nd βπ₯) + 1))} = (π‘π΅((2nd βπ₯) + 1)) |
143 | | uniiun 5022 |
. . . . . . . . . . . . . 14
β’ βͺ {(π‘π΅((2nd βπ₯) + 1))} = βͺ π β {(π‘π΅((2nd βπ₯) + 1))}π |
144 | 142, 143 | eqtr3i 2763 |
. . . . . . . . . . . . 13
β’ (π‘π΅((2nd βπ₯) + 1)) = βͺ
π β {(π‘π΅((2nd βπ₯) + 1))}π |
145 | 140, 144 | sseqtri 3984 |
. . . . . . . . . . . 12
β’ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β βͺ π β {(π‘π΅((2nd βπ₯) + 1))}π |
146 | | vex 3451 |
. . . . . . . . . . . . 13
β’ π β V |
147 | 13, 14, 146 | heiborlem1 36320 |
. . . . . . . . . . . 12
β’ (({(π‘π΅((2nd βπ₯) + 1))} β Fin β§ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β βͺ π β {(π‘π΅((2nd βπ₯) + 1))}π β§ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ) β βπ β {(π‘π΅((2nd βπ₯) + 1))}π β πΎ) |
148 | 139, 145,
147 | mp3an12 1452 |
. . . . . . . . . . 11
β’ (((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ β βπ β {(π‘π΅((2nd βπ₯) + 1))}π β πΎ) |
149 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π = (π‘π΅((2nd βπ₯) + 1)) β (π β πΎ β (π‘π΅((2nd βπ₯) + 1)) β πΎ)) |
150 | 141, 149 | rexsn 4647 |
. . . . . . . . . . 11
β’
(βπ β
{(π‘π΅((2nd βπ₯) + 1))}π β πΎ β (π‘π΅((2nd βπ₯) + 1)) β πΎ) |
151 | 148, 150 | sylib 217 |
. . . . . . . . . 10
β’ (((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ β (π‘π΅((2nd βπ₯) + 1)) β πΎ) |
152 | | ovex 7394 |
. . . . . . . . . . . 12
β’
((2nd βπ₯) + 1) β V |
153 | 13, 14, 6, 42, 152 | heiborlem2 36321 |
. . . . . . . . . . 11
β’ (π‘πΊ((2nd βπ₯) + 1) β (((2nd βπ₯) + 1) β
β0 β§ π‘
β (πΉβ((2nd βπ₯) + 1)) β§ (π‘π΅((2nd βπ₯) + 1)) β πΎ)) |
154 | 153 | biimpri 227 |
. . . . . . . . . 10
β’
((((2nd βπ₯) + 1) β β0 β§ π‘ β (πΉβ((2nd βπ₯) + 1)) β§ (π‘π΅((2nd βπ₯) + 1)) β πΎ) β π‘πΊ((2nd βπ₯) + 1)) |
155 | 137, 138,
151, 154 | syl3an 1161 |
. . . . . . . . 9
β’ (((π β§ π₯ β πΊ) β§ π‘ β (πΉβ((2nd βπ₯) + 1)) β§ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ) β π‘πΊ((2nd βπ₯) + 1)) |
156 | 155 | 3expb 1121 |
. . . . . . . 8
β’ (((π β§ π₯ β πΊ) β§ (π‘ β (πΉβ((2nd βπ₯) + 1)) β§ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ)) β π‘πΊ((2nd βπ₯) + 1)) |
157 | | simprr 772 |
. . . . . . . 8
β’ (((π β§ π₯ β πΊ) β§ (π‘ β (πΉβ((2nd βπ₯) + 1)) β§ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ)) β ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ) |
158 | 136, 156,
157 | jca32 517 |
. . . . . . 7
β’ (((π β§ π₯ β πΊ) β§ (π‘ β (πΉβ((2nd βπ₯) + 1)) β§ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ)) β (π‘ β βͺ π½ β§ (π‘πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ))) |
159 | 158 | ex 414 |
. . . . . 6
β’ ((π β§ π₯ β πΊ) β ((π‘ β (πΉβ((2nd βπ₯) + 1)) β§ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ) β (π‘ β βͺ π½ β§ (π‘πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ)))) |
160 | 159 | reximdv2 3158 |
. . . . 5
β’ ((π β§ π₯ β πΊ) β (βπ‘ β (πΉβ((2nd βπ₯) + 1))((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ β βπ‘ β βͺ π½(π‘πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ))) |
161 | 128, 160 | mpd 15 |
. . . 4
β’ ((π β§ π₯ β πΊ) β βπ‘ β βͺ π½(π‘πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ)) |
162 | 161 | ralrimiva 3140 |
. . 3
β’ (π β βπ₯ β πΊ βπ‘ β βͺ π½(π‘πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ)) |
163 | 13 | fvexi 6860 |
. . . . 5
β’ π½ β V |
164 | 163 | uniex 7682 |
. . . 4
β’ βͺ π½
β V |
165 | | breq1 5112 |
. . . . 5
β’ (π‘ = (πβπ₯) β (π‘πΊ((2nd βπ₯) + 1) β (πβπ₯)πΊ((2nd βπ₯) + 1))) |
166 | | oveq1 7368 |
. . . . . . 7
β’ (π‘ = (πβπ₯) β (π‘π΅((2nd βπ₯) + 1)) = ((πβπ₯)π΅((2nd βπ₯) + 1))) |
167 | 166 | ineq2d 4176 |
. . . . . 6
β’ (π‘ = (πβπ₯) β ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) = ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1)))) |
168 | 167 | eleq1d 2819 |
. . . . 5
β’ (π‘ = (πβπ₯) β (((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ β ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ)) |
169 | 165, 168 | anbi12d 632 |
. . . 4
β’ (π‘ = (πβπ₯) β ((π‘πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ) β ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ))) |
170 | 164, 169 | axcc4dom 10385 |
. . 3
β’ ((πΊ βΌ Ο β§
βπ₯ β πΊ βπ‘ β βͺ π½(π‘πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© (π‘π΅((2nd βπ₯) + 1))) β πΎ)) β βπ(π:πΊβΆβͺ π½ β§ βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ))) |
171 | 58, 162, 170 | syl2anc 585 |
. 2
β’ (π β βπ(π:πΊβΆβͺ π½ β§ βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ))) |
172 | | exsimpr 1873 |
. 2
β’
(βπ(π:πΊβΆβͺ π½ β§ βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ)) β βπβπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ)) |
173 | 171, 172 | syl 17 |
1
β’ (π β βπβπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ)) |