Step | Hyp | Ref
| Expression |
1 | | unissb 4936 |
. . 3
β’ (βͺ ran π
β (β Γ β) β
βπ β ran π
π β (β Γ
β)) |
2 | | dya2ioc.2 |
. . . . 5
β’ π
= (π’ β ran πΌ, π£ β ran πΌ β¦ (π’ Γ π£)) |
3 | | vex 3472 |
. . . . . 6
β’ π’ β V |
4 | | vex 3472 |
. . . . . 6
β’ π£ β V |
5 | 3, 4 | xpex 7737 |
. . . . 5
β’ (π’ Γ π£) β V |
6 | 2, 5 | elrnmpo 7541 |
. . . 4
β’ (π β ran π
β βπ’ β ran πΌβπ£ β ran πΌ π = (π’ Γ π£)) |
7 | | simpr 484 |
. . . . . . 7
β’ (((π’ β ran πΌ β§ π£ β ran πΌ) β§ π = (π’ Γ π£)) β π = (π’ Γ π£)) |
8 | | pwssb 5097 |
. . . . . . . . . . . 12
β’ (ran
πΌ β π« β
β βπ β ran
πΌ π β β) |
9 | | dya2ioc.1 |
. . . . . . . . . . . . . 14
β’ πΌ = (π₯ β β€, π β β€ β¦ ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) |
10 | | ovex 7438 |
. . . . . . . . . . . . . 14
β’ ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ))) β V |
11 | 9, 10 | elrnmpo 7541 |
. . . . . . . . . . . . 13
β’ (π β ran πΌ β βπ₯ β β€ βπ β β€ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) |
12 | | simpr 484 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) |
13 | | simpll 764 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β π₯ β β€) |
14 | 13 | zred 12670 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β π₯ β β) |
15 | | 2re 12290 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
β |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β 2 β
β) |
17 | | 2ne0 12320 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
0 |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β 2 β 0) |
19 | | simplr 766 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β π β β€) |
20 | 16, 18, 19 | reexpclzd 14217 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β (2βπ) β β) |
21 | | 2cnd 12294 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β 2 β
β) |
22 | 21, 18, 19 | expne0d 14122 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β (2βπ) β 0) |
23 | 14, 20, 22 | redivcld 12046 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β (π₯ / (2βπ)) β β) |
24 | | 1red 11219 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β 1 β
β) |
25 | 14, 24 | readdcld 11247 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β (π₯ + 1) β β) |
26 | 25, 20, 22 | redivcld 12046 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β ((π₯ + 1) / (2βπ)) β β) |
27 | 26 | rexrd 11268 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β ((π₯ + 1) / (2βπ)) β
β*) |
28 | | icossre 13411 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ / (2βπ)) β β β§ ((π₯ + 1) / (2βπ)) β β*) β ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ))) β β) |
29 | 23, 27, 28 | syl2anc 583 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ))) β β) |
30 | 12, 29 | eqsstrd 4015 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β€ β§ π β β€) β§ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ)))) β π β β) |
31 | 30 | ex 412 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β€ β§ π β β€) β (π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ))) β π β β)) |
32 | 31 | rexlimivv 3193 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
β€ βπ β
β€ π = ((π₯ / (2βπ))[,)((π₯ + 1) / (2βπ))) β π β β) |
33 | 11, 32 | sylbi 216 |
. . . . . . . . . . . 12
β’ (π β ran πΌ β π β β) |
34 | 8, 33 | mprgbir 3062 |
. . . . . . . . . . 11
β’ ran πΌ β π«
β |
35 | 34 | sseli 3973 |
. . . . . . . . . 10
β’ (π’ β ran πΌ β π’ β π« β) |
36 | 35 | elpwid 4606 |
. . . . . . . . 9
β’ (π’ β ran πΌ β π’ β β) |
37 | 34 | sseli 3973 |
. . . . . . . . . 10
β’ (π£ β ran πΌ β π£ β π« β) |
38 | 37 | elpwid 4606 |
. . . . . . . . 9
β’ (π£ β ran πΌ β π£ β β) |
39 | | xpss12 5684 |
. . . . . . . . 9
β’ ((π’ β β β§ π£ β β) β (π’ Γ π£) β (β Γ
β)) |
40 | 36, 38, 39 | syl2an 595 |
. . . . . . . 8
β’ ((π’ β ran πΌ β§ π£ β ran πΌ) β (π’ Γ π£) β (β Γ
β)) |
41 | 40 | adantr 480 |
. . . . . . 7
β’ (((π’ β ran πΌ β§ π£ β ran πΌ) β§ π = (π’ Γ π£)) β (π’ Γ π£) β (β Γ
β)) |
42 | 7, 41 | eqsstrd 4015 |
. . . . . 6
β’ (((π’ β ran πΌ β§ π£ β ran πΌ) β§ π = (π’ Γ π£)) β π β (β Γ
β)) |
43 | 42 | ex 412 |
. . . . 5
β’ ((π’ β ran πΌ β§ π£ β ran πΌ) β (π = (π’ Γ π£) β π β (β Γ
β))) |
44 | 43 | rexlimivv 3193 |
. . . 4
β’
(βπ’ β ran
πΌβπ£ β ran πΌ π = (π’ Γ π£) β π β (β Γ
β)) |
45 | 6, 44 | sylbi 216 |
. . 3
β’ (π β ran π
β π β (β Γ
β)) |
46 | 1, 45 | mprgbir 3062 |
. 2
β’ βͺ ran π
β (β Γ
β) |
47 | | sxbrsiga.0 |
. . . . . 6
β’ π½ = (topGenβran
(,)) |
48 | | retop 24633 |
. . . . . 6
β’
(topGenβran (,)) β Top |
49 | 47, 48 | eqeltri 2823 |
. . . . 5
β’ π½ β Top |
50 | 49, 49 | txtopi 23449 |
. . . 4
β’ (π½ Γt π½) β Top |
51 | | uniretop 24634 |
. . . . . . 7
β’ β =
βͺ (topGenβran (,)) |
52 | 47 | unieqi 4914 |
. . . . . . 7
β’ βͺ π½ =
βͺ (topGenβran (,)) |
53 | 51, 52 | eqtr4i 2757 |
. . . . . 6
β’ β =
βͺ π½ |
54 | 49, 49, 53, 53 | txunii 23452 |
. . . . 5
β’ (β
Γ β) = βͺ (π½ Γt π½) |
55 | 54 | topopn 22763 |
. . . 4
β’ ((π½ Γt π½) β Top β (β
Γ β) β (π½
Γt π½)) |
56 | 47, 9, 2 | dya2iocuni 33812 |
. . . 4
β’ ((β
Γ β) β (π½
Γt π½)
β βπ β
π« ran π
βͺ π =
(β Γ β)) |
57 | 50, 55, 56 | mp2b 10 |
. . 3
β’
βπ β
π« ran π
βͺ π =
(β Γ β) |
58 | | simpr 484 |
. . . . 5
β’ ((π β π« ran π
β§ βͺ π =
(β Γ β)) β βͺ π = (β Γ
β)) |
59 | | elpwi 4604 |
. . . . . . 7
β’ (π β π« ran π
β π β ran π
) |
60 | 59 | adantr 480 |
. . . . . 6
β’ ((π β π« ran π
β§ βͺ π =
(β Γ β)) β π β ran π
) |
61 | 60 | unissd 4912 |
. . . . 5
β’ ((π β π« ran π
β§ βͺ π =
(β Γ β)) β βͺ π β βͺ ran π
) |
62 | 58, 61 | eqsstrrd 4016 |
. . . 4
β’ ((π β π« ran π
β§ βͺ π =
(β Γ β)) β (β Γ β) β βͺ ran π
) |
63 | 62 | rexlimiva 3141 |
. . 3
β’
(βπ β
π« ran π
βͺ π =
(β Γ β) β (β Γ β) β βͺ ran π
) |
64 | 57, 63 | ax-mp 5 |
. 2
β’ (β
Γ β) β βͺ ran π
|
65 | 46, 64 | eqssi 3993 |
1
β’ βͺ ran π
= (β Γ
β) |