Step | Hyp | Ref
| Expression |
1 | | infxpidm2 9960 |
. . . . . . 7
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β (π΄ Γ π΄) β π΄) |
2 | | infn0 9258 |
. . . . . . . 8
β’ (Ο
βΌ π΄ β π΄ β β
) |
3 | 2 | adantl 483 |
. . . . . . 7
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β π΄ β β
) |
4 | | fseqen 9970 |
. . . . . . 7
β’ (((π΄ Γ π΄) β π΄ β§ π΄ β β
) β βͺ π β Ο (π΄ βm π) β (Ο Γ π΄)) |
5 | 1, 3, 4 | syl2anc 585 |
. . . . . 6
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β βͺ π β Ο (π΄ βm π) β (Ο Γ π΄)) |
6 | | xpdom1g 9020 |
. . . . . . 7
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β (Ο
Γ π΄) βΌ (π΄ Γ π΄)) |
7 | | domentr 8960 |
. . . . . . 7
β’
(((Ο Γ π΄) βΌ (π΄ Γ π΄) β§ (π΄ Γ π΄) β π΄) β (Ο Γ π΄) βΌ π΄) |
8 | 6, 1, 7 | syl2anc 585 |
. . . . . 6
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β (Ο
Γ π΄) βΌ π΄) |
9 | | endomtr 8959 |
. . . . . 6
β’
((βͺ π β Ο (π΄ βm π) β (Ο Γ π΄) β§ (Ο Γ π΄) βΌ π΄) β βͺ
π β Ο (π΄ βm π) βΌ π΄) |
10 | 5, 8, 9 | syl2anc 585 |
. . . . 5
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β βͺ π β Ο (π΄ βm π) βΌ π΄) |
11 | | numdom 9981 |
. . . . 5
β’ ((π΄ β dom card β§ βͺ π β Ο (π΄ βm π) βΌ π΄) β βͺ
π β Ο (π΄ βm π) β dom
card) |
12 | 10, 11 | syldan 592 |
. . . 4
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β βͺ π β Ο (π΄ βm π) β dom card) |
13 | | eliun 4963 |
. . . . . . . . 9
β’ (π₯ β βͺ π β Ο (π΄ βm π) β βπ β Ο π₯ β (π΄ βm π)) |
14 | | elmapi 8794 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (π΄ βm π) β π₯:πβΆπ΄) |
15 | 14 | ad2antll 728 |
. . . . . . . . . . . . . 14
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ (π β Ο β§ π₯ β (π΄ βm π))) β π₯:πβΆπ΄) |
16 | 15 | frnd 6681 |
. . . . . . . . . . . . 13
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ (π β Ο β§ π₯ β (π΄ βm π))) β ran π₯ β π΄) |
17 | | vex 3452 |
. . . . . . . . . . . . . . 15
β’ π₯ β V |
18 | 17 | rnex 7854 |
. . . . . . . . . . . . . 14
β’ ran π₯ β V |
19 | 18 | elpw 4569 |
. . . . . . . . . . . . 13
β’ (ran
π₯ β π« π΄ β ran π₯ β π΄) |
20 | 16, 19 | sylibr 233 |
. . . . . . . . . . . 12
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ (π β Ο β§ π₯ β (π΄ βm π))) β ran π₯ β π« π΄) |
21 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ (π β Ο β§ π₯ β (π΄ βm π))) β π β Ο) |
22 | | ssid 3971 |
. . . . . . . . . . . . . 14
β’ π β π |
23 | | ssnnfi 9120 |
. . . . . . . . . . . . . 14
β’ ((π β Ο β§ π β π) β π β Fin) |
24 | 21, 22, 23 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ (π β Ο β§ π₯ β (π΄ βm π))) β π β Fin) |
25 | | ffn 6673 |
. . . . . . . . . . . . . . 15
β’ (π₯:πβΆπ΄ β π₯ Fn π) |
26 | | dffn4 6767 |
. . . . . . . . . . . . . . 15
β’ (π₯ Fn π β π₯:πβontoβran π₯) |
27 | 25, 26 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (π₯:πβΆπ΄ β π₯:πβontoβran π₯) |
28 | 15, 27 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ (π β Ο β§ π₯ β (π΄ βm π))) β π₯:πβontoβran π₯) |
29 | | fofi 9289 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π₯:πβontoβran π₯) β ran π₯ β Fin) |
30 | 24, 28, 29 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ (π β Ο β§ π₯ β (π΄ βm π))) β ran π₯ β Fin) |
31 | 20, 30 | elind 4159 |
. . . . . . . . . . 11
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ (π β Ο β§ π₯ β (π΄ βm π))) β ran π₯ β (π« π΄ β© Fin)) |
32 | 31 | expr 458 |
. . . . . . . . . 10
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ π β Ο) β (π₯ β (π΄ βm π) β ran π₯ β (π« π΄ β© Fin))) |
33 | 32 | rexlimdva 3153 |
. . . . . . . . 9
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β
(βπ β Ο
π₯ β (π΄ βm π) β ran π₯ β (π« π΄ β© Fin))) |
34 | 13, 33 | biimtrid 241 |
. . . . . . . 8
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β (π₯ β βͺ π β Ο (π΄ βm π) β ran π₯ β (π« π΄ β© Fin))) |
35 | 34 | imp 408 |
. . . . . . 7
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ π₯ β βͺ π β Ο (π΄ βm π)) β ran π₯ β (π« π΄ β© Fin)) |
36 | 35 | fmpttd 7068 |
. . . . . 6
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β (π₯ β βͺ π β Ο (π΄ βm π) β¦ ran π₯):βͺ π β Ο (π΄ βm π)βΆ(π« π΄ β© Fin)) |
37 | 36 | ffnd 6674 |
. . . . 5
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β (π₯ β βͺ π β Ο (π΄ βm π) β¦ ran π₯) Fn βͺ
π β Ο (π΄ βm π)) |
38 | 36 | frnd 6681 |
. . . . . 6
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β ran
(π₯ β βͺ π β Ο (π΄ βm π) β¦ ran π₯) β (π« π΄ β© Fin)) |
39 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β π¦ β (π« π΄ β© Fin)) |
40 | 39 | elin2d 4164 |
. . . . . . . . . . 11
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β π¦ β Fin) |
41 | | isfi 8923 |
. . . . . . . . . . 11
β’ (π¦ β Fin β βπ β Ο π¦ β π) |
42 | 40, 41 | sylib 217 |
. . . . . . . . . 10
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β βπ β Ο π¦ β π) |
43 | | ensym 8950 |
. . . . . . . . . . . . 13
β’ (π¦ β π β π β π¦) |
44 | | bren 8900 |
. . . . . . . . . . . . 13
β’ (π β π¦ β βπ₯ π₯:πβ1-1-ontoβπ¦) |
45 | 43, 44 | sylib 217 |
. . . . . . . . . . . 12
β’ (π¦ β π β βπ₯ π₯:πβ1-1-ontoβπ¦) |
46 | | simprl 770 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ (π β Ο β§ π₯:πβ1-1-ontoβπ¦)) β π β Ο) |
47 | | f1of 6789 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯:πβ1-1-ontoβπ¦ β π₯:πβΆπ¦) |
48 | 47 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ (π β Ο β§ π₯:πβ1-1-ontoβπ¦)) β π₯:πβΆπ¦) |
49 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ (π β Ο β§ π₯:πβ1-1-ontoβπ¦)) β π¦ β (π« π΄ β© Fin)) |
50 | 49 | elin1d 4163 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ (π β Ο β§ π₯:πβ1-1-ontoβπ¦)) β π¦ β π« π΄) |
51 | 50 | elpwid 4574 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ (π β Ο β§ π₯:πβ1-1-ontoβπ¦)) β π¦ β π΄) |
52 | 48, 51 | fssd 6691 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ (π β Ο β§ π₯:πβ1-1-ontoβπ¦)) β π₯:πβΆπ΄) |
53 | | simplll 774 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ (π β Ο β§ π₯:πβ1-1-ontoβπ¦)) β π΄ β dom card) |
54 | | vex 3452 |
. . . . . . . . . . . . . . . . . . 19
β’ π β V |
55 | | elmapg 8785 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β dom card β§ π β V) β (π₯ β (π΄ βm π) β π₯:πβΆπ΄)) |
56 | 53, 54, 55 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ (π β Ο β§ π₯:πβ1-1-ontoβπ¦)) β (π₯ β (π΄ βm π) β π₯:πβΆπ΄)) |
57 | 52, 56 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ (π β Ο β§ π₯:πβ1-1-ontoβπ¦)) β π₯ β (π΄ βm π)) |
58 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (π΄ βm π) = (π΄ βm π)) |
59 | 58 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π₯ β (π΄ βm π) β π₯ β (π΄ βm π))) |
60 | 59 | rspcev 3584 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Ο β§ π₯ β (π΄ βm π)) β βπ β Ο π₯ β (π΄ βm π)) |
61 | 46, 57, 60 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ (π β Ο β§ π₯:πβ1-1-ontoβπ¦)) β βπ β Ο π₯ β (π΄ βm π)) |
62 | 61, 13 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ (π β Ο β§ π₯:πβ1-1-ontoβπ¦)) β π₯ β βͺ
π β Ο (π΄ βm π)) |
63 | | f1ofo 6796 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯:πβ1-1-ontoβπ¦ β π₯:πβontoβπ¦) |
64 | 63 | ad2antll 728 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ (π β Ο β§ π₯:πβ1-1-ontoβπ¦)) β π₯:πβontoβπ¦) |
65 | | forn 6764 |
. . . . . . . . . . . . . . . . 17
β’ (π₯:πβontoβπ¦ β ran π₯ = π¦) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ (π β Ο β§ π₯:πβ1-1-ontoβπ¦)) β ran π₯ = π¦) |
67 | 66 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ (π β Ο β§ π₯:πβ1-1-ontoβπ¦)) β π¦ = ran π₯) |
68 | 62, 67 | jca 513 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ (π β Ο β§ π₯:πβ1-1-ontoβπ¦)) β (π₯ β βͺ
π β Ο (π΄ βm π) β§ π¦ = ran π₯)) |
69 | 68 | expr 458 |
. . . . . . . . . . . . 13
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ π β Ο) β (π₯:πβ1-1-ontoβπ¦ β (π₯ β βͺ
π β Ο (π΄ βm π) β§ π¦ = ran π₯))) |
70 | 69 | eximdv 1921 |
. . . . . . . . . . . 12
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ π β Ο) β
(βπ₯ π₯:πβ1-1-ontoβπ¦ β βπ₯(π₯ β βͺ
π β Ο (π΄ βm π) β§ π¦ = ran π₯))) |
71 | 45, 70 | syl5 34 |
. . . . . . . . . . 11
β’ ((((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β§ π β Ο) β (π¦ β π β βπ₯(π₯ β βͺ
π β Ο (π΄ βm π) β§ π¦ = ran π₯))) |
72 | 71 | rexlimdva 3153 |
. . . . . . . . . 10
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β
(βπ β Ο
π¦ β π β βπ₯(π₯ β βͺ
π β Ο (π΄ βm π) β§ π¦ = ran π₯))) |
73 | 42, 72 | mpd 15 |
. . . . . . . . 9
β’ (((π΄ β dom card β§ Ο
βΌ π΄) β§ π¦ β (π« π΄ β© Fin)) β βπ₯(π₯ β βͺ
π β Ο (π΄ βm π) β§ π¦ = ran π₯)) |
74 | 73 | ex 414 |
. . . . . . . 8
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β (π¦ β (π« π΄ β© Fin) β βπ₯(π₯ β βͺ
π β Ο (π΄ βm π) β§ π¦ = ran π₯))) |
75 | | eqid 2737 |
. . . . . . . . . . 11
β’ (π₯ β βͺ π β Ο (π΄ βm π) β¦ ran π₯) = (π₯ β βͺ
π β Ο (π΄ βm π) β¦ ran π₯) |
76 | 75 | elrnmpt 5916 |
. . . . . . . . . 10
β’ (π¦ β V β (π¦ β ran (π₯ β βͺ
π β Ο (π΄ βm π) β¦ ran π₯) β βπ₯ β βͺ
π β Ο (π΄ βm π)π¦ = ran π₯)) |
77 | 76 | elv 3454 |
. . . . . . . . 9
β’ (π¦ β ran (π₯ β βͺ
π β Ο (π΄ βm π) β¦ ran π₯) β βπ₯ β βͺ
π β Ο (π΄ βm π)π¦ = ran π₯) |
78 | | df-rex 3075 |
. . . . . . . . 9
β’
(βπ₯ β
βͺ π β Ο (π΄ βm π)π¦ = ran π₯ β βπ₯(π₯ β βͺ
π β Ο (π΄ βm π) β§ π¦ = ran π₯)) |
79 | 77, 78 | bitri 275 |
. . . . . . . 8
β’ (π¦ β ran (π₯ β βͺ
π β Ο (π΄ βm π) β¦ ran π₯) β βπ₯(π₯ β βͺ
π β Ο (π΄ βm π) β§ π¦ = ran π₯)) |
80 | 74, 79 | syl6ibr 252 |
. . . . . . 7
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β (π¦ β (π« π΄ β© Fin) β π¦ β ran (π₯ β βͺ
π β Ο (π΄ βm π) β¦ ran π₯))) |
81 | 80 | ssrdv 3955 |
. . . . . 6
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β
(π« π΄ β© Fin)
β ran (π₯ β
βͺ π β Ο (π΄ βm π) β¦ ran π₯)) |
82 | 38, 81 | eqssd 3966 |
. . . . 5
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β ran
(π₯ β βͺ π β Ο (π΄ βm π) β¦ ran π₯) = (π« π΄ β© Fin)) |
83 | | df-fo 6507 |
. . . . 5
β’ ((π₯ β βͺ π β Ο (π΄ βm π) β¦ ran π₯):βͺ π β Ο (π΄ βm π)βontoβ(π« π΄ β© Fin) β ((π₯ β βͺ
π β Ο (π΄ βm π) β¦ ran π₯) Fn βͺ
π β Ο (π΄ βm π) β§ ran (π₯ β βͺ
π β Ο (π΄ βm π) β¦ ran π₯) = (π« π΄ β© Fin))) |
84 | 37, 82, 83 | sylanbrc 584 |
. . . 4
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β (π₯ β βͺ π β Ο (π΄ βm π) β¦ ran π₯):βͺ π β Ο (π΄ βm π)βontoβ(π« π΄ β© Fin)) |
85 | | fodomnum 10000 |
. . . 4
β’ (βͺ π β Ο (π΄ βm π) β dom card β ((π₯ β βͺ
π β Ο (π΄ βm π) β¦ ran π₯):βͺ π β Ο (π΄ βm π)βontoβ(π« π΄ β© Fin) β (π« π΄ β© Fin) βΌ βͺ π β Ο (π΄ βm π))) |
86 | 12, 84, 85 | sylc 65 |
. . 3
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β
(π« π΄ β© Fin)
βΌ βͺ π β Ο (π΄ βm π)) |
87 | | domtr 8954 |
. . 3
β’
(((π« π΄ β©
Fin) βΌ βͺ π β Ο (π΄ βm π) β§ βͺ
π β Ο (π΄ βm π) βΌ π΄) β (π« π΄ β© Fin) βΌ π΄) |
88 | 86, 10, 87 | syl2anc 585 |
. 2
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β
(π« π΄ β© Fin)
βΌ π΄) |
89 | | pwexg 5338 |
. . . . 5
β’ (π΄ β dom card β
π« π΄ β
V) |
90 | 89 | adantr 482 |
. . . 4
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β π«
π΄ β
V) |
91 | | inex1g 5281 |
. . . 4
β’
(π« π΄ β
V β (π« π΄ β©
Fin) β V) |
92 | 90, 91 | syl 17 |
. . 3
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β
(π« π΄ β© Fin)
β V) |
93 | | infpwfidom 9971 |
. . 3
β’
((π« π΄ β©
Fin) β V β π΄
βΌ (π« π΄ β©
Fin)) |
94 | 92, 93 | syl 17 |
. 2
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β π΄ βΌ (π« π΄ β© Fin)) |
95 | | sbth 9044 |
. 2
β’
(((π« π΄ β©
Fin) βΌ π΄ β§ π΄ βΌ (π« π΄ β© Fin)) β (π«
π΄ β© Fin) β π΄) |
96 | 88, 94, 95 | syl2anc 585 |
1
β’ ((π΄ β dom card β§ Ο
βΌ π΄) β
(π« π΄ β© Fin)
β π΄) |