Step | Hyp | Ref
| Expression |
1 | | onfin2 9231 |
. . . . 5
β’ Ο =
(On β© Fin) |
2 | | inss2 4230 |
. . . . 5
β’ (On β©
Fin) β Fin |
3 | 1, 2 | eqsstri 4017 |
. . . 4
β’ Ο
β Fin |
4 | | peano2 7881 |
. . . 4
β’ (π΄ β Ο β suc π΄ β
Ο) |
5 | 3, 4 | sselid 3981 |
. . 3
β’ (π΄ β Ο β suc π΄ β Fin) |
6 | 5 | 3ad2ant3 1136 |
. 2
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
suc π΄ β
Fin) |
7 | 4 | 3ad2ant3 1136 |
. . 3
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
suc π΄ β
Ο) |
8 | | breq1 5152 |
. . . . . 6
β’ (π = π β (π βΌ π΄ β π βΌ π΄)) |
9 | 8 | elrab 3684 |
. . . . 5
β’ (π β {π β π β£ π βΌ π΄} β (π β π β§ π βΌ π΄)) |
10 | | simprr 772 |
. . . . . . . 8
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π βΌ π΄) |
11 | | simpl2 1193 |
. . . . . . . . . . 11
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π β Fin) |
12 | | simprl 770 |
. . . . . . . . . . 11
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π β π) |
13 | 11, 12 | sseldd 3984 |
. . . . . . . . . 10
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π β Fin) |
14 | | finnum 9943 |
. . . . . . . . . 10
β’ (π β Fin β π β dom
card) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π β dom card) |
16 | | simpl3 1194 |
. . . . . . . . . . 11
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π΄ β Ο) |
17 | 3, 16 | sselid 3981 |
. . . . . . . . . 10
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π΄ β Fin) |
18 | | finnum 9943 |
. . . . . . . . . 10
β’ (π΄ β Fin β π΄ β dom
card) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π΄ β dom card) |
20 | | carddom2 9972 |
. . . . . . . . 9
β’ ((π β dom card β§ π΄ β dom card) β
((cardβπ) β
(cardβπ΄) β π βΌ π΄)) |
21 | 15, 19, 20 | syl2anc 585 |
. . . . . . . 8
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β ((cardβπ) β (cardβπ΄) β π βΌ π΄)) |
22 | 10, 21 | mpbird 257 |
. . . . . . 7
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β (cardβπ) β (cardβπ΄)) |
23 | 22 | ex 414 |
. . . . . 6
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
((π β π β§ π βΌ π΄) β (cardβπ) β (cardβπ΄))) |
24 | | cardnn 9958 |
. . . . . . . . 9
β’ (π΄ β Ο β
(cardβπ΄) = π΄) |
25 | 24 | sseq2d 4015 |
. . . . . . . 8
β’ (π΄ β Ο β
((cardβπ) β
(cardβπ΄) β
(cardβπ) β
π΄)) |
26 | | cardon 9939 |
. . . . . . . . 9
β’
(cardβπ)
β On |
27 | | nnon 7861 |
. . . . . . . . 9
β’ (π΄ β Ο β π΄ β On) |
28 | | onsssuc 6455 |
. . . . . . . . 9
β’
(((cardβπ)
β On β§ π΄ β
On) β ((cardβπ)
β π΄ β
(cardβπ) β suc
π΄)) |
29 | 26, 27, 28 | sylancr 588 |
. . . . . . . 8
β’ (π΄ β Ο β
((cardβπ) β
π΄ β (cardβπ) β suc π΄)) |
30 | 25, 29 | bitrd 279 |
. . . . . . 7
β’ (π΄ β Ο β
((cardβπ) β
(cardβπ΄) β
(cardβπ) β suc
π΄)) |
31 | 30 | 3ad2ant3 1136 |
. . . . . 6
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
((cardβπ) β
(cardβπ΄) β
(cardβπ) β suc
π΄)) |
32 | 23, 31 | sylibd 238 |
. . . . 5
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
((π β π β§ π βΌ π΄) β (cardβπ) β suc π΄)) |
33 | 9, 32 | biimtrid 241 |
. . . 4
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
(π β {π β π β£ π βΌ π΄} β (cardβπ) β suc π΄)) |
34 | | elrabi 3678 |
. . . . 5
β’ (π β {π β π β£ π βΌ π΄} β π β π) |
35 | | elrabi 3678 |
. . . . 5
β’ (π β {π β π β£ π βΌ π΄} β π β π) |
36 | | ssel 3976 |
. . . . . . . . . . 11
β’ (π β Fin β (π β π β π β Fin)) |
37 | | ssel 3976 |
. . . . . . . . . . 11
β’ (π β Fin β (π β π β π β Fin)) |
38 | 36, 37 | anim12d 610 |
. . . . . . . . . 10
β’ (π β Fin β ((π β π β§ π β π) β (π β Fin β§ π β Fin))) |
39 | 38 | imp 408 |
. . . . . . . . 9
β’ ((π β Fin β§ (π β π β§ π β π)) β (π β Fin β§ π β Fin)) |
40 | 39 | 3ad2antl2 1187 |
. . . . . . . 8
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π β π)) β (π β Fin β§ π β Fin)) |
41 | | sorpssi 7719 |
. . . . . . . . 9
β’ ((
[β] Or π
β§ (π β π β§ π β π)) β (π β π β¨ π β π)) |
42 | 41 | 3ad2antl1 1186 |
. . . . . . . 8
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π β π)) β (π β π β¨ π β π)) |
43 | | finnum 9943 |
. . . . . . . . . . 11
β’ (π β Fin β π β dom
card) |
44 | | carden2 9982 |
. . . . . . . . . . 11
β’ ((π β dom card β§ π β dom card) β
((cardβπ) =
(cardβπ) β π β π)) |
45 | 14, 43, 44 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β Fin β§ π β Fin) β
((cardβπ) =
(cardβπ) β π β π)) |
46 | 45 | adantr 482 |
. . . . . . . . 9
β’ (((π β Fin β§ π β Fin) β§ (π β π β¨ π β π)) β ((cardβπ) = (cardβπ) β π β π)) |
47 | | fin23lem25 10319 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π β Fin β§ (π β π β¨ π β π)) β (π β π β π = π)) |
48 | 47 | 3expa 1119 |
. . . . . . . . . 10
β’ (((π β Fin β§ π β Fin) β§ (π β π β¨ π β π)) β (π β π β π = π)) |
49 | 48 | biimpd 228 |
. . . . . . . . 9
β’ (((π β Fin β§ π β Fin) β§ (π β π β¨ π β π)) β (π β π β π = π)) |
50 | 46, 49 | sylbid 239 |
. . . . . . . 8
β’ (((π β Fin β§ π β Fin) β§ (π β π β¨ π β π)) β ((cardβπ) = (cardβπ) β π = π)) |
51 | 40, 42, 50 | syl2anc 585 |
. . . . . . 7
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π β π)) β ((cardβπ) = (cardβπ) β π = π)) |
52 | | fveq2 6892 |
. . . . . . 7
β’ (π = π β (cardβπ) = (cardβπ)) |
53 | 51, 52 | impbid1 224 |
. . . . . 6
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π β π)) β ((cardβπ) = (cardβπ) β π = π)) |
54 | 53 | ex 414 |
. . . . 5
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
((π β π β§ π β π) β ((cardβπ) = (cardβπ) β π = π))) |
55 | 34, 35, 54 | syl2ani 608 |
. . . 4
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
((π β {π β π β£ π βΌ π΄} β§ π β {π β π β£ π βΌ π΄}) β ((cardβπ) = (cardβπ) β π = π))) |
56 | 33, 55 | dom2d 8989 |
. . 3
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
(suc π΄ β Ο
β {π β π β£ π βΌ π΄} βΌ suc π΄)) |
57 | 7, 56 | mpd 15 |
. 2
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
{π β π β£ π βΌ π΄} βΌ suc π΄) |
58 | | domfi 9192 |
. 2
β’ ((suc
π΄ β Fin β§ {π β π β£ π βΌ π΄} βΌ suc π΄) β {π β π β£ π βΌ π΄} β Fin) |
59 | 6, 57, 58 | syl2anc 585 |
1
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
{π β π β£ π βΌ π΄} β Fin) |