Step | Hyp | Ref
| Expression |
1 | | omex 9584 |
. . . . 5
β’ Ο
β V |
2 | 1 | 0dom 9053 |
. . . 4
β’ β
βΌ Ο |
3 | | breq1 5109 |
. . . 4
β’ (βͺ π΄ =
β
β (βͺ π΄ βΌ Ο β β
βΌ
Ο)) |
4 | 2, 3 | mpbiri 258 |
. . 3
β’ (βͺ π΄ =
β
β βͺ π΄ βΌ Ο) |
5 | 4 | a1d 25 |
. 2
β’ (βͺ π΄ =
β
β ((π΄ βΌ
Ο β§ π΄ β Fin
β§ π΅ Or βͺ π΄)
β βͺ π΄ βΌ Ο)) |
6 | | n0 4307 |
. . 3
β’ (βͺ π΄
β β
β βπ π β βͺ π΄) |
7 | | ne0i 4295 |
. . . . . . . . . 10
β’ (π β βͺ π΄
β βͺ π΄ β β
) |
8 | | unieq 4877 |
. . . . . . . . . . . 12
β’ (π΄ = β
β βͺ π΄ =
βͺ β
) |
9 | | uni0 4897 |
. . . . . . . . . . . 12
β’ βͺ β
= β
|
10 | 8, 9 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (π΄ = β
β βͺ π΄ =
β
) |
11 | 10 | necon3i 2973 |
. . . . . . . . . 10
β’ (βͺ π΄
β β
β π΄ β
β
) |
12 | 7, 11 | syl 17 |
. . . . . . . . 9
β’ (π β βͺ π΄
β π΄ β
β
) |
13 | 12 | adantl 483 |
. . . . . . . 8
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ π β βͺ π΄) β π΄ β β
) |
14 | | simpl1 1192 |
. . . . . . . . 9
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ π β βͺ π΄) β π΄ βΌ Ο) |
15 | | ctex 8906 |
. . . . . . . . 9
β’ (π΄ βΌ Ο β π΄ β V) |
16 | | 0sdomg 9051 |
. . . . . . . . 9
β’ (π΄ β V β (β
βΊ π΄ β π΄ β β
)) |
17 | 14, 15, 16 | 3syl 18 |
. . . . . . . 8
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ π β βͺ π΄) β (β
βΊ π΄ β π΄ β β
)) |
18 | 13, 17 | mpbird 257 |
. . . . . . 7
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ π β βͺ π΄) β β
βΊ π΄) |
19 | | fodomr 9075 |
. . . . . . 7
β’ ((β
βΊ π΄ β§ π΄ βΌ Ο) β
βπ π:Οβontoβπ΄) |
20 | 18, 14, 19 | syl2anc 585 |
. . . . . 6
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ π β βͺ π΄) β βπ π:Οβontoβπ΄) |
21 | | omelon 9587 |
. . . . . . . . . . . 12
β’ Ο
β On |
22 | | onenon 9890 |
. . . . . . . . . . . 12
β’ (Ο
β On β Ο β dom card) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . 11
β’ Ο
β dom card |
24 | | xpnum 9892 |
. . . . . . . . . . 11
β’ ((Ο
β dom card β§ Ο β dom card) β (Ο Γ Ο)
β dom card) |
25 | 23, 23, 24 | mp2an 691 |
. . . . . . . . . 10
β’ (Ο
Γ Ο) β dom card |
26 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β π:Οβontoβπ΄) |
27 | | fof 6757 |
. . . . . . . . . . . . . . . . . . 19
β’ (π:Οβontoβπ΄ β π:ΟβΆπ΄) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β π:ΟβΆπ΄) |
29 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β π β Ο) |
30 | 28, 29 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β (πβπ) β π΄) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ βΌ
Ο β§ π΄ β Fin
β§ π΅ Or βͺ π΄)
β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β§ π β (cardβ(πβπ))) β (πβπ) β π΄) |
32 | | elssuni 4899 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) β π΄ β (πβπ) β βͺ π΄) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ βΌ
Ο β§ π΄ β Fin
β§ π΅ Or βͺ π΄)
β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β§ π β (cardβ(πβπ))) β (πβπ) β βͺ π΄) |
34 | 30, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β (πβπ) β βͺ π΄) |
35 | | simpll3 1215 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β π΅ Or βͺ π΄) |
36 | | soss 5566 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πβπ) β βͺ π΄ β (π΅ Or βͺ π΄ β π΅ Or (πβπ))) |
37 | 34, 35, 36 | sylc 65 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β π΅ Or (πβπ)) |
38 | | simpll2 1214 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β π΄ β Fin) |
39 | 38, 30 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β (πβπ) β Fin) |
40 | | finnisoeu 10054 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΅ Or (πβπ) β§ (πβπ) β Fin) β β!β β Isom E , π΅ ((cardβ(πβπ)), (πβπ))) |
41 | 37, 39, 40 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β β!β β Isom E , π΅ ((cardβ(πβπ)), (πβπ))) |
42 | | iotacl 6483 |
. . . . . . . . . . . . . . . . . . 19
β’
(β!β β Isom E , π΅ ((cardβ(πβπ)), (πβπ)) β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) β {β β£ β Isom E , π΅ ((cardβ(πβπ)), (πβπ))}) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) β {β β£ β Isom E , π΅ ((cardβ(πβπ)), (πβπ))}) |
44 | | iotaex 6470 |
. . . . . . . . . . . . . . . . . . 19
β’
(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) β V |
45 | | isoeq1 7263 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) β (π Isom E , π΅ ((cardβ(πβπ)), (πβπ)) β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) Isom E , π΅ ((cardβ(πβπ)), (πβπ)))) |
46 | | isoeq1 7263 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β = π β (β Isom E , π΅ ((cardβ(πβπ)), (πβπ)) β π Isom E , π΅ ((cardβ(πβπ)), (πβπ)))) |
47 | 46 | cbvabv 2806 |
. . . . . . . . . . . . . . . . . . 19
β’ {β β£ β Isom E , π΅ ((cardβ(πβπ)), (πβπ))} = {π β£ π Isom E , π΅ ((cardβ(πβπ)), (πβπ))} |
48 | 44, 45, 47 | elab2 3635 |
. . . . . . . . . . . . . . . . . 18
β’
((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) β {β β£ β Isom E , π΅ ((cardβ(πβπ)), (πβπ))} β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) Isom E , π΅ ((cardβ(πβπ)), (πβπ))) |
49 | 43, 48 | sylib 217 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) Isom E , π΅ ((cardβ(πβπ)), (πβπ))) |
50 | | isof1o 7269 |
. . . . . . . . . . . . . . . . 17
β’
((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) Isom E , π΅ ((cardβ(πβπ)), (πβπ)) β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))):(cardβ(πβπ))β1-1-ontoβ(πβπ)) |
51 | | f1of 6785 |
. . . . . . . . . . . . . . . . 17
β’
((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))):(cardβ(πβπ))β1-1-ontoβ(πβπ) β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))):(cardβ(πβπ))βΆ(πβπ)) |
52 | 49, 50, 51 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))):(cardβ(πβπ))βΆ(πβπ)) |
53 | 52 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ βΌ
Ο β§ π΄ β Fin
β§ π΅ Or βͺ π΄)
β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β§ π β (cardβ(πβπ))) β ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) β (πβπ)) |
54 | 33, 53 | sseldd 3946 |
. . . . . . . . . . . . . 14
β’
(((((π΄ βΌ
Ο β§ π΄ β Fin
β§ π΅ Or βͺ π΄)
β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β§ π β (cardβ(πβπ))) β ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) β βͺ π΄) |
55 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β π β βͺ π΄) |
56 | 55 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((π΄ βΌ
Ο β§ π΄ β Fin
β§ π΅ Or βͺ π΄)
β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β§ Β¬ π β (cardβ(πβπ))) β π β βͺ π΄) |
57 | 54, 56 | ifclda 4522 |
. . . . . . . . . . . . 13
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β Ο β§ π β Ο)) β if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π) β βͺ π΄) |
58 | 57 | ralrimivva 3194 |
. . . . . . . . . . . 12
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β βπ β Ο βπ β Ο if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π) β βͺ π΄) |
59 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π)) = (π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π)) |
60 | 59 | fmpo 8001 |
. . . . . . . . . . . 12
β’
(βπ β
Ο βπ β
Ο if(π β
(cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π) β βͺ π΄ β (π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π)):(Ο Γ Ο)βΆβͺ π΄) |
61 | 58, 60 | sylib 217 |
. . . . . . . . . . 11
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β (π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π)):(Ο Γ Ο)βΆβͺ π΄) |
62 | | eluni 4869 |
. . . . . . . . . . . . 13
β’ (π β βͺ π΄
β βπ(π β π β§ π β π΄)) |
63 | | simplrr 777 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β π β§ π β π΄)) β π:Οβontoβπ΄) |
64 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β π β§ π β π΄)) β π β π΄) |
65 | | foelrn 7057 |
. . . . . . . . . . . . . . . . 17
β’ ((π:Οβontoβπ΄ β§ π β π΄) β βπ β Ο π = (πβπ)) |
66 | 63, 64, 65 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β π β§ π β π΄)) β βπ β Ο π = (πβπ)) |
67 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β π β Ο) |
68 | | ordom 7813 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ Ord
Ο |
69 | | simpll2 1214 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β π΄ β Fin) |
70 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β π:Οβontoβπ΄) |
71 | 70, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β π:ΟβΆπ΄) |
72 | 71, 67 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β (πβπ) β π΄) |
73 | 69, 72 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β (πβπ) β Fin) |
74 | | ficardom 9902 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πβπ) β Fin β (cardβ(πβπ)) β Ο) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β (cardβ(πβπ)) β Ο) |
76 | | ordelss 6334 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((Ord
Ο β§ (cardβ(πβπ)) β Ο) β (cardβ(πβπ)) β Ο) |
77 | 68, 75, 76 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β (cardβ(πβπ)) β Ο) |
78 | | elssuni 4899 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πβπ) β π΄ β (πβπ) β βͺ π΄) |
79 | 72, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β (πβπ) β βͺ π΄) |
80 | | simpll3 1215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β π΅ Or βͺ π΄) |
81 | | soss 5566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πβπ) β βͺ π΄ β (π΅ Or βͺ π΄ β π΅ Or (πβπ))) |
82 | 79, 80, 81 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β π΅ Or (πβπ)) |
83 | | finnisoeu 10054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π΅ Or (πβπ) β§ (πβπ) β Fin) β β!β β Isom E , π΅ ((cardβ(πβπ)), (πβπ))) |
84 | 82, 73, 83 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β β!β β Isom E , π΅ ((cardβ(πβπ)), (πβπ))) |
85 | | iotacl 6483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(β!β β Isom E , π΅ ((cardβ(πβπ)), (πβπ)) β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) β {β β£ β Isom E , π΅ ((cardβ(πβπ)), (πβπ))}) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) β {β β£ β Isom E , π΅ ((cardβ(πβπ)), (πβπ))}) |
87 | | iotaex 6470 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) β V |
88 | | isoeq1 7263 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) β (π Isom E , π΅ ((cardβ(πβπ)), (πβπ)) β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) Isom E , π΅ ((cardβ(πβπ)), (πβπ)))) |
89 | | isoeq1 7263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (β = π β (β Isom E , π΅ ((cardβ(πβπ)), (πβπ)) β π Isom E , π΅ ((cardβ(πβπ)), (πβπ)))) |
90 | 89 | cbvabv 2806 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ {β β£ β Isom E , π΅ ((cardβ(πβπ)), (πβπ))} = {π β£ π Isom E , π΅ ((cardβ(πβπ)), (πβπ))} |
91 | 87, 88, 90 | elab2 3635 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) β {β β£ β Isom E , π΅ ((cardβ(πβπ)), (πβπ))} β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) Isom E , π΅ ((cardβ(πβπ)), (πβπ))) |
92 | 86, 91 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) Isom E , π΅ ((cardβ(πβπ)), (πβπ))) |
93 | | isof1o 7269 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) Isom E , π΅ ((cardβ(πβπ)), (πβπ)) β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))):(cardβ(πβπ))β1-1-ontoβ(πβπ)) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))):(cardβ(πβπ))β1-1-ontoβ(πβπ)) |
95 | | f1ocnv 6797 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))):(cardβ(πβπ))β1-1-ontoβ(πβπ) β β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))):(πβπ)β1-1-ontoβ(cardβ(πβπ))) |
96 | | f1of 6785 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))):(πβπ)β1-1-ontoβ(cardβ(πβπ)) β β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))):(πβπ)βΆ(cardβ(πβπ))) |
97 | 94, 95, 96 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))):(πβπ)βΆ(cardβ(πβπ))) |
98 | | simprll 778 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β π β π) |
99 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β π = (πβπ)) |
100 | 98, 99 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β π β (πβπ)) |
101 | 97, 100 | ffvelcdmd 7037 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β (β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) β (cardβ(πβπ))) |
102 | 77, 101 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β (β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) β Ο) |
103 | | 2fveq3 6848 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π β (cardβ(πβπ)) = (cardβ(πβπ))) |
104 | 103 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β (π β (cardβ(πβπ)) β π β (cardβ(πβπ)))) |
105 | | isoeq4 7266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((cardβ(πβπ)) = (cardβ(πβπ)) β (β Isom E , π΅ ((cardβ(πβπ)), (πβπ)) β β Isom E , π΅ ((cardβ(πβπ)), (πβπ)))) |
106 | 103, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = π β (β Isom E , π΅ ((cardβ(πβπ)), (πβπ)) β β Isom E , π΅ ((cardβ(πβπ)), (πβπ)))) |
107 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = π β (πβπ) = (πβπ)) |
108 | | isoeq5 7267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πβπ) = (πβπ) β (β Isom E , π΅ ((cardβ(πβπ)), (πβπ)) β β Isom E , π΅ ((cardβ(πβπ)), (πβπ)))) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = π β (β Isom E , π΅ ((cardβ(πβπ)), (πβπ)) β β Isom E , π΅ ((cardβ(πβπ)), (πβπ)))) |
110 | 106, 109 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = π β (β Isom E , π΅ ((cardβ(πβπ)), (πβπ)) β β Isom E , π΅ ((cardβ(πβπ)), (πβπ)))) |
111 | 110 | iotabidv 6481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π β (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))) = (β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))) |
112 | 111 | fveq1d 6845 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) = ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ)) |
113 | 104, 112 | ifbieq1d 4511 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π) = if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π)) |
114 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) β (π β (cardβ(πβπ)) β (β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) β (cardβ(πβπ)))) |
115 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) β ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) = ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))β(β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ))) |
116 | 114, 115 | ifbieq1d 4511 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) β if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π) = if((β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))β(β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ)), π)) |
117 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))β(β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ)) β V |
118 | | vex 3448 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ π β V |
119 | 117, 118 | ifex 4537 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ if((β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))β(β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ)), π) β V |
120 | 113, 116,
59, 119 | ovmpo 7516 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β Ο β§ (β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) β Ο) β (π(π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π))(β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ)) = if((β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))β(β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ)), π)) |
121 | 67, 102, 120 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β (π(π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π))(β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ)) = if((β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))β(β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ)), π)) |
122 | 101 | iftrued 4495 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β if((β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))β(β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ)), π) = ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))β(β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ))) |
123 | | f1ocnvfv2 7224 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ))):(cardβ(πβπ))β1-1-ontoβ(πβπ) β§ π β (πβπ)) β ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))β(β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ)) = π) |
124 | 94, 100, 123 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))β(β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ)) = π) |
125 | 121, 122,
124 | 3eqtrrd 2778 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β π = (π(π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π))(β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ))) |
126 | | rspceov 7405 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Ο β§ (β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ) β Ο β§ π = (π(π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π))(β‘(β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ))) β βπ β Ο βπ β Ο π = (π(π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π))π)) |
127 | 67, 102, 125, 126 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ ((π β π β§ π β π΄) β§ (π β Ο β§ π = (πβπ)))) β βπ β Ο βπ β Ο π = (π(π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π))π)) |
128 | 127 | expr 458 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β π β§ π β π΄)) β ((π β Ο β§ π = (πβπ)) β βπ β Ο βπ β Ο π = (π(π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π))π))) |
129 | 128 | expd 417 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β π β§ π β π΄)) β (π β Ο β (π = (πβπ) β βπ β Ο βπ β Ο π = (π(π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π))π)))) |
130 | 129 | rexlimdv 3147 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β π β§ π β π΄)) β (βπ β Ο π = (πβπ) β βπ β Ο βπ β Ο π = (π(π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π))π))) |
131 | 66, 130 | mpd 15 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β§ (π β π β§ π β π΄)) β βπ β Ο βπ β Ο π = (π(π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π))π)) |
132 | 131 | ex 414 |
. . . . . . . . . . . . . 14
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β ((π β π β§ π β π΄) β βπ β Ο βπ β Ο π = (π(π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π))π))) |
133 | 132 | exlimdv 1937 |
. . . . . . . . . . . . 13
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β (βπ(π β π β§ π β π΄) β βπ β Ο βπ β Ο π = (π(π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π))π))) |
134 | 62, 133 | biimtrid 241 |
. . . . . . . . . . . 12
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β (π β βͺ π΄ β βπ β Ο βπ β Ο π = (π(π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π))π))) |
135 | 134 | ralrimiv 3139 |
. . . . . . . . . . 11
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β βπ β βͺ π΄βπ β Ο βπ β Ο π = (π(π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π))π)) |
136 | | foov 7529 |
. . . . . . . . . . 11
β’ ((π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π)):(Ο Γ Ο)βontoββͺ π΄ β ((π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π)):(Ο Γ Ο)βΆβͺ π΄
β§ βπ β
βͺ π΄βπ β Ο βπ β Ο π = (π(π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π))π))) |
137 | 61, 135, 136 | sylanbrc 584 |
. . . . . . . . . 10
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β (π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π)):(Ο Γ Ο)βontoββͺ π΄) |
138 | | fodomnum 9998 |
. . . . . . . . . 10
β’ ((Ο
Γ Ο) β dom card β ((π β Ο, π β Ο β¦ if(π β (cardβ(πβπ)), ((β©ββ Isom E , π΅ ((cardβ(πβπ)), (πβπ)))βπ), π)):(Ο Γ Ο)βontoββͺ π΄ β βͺ π΄
βΌ (Ο Γ Ο))) |
139 | 25, 137, 138 | mpsyl 68 |
. . . . . . . . 9
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β βͺ π΄ βΌ (Ο Γ
Ο)) |
140 | | xpomen 9956 |
. . . . . . . . 9
β’ (Ο
Γ Ο) β Ο |
141 | | domentr 8956 |
. . . . . . . . 9
β’ ((βͺ π΄
βΌ (Ο Γ Ο) β§ (Ο Γ Ο) β
Ο) β βͺ π΄ βΌ Ο) |
142 | 139, 140,
141 | sylancl 587 |
. . . . . . . 8
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ (π β βͺ π΄
β§ π:Οβontoβπ΄)) β βͺ π΄ βΌ
Ο) |
143 | 142 | expr 458 |
. . . . . . 7
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ π β βͺ π΄) β (π:Οβontoβπ΄ β βͺ π΄ βΌ
Ο)) |
144 | 143 | exlimdv 1937 |
. . . . . 6
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ π β βͺ π΄) β (βπ π:Οβontoβπ΄ β βͺ π΄ βΌ
Ο)) |
145 | 20, 144 | mpd 15 |
. . . . 5
β’ (((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β§ π β βͺ π΄) β βͺ π΄
βΌ Ο) |
146 | 145 | expcom 415 |
. . . 4
β’ (π β βͺ π΄
β ((π΄ βΌ Ο
β§ π΄ β Fin β§
π΅ Or βͺ π΄)
β βͺ π΄ βΌ Ο)) |
147 | 146 | exlimiv 1934 |
. . 3
β’
(βπ π β βͺ π΄
β ((π΄ βΌ Ο
β§ π΄ β Fin β§
π΅ Or βͺ π΄)
β βͺ π΄ βΌ Ο)) |
148 | 6, 147 | sylbi 216 |
. 2
β’ (βͺ π΄
β β
β ((π΄
βΌ Ο β§ π΄
β Fin β§ π΅ Or
βͺ π΄) β βͺ π΄ βΌ
Ο)) |
149 | 5, 148 | pm2.61ine 3025 |
1
β’ ((π΄ βΌ Ο β§ π΄ β Fin β§ π΅ Or βͺ
π΄) β βͺ π΄
βΌ Ο) |