Step | Hyp | Ref
| Expression |
1 | | icccmp.5 |
. . . . 5
β’ (π β π΄ β β) |
2 | 1 | rexrd 11212 |
. . . 4
β’ (π β π΄ β
β*) |
3 | | icccmp.6 |
. . . . 5
β’ (π β π΅ β β) |
4 | 3 | rexrd 11212 |
. . . 4
β’ (π β π΅ β
β*) |
5 | | icccmp.7 |
. . . 4
β’ (π β π΄ β€ π΅) |
6 | | lbicc2 13388 |
. . . 4
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β π΄ β (π΄[,]π΅)) |
7 | 2, 4, 5, 6 | syl3anc 1372 |
. . 3
β’ (π β π΄ β (π΄[,]π΅)) |
8 | | icccmp.9 |
. . . . . 6
β’ (π β (π΄[,]π΅) β βͺ π) |
9 | 8, 7 | sseldd 3950 |
. . . . 5
β’ (π β π΄ β βͺ π) |
10 | | eluni2 4874 |
. . . . 5
β’ (π΄ β βͺ π
β βπ’ β
π π΄ β π’) |
11 | 9, 10 | sylib 217 |
. . . 4
β’ (π β βπ’ β π π΄ β π’) |
12 | | snssi 4773 |
. . . . . . . 8
β’ (π’ β π β {π’} β π) |
13 | 12 | ad2antrl 727 |
. . . . . . 7
β’ ((π β§ (π’ β π β§ π΄ β π’)) β {π’} β π) |
14 | | snex 5393 |
. . . . . . . 8
β’ {π’} β V |
15 | 14 | elpw 4569 |
. . . . . . 7
β’ ({π’} β π« π β {π’} β π) |
16 | 13, 15 | sylibr 233 |
. . . . . 6
β’ ((π β§ (π’ β π β§ π΄ β π’)) β {π’} β π« π) |
17 | | snfi 8995 |
. . . . . . 7
β’ {π’} β Fin |
18 | 17 | a1i 11 |
. . . . . 6
β’ ((π β§ (π’ β π β§ π΄ β π’)) β {π’} β Fin) |
19 | 16, 18 | elind 4159 |
. . . . 5
β’ ((π β§ (π’ β π β§ π΄ β π’)) β {π’} β (π« π β© Fin)) |
20 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π’ β π β§ π΄ β π’)) β π΄ β
β*) |
21 | | iccid 13316 |
. . . . . . 7
β’ (π΄ β β*
β (π΄[,]π΄) = {π΄}) |
22 | 20, 21 | syl 17 |
. . . . . 6
β’ ((π β§ (π’ β π β§ π΄ β π’)) β (π΄[,]π΄) = {π΄}) |
23 | | snssi 4773 |
. . . . . . 7
β’ (π΄ β π’ β {π΄} β π’) |
24 | 23 | ad2antll 728 |
. . . . . 6
β’ ((π β§ (π’ β π β§ π΄ β π’)) β {π΄} β π’) |
25 | 22, 24 | eqsstrd 3987 |
. . . . 5
β’ ((π β§ (π’ β π β§ π΄ β π’)) β (π΄[,]π΄) β π’) |
26 | | unieq 4881 |
. . . . . . . 8
β’ (π§ = {π’} β βͺ π§ = βͺ
{π’}) |
27 | | unisnv 4893 |
. . . . . . . 8
β’ βͺ {π’}
= π’ |
28 | 26, 27 | eqtrdi 2793 |
. . . . . . 7
β’ (π§ = {π’} β βͺ π§ = π’) |
29 | 28 | sseq2d 3981 |
. . . . . 6
β’ (π§ = {π’} β ((π΄[,]π΄) β βͺ π§ β (π΄[,]π΄) β π’)) |
30 | 29 | rspcev 3584 |
. . . . 5
β’ (({π’} β (π« π β© Fin) β§ (π΄[,]π΄) β π’) β βπ§ β (π« π β© Fin)(π΄[,]π΄) β βͺ π§) |
31 | 19, 25, 30 | syl2anc 585 |
. . . 4
β’ ((π β§ (π’ β π β§ π΄ β π’)) β βπ§ β (π« π β© Fin)(π΄[,]π΄) β βͺ π§) |
32 | 11, 31 | rexlimddv 3159 |
. . 3
β’ (π β βπ§ β (π« π β© Fin)(π΄[,]π΄) β βͺ π§) |
33 | | oveq2 7370 |
. . . . . 6
β’ (π₯ = π΄ β (π΄[,]π₯) = (π΄[,]π΄)) |
34 | 33 | sseq1d 3980 |
. . . . 5
β’ (π₯ = π΄ β ((π΄[,]π₯) β βͺ π§ β (π΄[,]π΄) β βͺ π§)) |
35 | 34 | rexbidv 3176 |
. . . 4
β’ (π₯ = π΄ β (βπ§ β (π« π β© Fin)(π΄[,]π₯) β βͺ π§ β βπ§ β (π« π β© Fin)(π΄[,]π΄) β βͺ π§)) |
36 | | icccmp.4 |
. . . 4
β’ π = {π₯ β (π΄[,]π΅) β£ βπ§ β (π« π β© Fin)(π΄[,]π₯) β βͺ π§} |
37 | 35, 36 | elrab2 3653 |
. . 3
β’ (π΄ β π β (π΄ β (π΄[,]π΅) β§ βπ§ β (π« π β© Fin)(π΄[,]π΄) β βͺ π§)) |
38 | 7, 32, 37 | sylanbrc 584 |
. 2
β’ (π β π΄ β π) |
39 | 36 | ssrab3 4045 |
. . . . 5
β’ π β (π΄[,]π΅) |
40 | 39 | sseli 3945 |
. . . 4
β’ (π¦ β π β π¦ β (π΄[,]π΅)) |
41 | | elicc2 13336 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β) β (π¦ β (π΄[,]π΅) β (π¦ β β β§ π΄ β€ π¦ β§ π¦ β€ π΅))) |
42 | 1, 3, 41 | syl2anc 585 |
. . . . . 6
β’ (π β (π¦ β (π΄[,]π΅) β (π¦ β β β§ π΄ β€ π¦ β§ π¦ β€ π΅))) |
43 | 42 | biimpa 478 |
. . . . 5
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π¦ β β β§ π΄ β€ π¦ β§ π¦ β€ π΅)) |
44 | 43 | simp3d 1145 |
. . . 4
β’ ((π β§ π¦ β (π΄[,]π΅)) β π¦ β€ π΅) |
45 | 40, 44 | sylan2 594 |
. . 3
β’ ((π β§ π¦ β π) β π¦ β€ π΅) |
46 | 45 | ralrimiva 3144 |
. 2
β’ (π β βπ¦ β π π¦ β€ π΅) |
47 | 38, 46 | jca 513 |
1
β’ (π β (π΄ β π β§ βπ¦ β π π¦ β€ π΅)) |