Step | Hyp | Ref
| Expression |
1 | | onfin2 9233 |
. . . . 5
β’ Ο =
(On β© Fin) |
2 | | inss2 4228 |
. . . . 5
β’ (On β©
Fin) β Fin |
3 | 1, 2 | eqsstri 4015 |
. . . 4
β’ Ο
β Fin |
4 | | peano2 7883 |
. . . 4
β’ (π΄ β Ο β suc π΄ β
Ο) |
5 | 3, 4 | sselid 3979 |
. . 3
β’ (π΄ β Ο β suc π΄ β Fin) |
6 | 5 | 3ad2ant3 1133 |
. 2
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
suc π΄ β
Fin) |
7 | 4 | 3ad2ant3 1133 |
. . 3
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
suc π΄ β
Ο) |
8 | | breq1 5150 |
. . . . . 6
β’ (π = π β (π βΌ π΄ β π βΌ π΄)) |
9 | 8 | elrab 3682 |
. . . . 5
β’ (π β {π β π β£ π βΌ π΄} β (π β π β§ π βΌ π΄)) |
10 | | simprr 769 |
. . . . . . . 8
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π βΌ π΄) |
11 | | simpl2 1190 |
. . . . . . . . . . 11
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π β Fin) |
12 | | simprl 767 |
. . . . . . . . . . 11
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π β π) |
13 | 11, 12 | sseldd 3982 |
. . . . . . . . . 10
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π β Fin) |
14 | | finnum 9945 |
. . . . . . . . . 10
β’ (π β Fin β π β dom
card) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π β dom card) |
16 | | simpl3 1191 |
. . . . . . . . . . 11
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π΄ β Ο) |
17 | 3, 16 | sselid 3979 |
. . . . . . . . . 10
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π΄ β Fin) |
18 | | finnum 9945 |
. . . . . . . . . 10
β’ (π΄ β Fin β π΄ β dom
card) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β π΄ β dom card) |
20 | | carddom2 9974 |
. . . . . . . . 9
β’ ((π β dom card β§ π΄ β dom card) β
((cardβπ) β
(cardβπ΄) β π βΌ π΄)) |
21 | 15, 19, 20 | syl2anc 582 |
. . . . . . . 8
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β ((cardβπ) β (cardβπ΄) β π βΌ π΄)) |
22 | 10, 21 | mpbird 256 |
. . . . . . 7
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π βΌ π΄)) β (cardβπ) β (cardβπ΄)) |
23 | 22 | ex 411 |
. . . . . 6
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
((π β π β§ π βΌ π΄) β (cardβπ) β (cardβπ΄))) |
24 | | cardnn 9960 |
. . . . . . . . 9
β’ (π΄ β Ο β
(cardβπ΄) = π΄) |
25 | 24 | sseq2d 4013 |
. . . . . . . 8
β’ (π΄ β Ο β
((cardβπ) β
(cardβπ΄) β
(cardβπ) β
π΄)) |
26 | | cardon 9941 |
. . . . . . . . 9
β’
(cardβπ)
β On |
27 | | nnon 7863 |
. . . . . . . . 9
β’ (π΄ β Ο β π΄ β On) |
28 | | onsssuc 6453 |
. . . . . . . . 9
β’
(((cardβπ)
β On β§ π΄ β
On) β ((cardβπ)
β π΄ β
(cardβπ) β suc
π΄)) |
29 | 26, 27, 28 | sylancr 585 |
. . . . . . . 8
β’ (π΄ β Ο β
((cardβπ) β
π΄ β (cardβπ) β suc π΄)) |
30 | 25, 29 | bitrd 278 |
. . . . . . 7
β’ (π΄ β Ο β
((cardβπ) β
(cardβπ΄) β
(cardβπ) β suc
π΄)) |
31 | 30 | 3ad2ant3 1133 |
. . . . . 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 3676 |
. . . . 5
β’ (π β {π β π β£ π βΌ π΄} β π β π) |
35 | | elrabi 3676 |
. . . . 5
β’ (π β {π β π β£ π βΌ π΄} β π β π) |
36 | | ssel 3974 |
. . . . . . . . . . 11
β’ (π β Fin β (π β π β π β Fin)) |
37 | | ssel 3974 |
. . . . . . . . . . 11
β’ (π β Fin β (π β π β π β Fin)) |
38 | 36, 37 | anim12d 607 |
. . . . . . . . . 10
β’ (π β Fin β ((π β π β§ π β π) β (π β Fin β§ π β Fin))) |
39 | 38 | imp 405 |
. . . . . . . . 9
β’ ((π β Fin β§ (π β π β§ π β π)) β (π β Fin β§ π β Fin)) |
40 | 39 | 3ad2antl2 1184 |
. . . . . . . 8
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π β π)) β (π β Fin β§ π β Fin)) |
41 | | sorpssi 7721 |
. . . . . . . . 9
β’ ((
[β] Or π
β§ (π β π β§ π β π)) β (π β π β¨ π β π)) |
42 | 41 | 3ad2antl1 1183 |
. . . . . . . 8
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π β π)) β (π β π β¨ π β π)) |
43 | | finnum 9945 |
. . . . . . . . . . 11
β’ (π β Fin β π β dom
card) |
44 | | carden2 9984 |
. . . . . . . . . . 11
β’ ((π β dom card β§ π β dom card) β
((cardβπ) =
(cardβπ) β π β π)) |
45 | 14, 43, 44 | syl2an 594 |
. . . . . . . . . 10
β’ ((π β Fin β§ π β Fin) β
((cardβπ) =
(cardβπ) β π β π)) |
46 | 45 | adantr 479 |
. . . . . . . . 9
β’ (((π β Fin β§ π β Fin) β§ (π β π β¨ π β π)) β ((cardβπ) = (cardβπ) β π β π)) |
47 | | fin23lem25 10321 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π β Fin β§ (π β π β¨ π β π)) β (π β π β π = π)) |
48 | 47 | 3expa 1116 |
. . . . . . . . . 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 582 |
. . . . . . 7
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π β π)) β ((cardβπ) = (cardβπ) β π = π)) |
52 | | fveq2 6890 |
. . . . . . 7
β’ (π = π β (cardβπ) = (cardβπ)) |
53 | 51, 52 | impbid1 224 |
. . . . . 6
β’ (((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β§
(π β π β§ π β π)) β ((cardβπ) = (cardβπ) β π = π)) |
54 | 53 | ex 411 |
. . . . 5
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
((π β π β§ π β π) β ((cardβπ) = (cardβπ) β π = π))) |
55 | 34, 35, 54 | syl2ani 605 |
. . . 4
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
((π β {π β π β£ π βΌ π΄} β§ π β {π β π β£ π βΌ π΄}) β ((cardβπ) = (cardβπ) β π = π))) |
56 | 33, 55 | dom2d 8991 |
. . 3
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
(suc π΄ β Ο
β {π β π β£ π βΌ π΄} βΌ suc π΄)) |
57 | 7, 56 | mpd 15 |
. 2
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
{π β π β£ π βΌ π΄} βΌ suc π΄) |
58 | | domfi 9194 |
. 2
β’ ((suc
π΄ β Fin β§ {π β π β£ π βΌ π΄} βΌ suc π΄) β {π β π β£ π βΌ π΄} β Fin) |
59 | 6, 57, 58 | syl2anc 582 |
1
β’ ((
[β] Or π
β§ π β Fin β§
π΄ β Ο) β
{π β π β£ π βΌ π΄} β Fin) |