Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . 3
β’ (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π}) = (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π}) |
2 | 1 | rnmpt 5915 |
. 2
β’ ran
(π β Ο β¦
βͺ {π β π΄ β£ π βΌ π}) = {π β£ βπ β Ο π = βͺ {π β π΄ β£ π βΌ π}} |
3 | | unieq 4881 |
. . . . . . . . . . . 12
β’ ({π β π΄ β£ π βΌ π} = β
β βͺ {π
β π΄ β£ π βΌ π} = βͺ
β
) |
4 | | uni0 4901 |
. . . . . . . . . . . 12
β’ βͺ β
= β
|
5 | 3, 4 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ ({π β π΄ β£ π βΌ π} = β
β βͺ {π
β π΄ β£ π βΌ π} = β
) |
6 | 5 | adantl 483 |
. . . . . . . . . 10
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β Ο) β§
{π β π΄ β£ π βΌ π} = β
) β βͺ {π
β π΄ β£ π βΌ π} = β
) |
7 | | 0ex 5269 |
. . . . . . . . . . 11
β’ β
β V |
8 | 7 | elsn2 4630 |
. . . . . . . . . 10
β’ (βͺ {π
β π΄ β£ π βΌ π} β {β
} β βͺ {π
β π΄ β£ π βΌ π} = β
) |
9 | 6, 8 | sylibr 233 |
. . . . . . . . 9
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β Ο) β§
{π β π΄ β£ π βΌ π} = β
) β βͺ {π
β π΄ β£ π βΌ π} β {β
}) |
10 | 9 | olcd 873 |
. . . . . . . 8
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β Ο) β§
{π β π΄ β£ π βΌ π} = β
) β (βͺ {π
β π΄ β£ π βΌ π} β π΄ β¨ βͺ {π β π΄ β£ π βΌ π} β {β
})) |
11 | | ssrab2 4042 |
. . . . . . . . . 10
β’ {π β π΄ β£ π βΌ π} β π΄ |
12 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β Ο) β§
{π β π΄ β£ π βΌ π} β β
) β {π β π΄ β£ π βΌ π} β β
) |
13 | | fin1a2lem9 10351 |
. . . . . . . . . . . 12
β’ ((
[β] Or π΄
β§ π΄ β Fin β§
π β Ο) β
{π β π΄ β£ π βΌ π} β Fin) |
14 | 13 | ad4ant123 1173 |
. . . . . . . . . . 11
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β Ο) β§
{π β π΄ β£ π βΌ π} β β
) β {π β π΄ β£ π βΌ π} β Fin) |
15 | | simplll 774 |
. . . . . . . . . . . 12
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β Ο) β§
{π β π΄ β£ π βΌ π} β β
) β [β] Or
π΄) |
16 | | soss 5570 |
. . . . . . . . . . . 12
β’ ({π β π΄ β£ π βΌ π} β π΄ β ( [β] Or π΄ β [β] Or
{π β π΄ β£ π βΌ π})) |
17 | 11, 15, 16 | mpsyl 68 |
. . . . . . . . . . 11
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β Ο) β§
{π β π΄ β£ π βΌ π} β β
) β [β] Or
{π β π΄ β£ π βΌ π}) |
18 | | fin1a2lem10 10352 |
. . . . . . . . . . 11
β’ (({π β π΄ β£ π βΌ π} β β
β§ {π β π΄ β£ π βΌ π} β Fin β§ [β] Or
{π β π΄ β£ π βΌ π}) β βͺ {π β π΄ β£ π βΌ π} β {π β π΄ β£ π βΌ π}) |
19 | 12, 14, 17, 18 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β Ο) β§
{π β π΄ β£ π βΌ π} β β
) β βͺ {π
β π΄ β£ π βΌ π} β {π β π΄ β£ π βΌ π}) |
20 | 11, 19 | sselid 3947 |
. . . . . . . . 9
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β Ο) β§
{π β π΄ β£ π βΌ π} β β
) β βͺ {π
β π΄ β£ π βΌ π} β π΄) |
21 | 20 | orcd 872 |
. . . . . . . 8
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β Ο) β§
{π β π΄ β£ π βΌ π} β β
) β (βͺ {π
β π΄ β£ π βΌ π} β π΄ β¨ βͺ {π β π΄ β£ π βΌ π} β {β
})) |
22 | 10, 21 | pm2.61dane 3033 |
. . . . . . 7
β’ (((
[β] Or π΄
β§ π΄ β Fin) β§
π β Ο) β
(βͺ {π β π΄ β£ π βΌ π} β π΄ β¨ βͺ {π β π΄ β£ π βΌ π} β {β
})) |
23 | | eleq1 2826 |
. . . . . . . 8
β’ (π = βͺ
{π β π΄ β£ π βΌ π} β (π β π΄ β βͺ {π β π΄ β£ π βΌ π} β π΄)) |
24 | | eleq1 2826 |
. . . . . . . 8
β’ (π = βͺ
{π β π΄ β£ π βΌ π} β (π β {β
} β βͺ {π
β π΄ β£ π βΌ π} β {β
})) |
25 | 23, 24 | orbi12d 918 |
. . . . . . 7
β’ (π = βͺ
{π β π΄ β£ π βΌ π} β ((π β π΄ β¨ π β {β
}) β (βͺ {π
β π΄ β£ π βΌ π} β π΄ β¨ βͺ {π β π΄ β£ π βΌ π} β {β
}))) |
26 | 22, 25 | syl5ibrcom 247 |
. . . . . 6
β’ (((
[β] Or π΄
β§ π΄ β Fin) β§
π β Ο) β
(π = βͺ {π
β π΄ β£ π βΌ π} β (π β π΄ β¨ π β {β
}))) |
27 | 26 | rexlimdva 3153 |
. . . . 5
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
(βπ β Ο
π = βͺ {π
β π΄ β£ π βΌ π} β (π β π΄ β¨ π β {β
}))) |
28 | | simpr 486 |
. . . . . . . . . 10
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
π΄ β
Fin) |
29 | 28 | sselda 3949 |
. . . . . . . . 9
β’ (((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β π β Fin) |
30 | | ficardom 9904 |
. . . . . . . . 9
β’ (π β Fin β
(cardβπ) β
Ο) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
β’ (((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β (cardβπ) β Ο) |
32 | | breq1 5113 |
. . . . . . . . . . 11
β’ (π = π β (π βΌ (cardβπ) β π βΌ (cardβπ))) |
33 | | simpr 486 |
. . . . . . . . . . 11
β’ (((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β π β π΄) |
34 | | ficardid 9905 |
. . . . . . . . . . . . 13
β’ (π β Fin β
(cardβπ) β
π) |
35 | 29, 34 | syl 17 |
. . . . . . . . . . . 12
β’ (((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β (cardβπ) β π) |
36 | | ensym 8950 |
. . . . . . . . . . . 12
β’
((cardβπ)
β π β π β (cardβπ)) |
37 | | endom 8926 |
. . . . . . . . . . . 12
β’ (π β (cardβπ) β π βΌ (cardβπ)) |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . . . 11
β’ (((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β π βΌ (cardβπ)) |
39 | 32, 33, 38 | elrabd 3652 |
. . . . . . . . . 10
β’ (((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β π β {π β π΄ β£ π βΌ (cardβπ)}) |
40 | | elssuni 4903 |
. . . . . . . . . 10
β’ (π β {π β π΄ β£ π βΌ (cardβπ)} β π β βͺ {π β π΄ β£ π βΌ (cardβπ)}) |
41 | 39, 40 | syl 17 |
. . . . . . . . 9
β’ (((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β π β βͺ {π β π΄ β£ π βΌ (cardβπ)}) |
42 | | breq1 5113 |
. . . . . . . . . . . . 13
β’ (π = π β (π βΌ (cardβπ) β π βΌ (cardβπ))) |
43 | 42 | elrab 3650 |
. . . . . . . . . . . 12
β’ (π β {π β π΄ β£ π βΌ (cardβπ)} β (π β π΄ β§ π βΌ (cardβπ))) |
44 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β§ (π β π΄ β§ π βΌ (cardβπ))) β π βΌ (cardβπ)) |
45 | 35 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β§ (π β π΄ β§ π βΌ (cardβπ))) β (cardβπ) β π) |
46 | | domentr 8960 |
. . . . . . . . . . . . . . 15
β’ ((π βΌ (cardβπ) β§ (cardβπ) β π) β π βΌ π) |
47 | 44, 45, 46 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β§ (π β π΄ β§ π βΌ (cardβπ))) β π βΌ π) |
48 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β§ (π β π΄ β§ π βΌ (cardβπ))) β π΄ β Fin) |
49 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β§ (π β π΄ β§ π βΌ (cardβπ))) β π β π΄) |
50 | 48, 49 | sseldd 3950 |
. . . . . . . . . . . . . . 15
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β§ (π β π΄ β§ π βΌ (cardβπ))) β π β Fin) |
51 | 29 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β§ (π β π΄ β§ π βΌ (cardβπ))) β π β Fin) |
52 | | simplll 774 |
. . . . . . . . . . . . . . . 16
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β§ (π β π΄ β§ π βΌ (cardβπ))) β [β] Or π΄) |
53 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β§ (π β π΄ β§ π βΌ (cardβπ))) β π β π΄) |
54 | | sorpssi 7671 |
. . . . . . . . . . . . . . . 16
β’ ((
[β] Or π΄
β§ (π β π΄ β§ π β π΄)) β (π β π β¨ π β π)) |
55 | 52, 49, 53, 54 | syl12anc 836 |
. . . . . . . . . . . . . . 15
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β§ (π β π΄ β§ π βΌ (cardβπ))) β (π β π β¨ π β π)) |
56 | | fincssdom 10266 |
. . . . . . . . . . . . . . 15
β’ ((π β Fin β§ π β Fin β§ (π β π β¨ π β π)) β (π βΌ π β π β π)) |
57 | 50, 51, 55, 56 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β§ (π β π΄ β§ π βΌ (cardβπ))) β (π βΌ π β π β π)) |
58 | 47, 57 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β§ (π β π΄ β§ π βΌ (cardβπ))) β π β π) |
59 | 58 | ex 414 |
. . . . . . . . . . . 12
β’ (((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β ((π β π΄ β§ π βΌ (cardβπ)) β π β π)) |
60 | 43, 59 | biimtrid 241 |
. . . . . . . . . . 11
β’ (((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β (π β {π β π΄ β£ π βΌ (cardβπ)} β π β π)) |
61 | 60 | ralrimiv 3143 |
. . . . . . . . . 10
β’ (((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β βπ β {π β π΄ β£ π βΌ (cardβπ)}π β π) |
62 | | unissb 4905 |
. . . . . . . . . 10
β’ (βͺ {π
β π΄ β£ π βΌ (cardβπ)} β π β βπ β {π β π΄ β£ π βΌ (cardβπ)}π β π) |
63 | 61, 62 | sylibr 233 |
. . . . . . . . 9
β’ (((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β βͺ {π β π΄ β£ π βΌ (cardβπ)} β π) |
64 | 41, 63 | eqssd 3966 |
. . . . . . . 8
β’ (((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β π = βͺ {π β π΄ β£ π βΌ (cardβπ)}) |
65 | | breq2 5114 |
. . . . . . . . . . 11
β’ (π = (cardβπ) β (π βΌ π β π βΌ (cardβπ))) |
66 | 65 | rabbidv 3418 |
. . . . . . . . . 10
β’ (π = (cardβπ) β {π β π΄ β£ π βΌ π} = {π β π΄ β£ π βΌ (cardβπ)}) |
67 | 66 | unieqd 4884 |
. . . . . . . . 9
β’ (π = (cardβπ) β βͺ {π
β π΄ β£ π βΌ π} = βͺ {π β π΄ β£ π βΌ (cardβπ)}) |
68 | 67 | rspceeqv 3600 |
. . . . . . . 8
β’
(((cardβπ)
β Ο β§ π =
βͺ {π β π΄ β£ π βΌ (cardβπ)}) β βπ β Ο π = βͺ {π β π΄ β£ π βΌ π}) |
69 | 31, 64, 68 | syl2anc 585 |
. . . . . . 7
β’ (((
[β] Or π΄
β§ π΄ β Fin) β§
π β π΄) β βπ β Ο π = βͺ {π β π΄ β£ π βΌ π}) |
70 | 69 | ex 414 |
. . . . . 6
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
(π β π΄ β βπ β Ο π = βͺ {π β π΄ β£ π βΌ π})) |
71 | | velsn 4607 |
. . . . . . 7
β’ (π β {β
} β π = β
) |
72 | | peano1 7830 |
. . . . . . . . 9
β’ β
β Ο |
73 | | dom0 9053 |
. . . . . . . . . . . . . . . 16
β’ (π βΌ β
β π = β
) |
74 | 73 | biimpi 215 |
. . . . . . . . . . . . . . 15
β’ (π βΌ β
β π = β
) |
75 | 74 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β π΄ β§ π βΌ β
) β π = β
) |
76 | 75 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
((π β π΄ β§ π βΌ β
) β π = β
)) |
77 | | breq1 5113 |
. . . . . . . . . . . . . 14
β’ (π = π β (π βΌ β
β π βΌ β
)) |
78 | 77 | elrab 3650 |
. . . . . . . . . . . . 13
β’ (π β {π β π΄ β£ π βΌ β
} β (π β π΄ β§ π βΌ β
)) |
79 | | velsn 4607 |
. . . . . . . . . . . . 13
β’ (π β {β
} β π = β
) |
80 | 76, 78, 79 | 3imtr4g 296 |
. . . . . . . . . . . 12
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
(π β {π β π΄ β£ π βΌ β
} β π β {β
})) |
81 | 80 | ssrdv 3955 |
. . . . . . . . . . 11
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
{π β π΄ β£ π βΌ β
} β
{β
}) |
82 | | uni0b 4899 |
. . . . . . . . . . 11
β’ (βͺ {π
β π΄ β£ π βΌ β
} = β
β {π β π΄ β£ π βΌ β
} β
{β
}) |
83 | 81, 82 | sylibr 233 |
. . . . . . . . . 10
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
βͺ {π β π΄ β£ π βΌ β
} = β
) |
84 | 83 | eqcomd 2743 |
. . . . . . . . 9
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
β
= βͺ {π β π΄ β£ π βΌ β
}) |
85 | | breq2 5114 |
. . . . . . . . . . . 12
β’ (π = β
β (π βΌ π β π βΌ β
)) |
86 | 85 | rabbidv 3418 |
. . . . . . . . . . 11
β’ (π = β
β {π β π΄ β£ π βΌ π} = {π β π΄ β£ π βΌ β
}) |
87 | 86 | unieqd 4884 |
. . . . . . . . . 10
β’ (π = β
β βͺ {π
β π΄ β£ π βΌ π} = βͺ {π β π΄ β£ π βΌ β
}) |
88 | 87 | rspceeqv 3600 |
. . . . . . . . 9
β’ ((β
β Ο β§ β
= βͺ {π β π΄ β£ π βΌ β
}) β βπ β Ο β
= βͺ {π
β π΄ β£ π βΌ π}) |
89 | 72, 84, 88 | sylancr 588 |
. . . . . . . 8
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
βπ β Ο
β
= βͺ {π β π΄ β£ π βΌ π}) |
90 | | eqeq1 2741 |
. . . . . . . . 9
β’ (π = β
β (π = βͺ
{π β π΄ β£ π βΌ π} β β
= βͺ {π
β π΄ β£ π βΌ π})) |
91 | 90 | rexbidv 3176 |
. . . . . . . 8
β’ (π = β
β (βπ β Ο π = βͺ
{π β π΄ β£ π βΌ π} β βπ β Ο β
= βͺ {π
β π΄ β£ π βΌ π})) |
92 | 89, 91 | syl5ibrcom 247 |
. . . . . . 7
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
(π = β
β
βπ β Ο
π = βͺ {π
β π΄ β£ π βΌ π})) |
93 | 71, 92 | biimtrid 241 |
. . . . . 6
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
(π β {β
} β
βπ β Ο
π = βͺ {π
β π΄ β£ π βΌ π})) |
94 | 70, 93 | jaod 858 |
. . . . 5
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
((π β π΄ β¨ π β {β
}) β βπ β Ο π = βͺ
{π β π΄ β£ π βΌ π})) |
95 | 27, 94 | impbid 211 |
. . . 4
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
(βπ β Ο
π = βͺ {π
β π΄ β£ π βΌ π} β (π β π΄ β¨ π β {β
}))) |
96 | | elun 4113 |
. . . 4
β’ (π β (π΄ βͺ {β
}) β (π β π΄ β¨ π β {β
})) |
97 | 95, 96 | bitr4di 289 |
. . 3
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
(βπ β Ο
π = βͺ {π
β π΄ β£ π βΌ π} β π β (π΄ βͺ {β
}))) |
98 | 97 | abbi1dv 2873 |
. 2
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
{π β£ βπ β Ο π = βͺ
{π β π΄ β£ π βΌ π}} = (π΄ βͺ {β
})) |
99 | 2, 98 | eqtrid 2789 |
1
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
ran (π β Ο
β¦ βͺ {π β π΄ β£ π βΌ π}) = (π΄ βͺ {β
})) |