Step | Hyp | Ref
| Expression |
1 | | elex 3464 |
. . 3
β’ (πΆ β π΄ β πΆ β V) |
2 | 1 | a1i 11 |
. 2
β’ (π β (πΆ β π΄ β πΆ β V)) |
3 | | id 22 |
. . . . 5
β’
((π« πΆ β©
Fin) β π΄ β
(π« πΆ β© Fin)
β π΄) |
4 | | ssun1 4133 |
. . . . . . . 8
β’ βͺ π΄
β (βͺ π΄ βͺ π΅) |
5 | | undif1 4436 |
. . . . . . . 8
β’ ((βͺ π΄
β π΅) βͺ π΅) = (βͺ π΄
βͺ π΅) |
6 | 4, 5 | sseqtrri 3982 |
. . . . . . 7
β’ βͺ π΄
β ((βͺ π΄ β π΅) βͺ π΅) |
7 | | fvex 6856 |
. . . . . . . . 9
β’
(cardβ(βͺ π΄ β π΅)) β V |
8 | | ttukeylem.1 |
. . . . . . . . . 10
β’ (π β πΉ:(cardβ(βͺ
π΄ β π΅))β1-1-ontoβ(βͺ π΄ β π΅)) |
9 | | f1ofo 6792 |
. . . . . . . . . 10
β’ (πΉ:(cardβ(βͺ π΄
β π΅))β1-1-ontoβ(βͺ π΄ β π΅) β πΉ:(cardβ(βͺ
π΄ β π΅))βontoβ(βͺ π΄ β π΅)) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
β’ (π β πΉ:(cardβ(βͺ
π΄ β π΅))βontoβ(βͺ π΄ β π΅)) |
11 | | focdmex 7889 |
. . . . . . . . 9
β’
((cardβ(βͺ π΄ β π΅)) β V β (πΉ:(cardβ(βͺ
π΄ β π΅))βontoβ(βͺ π΄ β π΅) β (βͺ π΄ β π΅) β V)) |
12 | 7, 10, 11 | mpsyl 68 |
. . . . . . . 8
β’ (π β (βͺ π΄
β π΅) β
V) |
13 | | ttukeylem.2 |
. . . . . . . 8
β’ (π β π΅ β π΄) |
14 | | unexg 7684 |
. . . . . . . 8
β’ (((βͺ π΄
β π΅) β V β§
π΅ β π΄) β ((βͺ
π΄ β π΅) βͺ π΅) β V) |
15 | 12, 13, 14 | syl2anc 585 |
. . . . . . 7
β’ (π β ((βͺ π΄
β π΅) βͺ π΅) β V) |
16 | | ssexg 5281 |
. . . . . . 7
β’ ((βͺ π΄
β ((βͺ π΄ β π΅) βͺ π΅) β§ ((βͺ π΄ β π΅) βͺ π΅) β V) β βͺ π΄
β V) |
17 | 6, 15, 16 | sylancr 588 |
. . . . . 6
β’ (π β βͺ π΄
β V) |
18 | | uniexb 7699 |
. . . . . 6
β’ (π΄ β V β βͺ π΄
β V) |
19 | 17, 18 | sylibr 233 |
. . . . 5
β’ (π β π΄ β V) |
20 | | ssexg 5281 |
. . . . 5
β’
(((π« πΆ β©
Fin) β π΄ β§ π΄ β V) β (π«
πΆ β© Fin) β
V) |
21 | 3, 19, 20 | syl2anr 598 |
. . . 4
β’ ((π β§ (π« πΆ β© Fin) β π΄) β (π« πΆ β© Fin) β
V) |
22 | | infpwfidom 9965 |
. . . 4
β’
((π« πΆ β©
Fin) β V β πΆ
βΌ (π« πΆ β©
Fin)) |
23 | | reldom 8890 |
. . . . 5
β’ Rel
βΌ |
24 | 23 | brrelex1i 5689 |
. . . 4
β’ (πΆ βΌ (π« πΆ β© Fin) β πΆ β V) |
25 | 21, 22, 24 | 3syl 18 |
. . 3
β’ ((π β§ (π« πΆ β© Fin) β π΄) β πΆ β V) |
26 | 25 | ex 414 |
. 2
β’ (π β ((π« πΆ β© Fin) β π΄ β πΆ β V)) |
27 | | ttukeylem.3 |
. . 3
β’ (π β βπ₯(π₯ β π΄ β (π« π₯ β© Fin) β π΄)) |
28 | | eleq1 2826 |
. . . . 5
β’ (π₯ = πΆ β (π₯ β π΄ β πΆ β π΄)) |
29 | | pweq 4575 |
. . . . . . 7
β’ (π₯ = πΆ β π« π₯ = π« πΆ) |
30 | 29 | ineq1d 4172 |
. . . . . 6
β’ (π₯ = πΆ β (π« π₯ β© Fin) = (π« πΆ β© Fin)) |
31 | 30 | sseq1d 3976 |
. . . . 5
β’ (π₯ = πΆ β ((π« π₯ β© Fin) β π΄ β (π« πΆ β© Fin) β π΄)) |
32 | 28, 31 | bibi12d 346 |
. . . 4
β’ (π₯ = πΆ β ((π₯ β π΄ β (π« π₯ β© Fin) β π΄) β (πΆ β π΄ β (π« πΆ β© Fin) β π΄))) |
33 | 32 | spcgv 3556 |
. . 3
β’ (πΆ β V β (βπ₯(π₯ β π΄ β (π« π₯ β© Fin) β π΄) β (πΆ β π΄ β (π« πΆ β© Fin) β π΄))) |
34 | 27, 33 | syl5com 31 |
. 2
β’ (π β (πΆ β V β (πΆ β π΄ β (π« πΆ β© Fin) β π΄))) |
35 | 2, 26, 34 | pm5.21ndd 381 |
1
β’ (π β (πΆ β π΄ β (π« πΆ β© Fin) β π΄)) |