Step | Hyp | Ref
| Expression |
1 | | icccmp.2 |
. 2
β’ π = (π½ βΎt (π΄[,]π΅)) |
2 | | icccmp.1 |
. . . . . . . 8
β’ π½ = (topGenβran
(,)) |
3 | | eqid 2733 |
. . . . . . . 8
β’ ((abs
β β ) βΎ (β Γ β)) = ((abs β β )
βΎ (β Γ β)) |
4 | | eqid 2733 |
. . . . . . . 8
β’ {π₯ β (π΄[,]π΅) β£ βπ§ β (π« π’ β© Fin)(π΄[,]π₯) β βͺ π§} = {π₯ β (π΄[,]π΅) β£ βπ§ β (π« π’ β© Fin)(π΄[,]π₯) β βͺ π§} |
5 | | simplll 774 |
. . . . . . . 8
β’ ((((π΄ β β β§ π΅ β β) β§ π΄ β€ π΅) β§ (π’ β π« π½ β§ (π΄[,]π΅) β βͺ π’)) β π΄ β β) |
6 | | simpllr 775 |
. . . . . . . 8
β’ ((((π΄ β β β§ π΅ β β) β§ π΄ β€ π΅) β§ (π’ β π« π½ β§ (π΄[,]π΅) β βͺ π’)) β π΅ β β) |
7 | | simplr 768 |
. . . . . . . 8
β’ ((((π΄ β β β§ π΅ β β) β§ π΄ β€ π΅) β§ (π’ β π« π½ β§ (π΄[,]π΅) β βͺ π’)) β π΄ β€ π΅) |
8 | | elpwi 4571 |
. . . . . . . . 9
β’ (π’ β π« π½ β π’ β π½) |
9 | 8 | ad2antrl 727 |
. . . . . . . 8
β’ ((((π΄ β β β§ π΅ β β) β§ π΄ β€ π΅) β§ (π’ β π« π½ β§ (π΄[,]π΅) β βͺ π’)) β π’ β π½) |
10 | | simprr 772 |
. . . . . . . 8
β’ ((((π΄ β β β§ π΅ β β) β§ π΄ β€ π΅) β§ (π’ β π« π½ β§ (π΄[,]π΅) β βͺ π’)) β (π΄[,]π΅) β βͺ π’) |
11 | 2, 1, 3, 4, 5, 6, 7, 9, 10 | icccmplem3 24210 |
. . . . . . 7
β’ ((((π΄ β β β§ π΅ β β) β§ π΄ β€ π΅) β§ (π’ β π« π½ β§ (π΄[,]π΅) β βͺ π’)) β π΅ β {π₯ β (π΄[,]π΅) β£ βπ§ β (π« π’ β© Fin)(π΄[,]π₯) β βͺ π§}) |
12 | | oveq2 7369 |
. . . . . . . . . . 11
β’ (π₯ = π΅ β (π΄[,]π₯) = (π΄[,]π΅)) |
13 | 12 | sseq1d 3979 |
. . . . . . . . . 10
β’ (π₯ = π΅ β ((π΄[,]π₯) β βͺ π§ β (π΄[,]π΅) β βͺ π§)) |
14 | 13 | rexbidv 3172 |
. . . . . . . . 9
β’ (π₯ = π΅ β (βπ§ β (π« π’ β© Fin)(π΄[,]π₯) β βͺ π§ β βπ§ β (π« π’ β© Fin)(π΄[,]π΅) β βͺ π§)) |
15 | 14 | elrab 3649 |
. . . . . . . 8
β’ (π΅ β {π₯ β (π΄[,]π΅) β£ βπ§ β (π« π’ β© Fin)(π΄[,]π₯) β βͺ π§} β (π΅ β (π΄[,]π΅) β§ βπ§ β (π« π’ β© Fin)(π΄[,]π΅) β βͺ π§)) |
16 | 15 | simprbi 498 |
. . . . . . 7
β’ (π΅ β {π₯ β (π΄[,]π΅) β£ βπ§ β (π« π’ β© Fin)(π΄[,]π₯) β βͺ π§} β βπ§ β (π« π’ β© Fin)(π΄[,]π΅) β βͺ π§) |
17 | 11, 16 | syl 17 |
. . . . . 6
β’ ((((π΄ β β β§ π΅ β β) β§ π΄ β€ π΅) β§ (π’ β π« π½ β§ (π΄[,]π΅) β βͺ π’)) β βπ§ β (π« π’ β© Fin)(π΄[,]π΅) β βͺ π§) |
18 | 17 | expr 458 |
. . . . 5
β’ ((((π΄ β β β§ π΅ β β) β§ π΄ β€ π΅) β§ π’ β π« π½) β ((π΄[,]π΅) β βͺ π’ β βπ§ β (π« π’ β© Fin)(π΄[,]π΅) β βͺ π§)) |
19 | 18 | ralrimiva 3140 |
. . . 4
β’ (((π΄ β β β§ π΅ β β) β§ π΄ β€ π΅) β βπ’ β π« π½((π΄[,]π΅) β βͺ π’ β βπ§ β (π« π’ β© Fin)(π΄[,]π΅) β βͺ π§)) |
20 | | retop 24148 |
. . . . . 6
β’
(topGenβran (,)) β Top |
21 | 2, 20 | eqeltri 2830 |
. . . . 5
β’ π½ β Top |
22 | | iccssre 13355 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
23 | 22 | adantr 482 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β) β§ π΄ β€ π΅) β (π΄[,]π΅) β β) |
24 | | uniretop 24149 |
. . . . . . 7
β’ β =
βͺ (topGenβran (,)) |
25 | 2 | unieqi 4882 |
. . . . . . 7
β’ βͺ π½ =
βͺ (topGenβran (,)) |
26 | 24, 25 | eqtr4i 2764 |
. . . . . 6
β’ β =
βͺ π½ |
27 | 26 | cmpsub 22774 |
. . . . 5
β’ ((π½ β Top β§ (π΄[,]π΅) β β) β ((π½ βΎt (π΄[,]π΅)) β Comp β βπ’ β π« π½((π΄[,]π΅) β βͺ π’ β βπ§ β (π« π’ β© Fin)(π΄[,]π΅) β βͺ π§))) |
28 | 21, 23, 27 | sylancr 588 |
. . . 4
β’ (((π΄ β β β§ π΅ β β) β§ π΄ β€ π΅) β ((π½ βΎt (π΄[,]π΅)) β Comp β βπ’ β π« π½((π΄[,]π΅) β βͺ π’ β βπ§ β (π« π’ β© Fin)(π΄[,]π΅) β βͺ π§))) |
29 | 19, 28 | mpbird 257 |
. . 3
β’ (((π΄ β β β§ π΅ β β) β§ π΄ β€ π΅) β (π½ βΎt (π΄[,]π΅)) β Comp) |
30 | | rexr 11209 |
. . . . . . . 8
β’ (π΄ β β β π΄ β
β*) |
31 | | rexr 11209 |
. . . . . . . 8
β’ (π΅ β β β π΅ β
β*) |
32 | | icc0 13321 |
. . . . . . . 8
β’ ((π΄ β β*
β§ π΅ β
β*) β ((π΄[,]π΅) = β
β π΅ < π΄)) |
33 | 30, 31, 32 | syl2an 597 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β) β ((π΄[,]π΅) = β
β π΅ < π΄)) |
34 | 33 | biimpar 479 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β β) β§ π΅ < π΄) β (π΄[,]π΅) = β
) |
35 | 34 | oveq2d 7377 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β) β§ π΅ < π΄) β (π½ βΎt (π΄[,]π΅)) = (π½ βΎt
β
)) |
36 | | rest0 22543 |
. . . . . 6
β’ (π½ β Top β (π½ βΎt β
) =
{β
}) |
37 | 21, 36 | ax-mp 5 |
. . . . 5
β’ (π½ βΎt β
) =
{β
} |
38 | 35, 37 | eqtrdi 2789 |
. . . 4
β’ (((π΄ β β β§ π΅ β β) β§ π΅ < π΄) β (π½ βΎt (π΄[,]π΅)) = {β
}) |
39 | | 0cmp 22768 |
. . . 4
β’ {β
}
β Comp |
40 | 38, 39 | eqeltrdi 2842 |
. . 3
β’ (((π΄ β β β§ π΅ β β) β§ π΅ < π΄) β (π½ βΎt (π΄[,]π΅)) β Comp) |
41 | | lelttric 11270 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β (π΄ β€ π΅ β¨ π΅ < π΄)) |
42 | 29, 40, 41 | mpjaodan 958 |
. 2
β’ ((π΄ β β β§ π΅ β β) β (π½ βΎt (π΄[,]π΅)) β Comp) |
43 | 1, 42 | eqeltrid 2838 |
1
β’ ((π΄ β β β§ π΅ β β) β π β Comp) |