Step | Hyp | Ref
| Expression |
1 | | rankwflemb 9734 |
. . . 4
β’ (π¦ β βͺ (π
1 β On) β βπ§ β On π¦ β (π
1βsuc
π§)) |
2 | | harcl 9500 |
. . . . . . . . 9
β’
(harβ(π
1βπ§)) β On |
3 | | pweq 4575 |
. . . . . . . . . . 11
β’ (π₯ =
(harβ(π
1βπ§)) β π« π₯ = π«
(harβ(π
1βπ§))) |
4 | 3 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π₯ =
(harβ(π
1βπ§)) β (π« π₯ β dom card β π«
(harβ(π
1βπ§)) β dom card)) |
5 | 4 | rspcv 3576 |
. . . . . . . . 9
β’
((harβ(π
1βπ§)) β On β (βπ₯ β On π« π₯ β dom card β
π« (harβ(π
1βπ§)) β dom card)) |
6 | 2, 5 | ax-mp 5 |
. . . . . . . 8
β’
(βπ₯ β On
π« π₯ β dom card
β π« (harβ(π
1βπ§)) β dom card) |
7 | | cardid2 9894 |
. . . . . . . 8
β’
(π« (harβ(π
1βπ§)) β dom card β
(cardβπ« (harβ(π
1βπ§))) β π«
(harβ(π
1βπ§))) |
8 | | ensym 8946 |
. . . . . . . 8
β’
((cardβπ« (harβ(π
1βπ§))) β π«
(harβ(π
1βπ§)) β π«
(harβ(π
1βπ§)) β (cardβπ«
(harβ(π
1βπ§)))) |
9 | | bren 8896 |
. . . . . . . . 9
β’
(π« (harβ(π
1βπ§)) β (cardβπ«
(harβ(π
1βπ§))) β βπ π:π«
(harβ(π
1βπ§))β1-1-ontoβ(cardβπ«
(harβ(π
1βπ§)))) |
10 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π:π«
(harβ(π
1βπ§))β1-1-ontoβ(cardβπ«
(harβ(π
1βπ§))) β§ π§ β On) β π§ β On) |
11 | | f1of1 6784 |
. . . . . . . . . . . . . 14
β’ (π:π«
(harβ(π
1βπ§))β1-1-ontoβ(cardβπ«
(harβ(π
1βπ§))) β π:π«
(harβ(π
1βπ§))β1-1β(cardβπ«
(harβ(π
1βπ§)))) |
12 | 11 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π:π«
(harβ(π
1βπ§))β1-1-ontoβ(cardβπ«
(harβ(π
1βπ§))) β§ π§ β On) β π:π«
(harβ(π
1βπ§))β1-1β(cardβπ«
(harβ(π
1βπ§)))) |
13 | | cardon 9885 |
. . . . . . . . . . . . . 14
β’
(cardβπ« (harβ(π
1βπ§))) β On |
14 | 13 | onssi 7774 |
. . . . . . . . . . . . 13
β’
(cardβπ« (harβ(π
1βπ§))) β On |
15 | | f1ss 6745 |
. . . . . . . . . . . . 13
β’ ((π:π«
(harβ(π
1βπ§))β1-1β(cardβπ«
(harβ(π
1βπ§))) β§ (cardβπ«
(harβ(π
1βπ§))) β On) β π:π«
(harβ(π
1βπ§))β1-1βOn) |
16 | 12, 14, 15 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π:π«
(harβ(π
1βπ§))β1-1-ontoβ(cardβπ«
(harβ(π
1βπ§))) β§ π§ β On) β π:π«
(harβ(π
1βπ§))β1-1βOn) |
17 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π β (rankβπ¦) = (rankβπ)) |
18 | 17 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = π β (suc βͺ ran
βͺ ran π₯ Β·o (rankβπ¦)) = (suc βͺ ran βͺ ran π₯ Β·o (rankβπ))) |
19 | | suceq 6384 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((rankβπ¦) =
(rankβπ) β suc
(rankβπ¦) = suc
(rankβπ)) |
20 | 17, 19 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π β suc (rankβπ¦) = suc (rankβπ)) |
21 | 20 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π β (π₯βsuc (rankβπ¦)) = (π₯βsuc (rankβπ))) |
22 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π β π¦ = π) |
23 | 21, 22 | fveq12d 6850 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = π β ((π₯βsuc (rankβπ¦))βπ¦) = ((π₯βsuc (rankβπ))βπ)) |
24 | 18, 23 | oveq12d 7376 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π β ((suc βͺ
ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)) = ((suc βͺ ran
βͺ ran π₯ Β·o (rankβπ)) +o ((π₯βsuc (rankβπ))βπ))) |
25 | | imaeq2 6010 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = π β ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦) = ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π)) |
26 | 25 | fveq2d 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π β (πβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)) = (πβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π))) |
27 | 24, 26 | ifeq12d 4508 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β if(dom π₯ = βͺ dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦))) = if(dom π₯ = βͺ dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ)) +o ((π₯βsuc (rankβπ))βπ)), (πβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π)))) |
28 | 27 | cbvmptv 5219 |
. . . . . . . . . . . . . . 15
β’ (π¦ β
(π
1βdom π₯) β¦ if(dom π₯ = βͺ dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)))) = (π β (π
1βdom
π₯) β¦ if(dom π₯ = βͺ
dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ)) +o ((π₯βsuc (rankβπ))βπ)), (πβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π)))) |
29 | | dmeq 5860 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β dom π₯ = dom π) |
30 | 29 | fveq2d 6847 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (π
1βdom
π₯) =
(π
1βdom π)) |
31 | 29 | unieqd 4880 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β βͺ dom
π₯ = βͺ dom π) |
32 | 29, 31 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (dom π₯ = βͺ dom π₯ β dom π = βͺ dom π)) |
33 | | rneq 5892 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = π β ran π₯ = ran π) |
34 | 33 | unieqd 4880 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π β βͺ ran
π₯ = βͺ ran π) |
35 | 34 | rneqd 5894 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π β ran βͺ ran
π₯ = ran βͺ ran π) |
36 | 35 | unieqd 4880 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π β βͺ ran
βͺ ran π₯ = βͺ ran βͺ ran π) |
37 | | suceq 6384 |
. . . . . . . . . . . . . . . . . . . 20
β’ (βͺ ran βͺ ran π₯ = βͺ ran βͺ ran π β suc βͺ ran
βͺ ran π₯ = suc βͺ ran βͺ ran π) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π β suc βͺ ran
βͺ ran π₯ = suc βͺ ran βͺ ran π) |
39 | 38 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β (suc βͺ ran
βͺ ran π₯ Β·o (rankβπ)) = (suc βͺ ran βͺ ran π Β·o (rankβπ))) |
40 | | fveq1 6842 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π β (π₯βsuc (rankβπ)) = (πβsuc (rankβπ))) |
41 | 40 | fveq1d 6845 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β ((π₯βsuc (rankβπ))βπ) = ((πβsuc (rankβπ))βπ)) |
42 | 39, 41 | oveq12d 7376 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β ((suc βͺ
ran βͺ ran π₯ Β·o (rankβπ)) +o ((π₯βsuc (rankβπ))βπ)) = ((suc βͺ ran
βͺ ran π Β·o (rankβπ)) +o ((πβsuc (rankβπ))βπ))) |
43 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ = π β π₯ = π) |
44 | 43, 31 | fveq12d 6850 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = π β (π₯ββͺ dom π₯) = (πββͺ dom π)) |
45 | 44 | rneqd 5894 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π β ran (π₯ββͺ dom π₯) = ran (πββͺ dom π)) |
46 | | oieq2 9454 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (ran
(π₯ββͺ dom π₯) = ran (πββͺ dom π) β OrdIso( E , ran (π₯ββͺ dom π₯)) = OrdIso( E , ran (πββͺ dom π))) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π β OrdIso( E , ran (π₯ββͺ dom π₯)) = OrdIso( E , ran (πββͺ dom π))) |
48 | 47 | cnveqd 5832 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π β β‘OrdIso( E , ran (π₯ββͺ dom π₯)) = β‘OrdIso( E , ran (πββͺ dom π))) |
49 | 48, 44 | coeq12d 5821 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π β (β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) = (β‘OrdIso( E , ran (πββͺ dom π)) β (πββͺ dom π))) |
50 | 49 | imaeq1d 6013 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π) = ((β‘OrdIso( E , ran (πββͺ dom π)) β (πββͺ dom π)) β π)) |
51 | 50 | fveq2d 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (πβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π)) = (πβ((β‘OrdIso( E , ran (πββͺ dom π)) β (πββͺ dom π)) β π))) |
52 | 32, 42, 51 | ifbieq12d 4515 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β if(dom π₯ = βͺ dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ)) +o ((π₯βsuc (rankβπ))βπ)), (πβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π))) = if(dom π = βͺ dom π, ((suc βͺ ran βͺ ran π Β·o (rankβπ)) +o ((πβsuc (rankβπ))βπ)), (πβ((β‘OrdIso( E , ran (πββͺ dom π)) β (πββͺ dom π)) β π)))) |
53 | 30, 52 | mpteq12dv 5197 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (π β (π
1βdom
π₯) β¦ if(dom π₯ = βͺ
dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ)) +o ((π₯βsuc (rankβπ))βπ)), (πβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π)))) = (π β (π
1βdom
π) β¦ if(dom π = βͺ
dom π, ((suc βͺ ran βͺ ran π Β·o (rankβπ)) +o ((πβsuc (rankβπ))βπ)), (πβ((β‘OrdIso( E , ran (πββͺ dom π)) β (πββͺ dom π)) β π))))) |
54 | 28, 53 | eqtrid 2785 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (π¦ β (π
1βdom
π₯) β¦ if(dom π₯ = βͺ
dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)))) = (π β (π
1βdom
π) β¦ if(dom π = βͺ
dom π, ((suc βͺ ran βͺ ran π Β·o (rankβπ)) +o ((πβsuc (rankβπ))βπ)), (πβ((β‘OrdIso( E , ran (πββͺ dom π)) β (πββͺ dom π)) β π))))) |
55 | 54 | cbvmptv 5219 |
. . . . . . . . . . . . 13
β’ (π₯ β V β¦ (π¦ β
(π
1βdom π₯) β¦ if(dom π₯ = βͺ dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦))))) = (π β V β¦ (π β (π
1βdom
π) β¦ if(dom π = βͺ
dom π, ((suc βͺ ran βͺ ran π Β·o (rankβπ)) +o ((πβsuc (rankβπ))βπ)), (πβ((β‘OrdIso( E , ran (πββͺ dom π)) β (πββͺ dom π)) β π))))) |
56 | | recseq 8321 |
. . . . . . . . . . . . 13
β’ ((π₯ β V β¦ (π¦ β
(π
1βdom π₯) β¦ if(dom π₯ = βͺ dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦))))) = (π β V β¦ (π β (π
1βdom
π) β¦ if(dom π = βͺ
dom π, ((suc βͺ ran βͺ ran π Β·o (rankβπ)) +o ((πβsuc (rankβπ))βπ)), (πβ((β‘OrdIso( E , ran (πββͺ dom π)) β (πββͺ dom π)) β π))))) β recs((π₯ β V β¦ (π¦ β (π
1βdom
π₯) β¦ if(dom π₯ = βͺ
dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)))))) = recs((π β V β¦ (π β (π
1βdom
π) β¦ if(dom π = βͺ
dom π, ((suc βͺ ran βͺ ran π Β·o (rankβπ)) +o ((πβsuc (rankβπ))βπ)), (πβ((β‘OrdIso( E , ran (πββͺ dom π)) β (πββͺ dom π)) β π))))))) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . 12
β’
recs((π₯ β V
β¦ (π¦ β
(π
1βdom π₯) β¦ if(dom π₯ = βͺ dom π₯, ((suc βͺ ran βͺ ran π₯ Β·o (rankβπ¦)) +o ((π₯βsuc (rankβπ¦))βπ¦)), (πβ((β‘OrdIso( E , ran (π₯ββͺ dom π₯)) β (π₯ββͺ dom π₯)) β π¦)))))) = recs((π β V β¦ (π β (π
1βdom
π) β¦ if(dom π = βͺ
dom π, ((suc βͺ ran βͺ ran π Β·o (rankβπ)) +o ((πβsuc (rankβπ))βπ)), (πβ((β‘OrdIso( E , ran (πββͺ dom π)) β (πββͺ dom π)) β π)))))) |
58 | 10, 16, 57 | dfac12lem3 10086 |
. . . . . . . . . . 11
β’ ((π:π«
(harβ(π
1βπ§))β1-1-ontoβ(cardβπ«
(harβ(π
1βπ§))) β§ π§ β On) β
(π
1βπ§) β dom card) |
59 | 58 | ex 414 |
. . . . . . . . . 10
β’ (π:π«
(harβ(π
1βπ§))β1-1-ontoβ(cardβπ«
(harβ(π
1βπ§))) β (π§ β On β
(π
1βπ§) β dom card)) |
60 | 59 | exlimiv 1934 |
. . . . . . . . 9
β’
(βπ π:π«
(harβ(π
1βπ§))β1-1-ontoβ(cardβπ«
(harβ(π
1βπ§))) β (π§ β On β
(π
1βπ§) β dom card)) |
61 | 9, 60 | sylbi 216 |
. . . . . . . 8
β’
(π« (harβ(π
1βπ§)) β (cardβπ«
(harβ(π
1βπ§))) β (π§ β On β
(π
1βπ§) β dom card)) |
62 | 6, 7, 8, 61 | 4syl 19 |
. . . . . . 7
β’
(βπ₯ β On
π« π₯ β dom card
β (π§ β On β
(π
1βπ§) β dom card)) |
63 | 62 | imp 408 |
. . . . . 6
β’
((βπ₯ β
On π« π₯ β dom
card β§ π§ β On)
β (π
1βπ§) β dom card) |
64 | | r1suc 9711 |
. . . . . . . . 9
β’ (π§ β On β
(π
1βsuc π§) = π«
(π
1βπ§)) |
65 | 64 | adantl 483 |
. . . . . . . 8
β’
((βπ₯ β
On π« π₯ β dom
card β§ π§ β On)
β (π
1βsuc π§) = π«
(π
1βπ§)) |
66 | 65 | eleq2d 2820 |
. . . . . . 7
β’
((βπ₯ β
On π« π₯ β dom
card β§ π§ β On)
β (π¦ β
(π
1βsuc π§) β π¦ β π«
(π
1βπ§))) |
67 | | elpwi 4568 |
. . . . . . 7
β’ (π¦ β π«
(π
1βπ§) β π¦ β (π
1βπ§)) |
68 | 66, 67 | syl6bi 253 |
. . . . . 6
β’
((βπ₯ β
On π« π₯ β dom
card β§ π§ β On)
β (π¦ β
(π
1βsuc π§) β π¦ β (π
1βπ§))) |
69 | | ssnum 9980 |
. . . . . 6
β’
(((π
1βπ§) β dom card β§ π¦ β (π
1βπ§)) β π¦ β dom card) |
70 | 63, 68, 69 | syl6an 683 |
. . . . 5
β’
((βπ₯ β
On π« π₯ β dom
card β§ π§ β On)
β (π¦ β
(π
1βsuc π§) β π¦ β dom card)) |
71 | 70 | rexlimdva 3149 |
. . . 4
β’
(βπ₯ β On
π« π₯ β dom card
β (βπ§ β On
π¦ β
(π
1βsuc π§) β π¦ β dom card)) |
72 | 1, 71 | biimtrid 241 |
. . 3
β’
(βπ₯ β On
π« π₯ β dom card
β (π¦ β βͺ (π
1 β On) β π¦ β dom
card)) |
73 | 72 | ssrdv 3951 |
. 2
β’
(βπ₯ β On
π« π₯ β dom card
β βͺ (π
1 β On) β
dom card) |
74 | | onwf 9771 |
. . . . . 6
β’ On
β βͺ (π
1 β
On) |
75 | 74 | sseli 3941 |
. . . . 5
β’ (π₯ β On β π₯ β βͺ (π
1 β On)) |
76 | | pwwf 9748 |
. . . . 5
β’ (π₯ β βͺ (π
1 β On) β π«
π₯ β βͺ (π
1 β On)) |
77 | 75, 76 | sylib 217 |
. . . 4
β’ (π₯ β On β π«
π₯ β βͺ (π
1 β On)) |
78 | | ssel 3938 |
. . . 4
β’ (βͺ (π
1 β On) β dom card
β (π« π₯ β
βͺ (π
1 β On) β
π« π₯ β dom
card)) |
79 | 77, 78 | syl5 34 |
. . 3
β’ (βͺ (π
1 β On) β dom card
β (π₯ β On β
π« π₯ β dom
card)) |
80 | 79 | ralrimiv 3139 |
. 2
β’ (βͺ (π
1 β On) β dom card
β βπ₯ β On
π« π₯ β dom
card) |
81 | 73, 80 | impbii 208 |
1
β’
(βπ₯ β On
π« π₯ β dom card
β βͺ (π
1 β On) β
dom card) |