Step | Hyp | Ref
| Expression |
1 | | aomclem5.f |
. . . . . 6
β’ πΉ = {β¨π, πβ© β£ ((rankβπ) E (rankβπ) β¨ ((rankβπ) = (rankβπ) β§ π(π§βsuc (rankβπ))π))} |
2 | | aomclem5.on |
. . . . . . 7
β’ (π β dom π§ β On) |
3 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ dom π§ = βͺ dom π§) β dom π§ β On) |
4 | | simpr 486 |
. . . . . 6
β’ ((π β§ dom π§ = βͺ dom π§) β dom π§ = βͺ dom π§) |
5 | | aomclem5.we |
. . . . . . 7
β’ (π β βπ β dom π§(π§βπ) We (π
1βπ)) |
6 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ dom π§ = βͺ dom π§) β βπ β dom π§(π§βπ) We (π
1βπ)) |
7 | 1, 3, 4, 6 | aomclem4 41413 |
. . . . 5
β’ ((π β§ dom π§ = βͺ dom π§) β πΉ We (π
1βdom π§)) |
8 | | iftrue 4497 |
. . . . . . 7
β’ (dom
π§ = βͺ dom π§ β if(dom π§ = βͺ dom π§, πΉ, πΈ) = πΉ) |
9 | 8 | adantl 483 |
. . . . . 6
β’ ((π β§ dom π§ = βͺ dom π§) β if(dom π§ = βͺ
dom π§, πΉ, πΈ) = πΉ) |
10 | | eqidd 2738 |
. . . . . 6
β’ ((π β§ dom π§ = βͺ dom π§) β
(π
1βdom π§) = (π
1βdom π§)) |
11 | 9, 10 | weeq12d 41396 |
. . . . 5
β’ ((π β§ dom π§ = βͺ dom π§) β (if(dom π§ = βͺ
dom π§, πΉ, πΈ) We (π
1βdom π§) β πΉ We (π
1βdom π§))) |
12 | 7, 11 | mpbird 257 |
. . . 4
β’ ((π β§ dom π§ = βͺ dom π§) β if(dom π§ = βͺ
dom π§, πΉ, πΈ) We (π
1βdom π§)) |
13 | | aomclem5.b |
. . . . . 6
β’ π΅ = {β¨π, πβ© β£ βπ β (π
1ββͺ dom π§)((π β π β§ Β¬ π β π) β§ βπ β (π
1ββͺ dom π§)(π(π§ββͺ dom π§)π β (π β π β π β π)))} |
14 | | aomclem5.c |
. . . . . 6
β’ πΆ = (π β V β¦ sup((π¦βπ), (π
1βdom π§), π΅)) |
15 | | aomclem5.d |
. . . . . 6
β’ π· = recs((π β V β¦ (πΆβ((π
1βdom
π§) β ran π)))) |
16 | | aomclem5.e |
. . . . . 6
β’ πΈ = {β¨π, πβ© β£ β©
(β‘π· β {π}) β β© (β‘π· β {π})} |
17 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ dom π§ = βͺ
dom π§) β dom π§ β On) |
18 | | eloni 6332 |
. . . . . . . 8
β’ (dom
π§ β On β Ord dom
π§) |
19 | | orduniorsuc 7770 |
. . . . . . . 8
β’ (Ord dom
π§ β (dom π§ = βͺ
dom π§ β¨ dom π§ = suc βͺ dom π§)) |
20 | 2, 18, 19 | 3syl 18 |
. . . . . . 7
β’ (π β (dom π§ = βͺ dom π§ β¨ dom π§ = suc βͺ dom π§)) |
21 | 20 | orcanai 1002 |
. . . . . 6
β’ ((π β§ Β¬ dom π§ = βͺ
dom π§) β dom π§ = suc βͺ dom π§) |
22 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ dom π§ = βͺ
dom π§) β βπ β dom π§(π§βπ) We (π
1βπ)) |
23 | | aomclem5.a |
. . . . . . 7
β’ (π β π΄ β On) |
24 | 23 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ dom π§ = βͺ
dom π§) β π΄ β On) |
25 | | aomclem5.za |
. . . . . . 7
β’ (π β dom π§ β π΄) |
26 | 25 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ dom π§ = βͺ
dom π§) β dom π§ β π΄) |
27 | | aomclem5.y |
. . . . . . 7
β’ (π β βπ β π«
(π
1βπ΄)(π β β
β (π¦βπ) β ((π« π β© Fin) β
{β
}))) |
28 | 27 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ dom π§ = βͺ
dom π§) β βπ β π«
(π
1βπ΄)(π β β
β (π¦βπ) β ((π« π β© Fin) β
{β
}))) |
29 | 13, 14, 15, 16, 17, 21, 22, 24, 26, 28 | aomclem3 41412 |
. . . . 5
β’ ((π β§ Β¬ dom π§ = βͺ
dom π§) β πΈ We
(π
1βdom π§)) |
30 | | iffalse 4500 |
. . . . . . 7
β’ (Β¬
dom π§ = βͺ dom π§ β if(dom π§ = βͺ dom π§, πΉ, πΈ) = πΈ) |
31 | 30 | adantl 483 |
. . . . . 6
β’ ((π β§ Β¬ dom π§ = βͺ
dom π§) β if(dom π§ = βͺ
dom π§, πΉ, πΈ) = πΈ) |
32 | | eqidd 2738 |
. . . . . 6
β’ ((π β§ Β¬ dom π§ = βͺ
dom π§) β
(π
1βdom π§) = (π
1βdom π§)) |
33 | 31, 32 | weeq12d 41396 |
. . . . 5
β’ ((π β§ Β¬ dom π§ = βͺ
dom π§) β (if(dom π§ = βͺ
dom π§, πΉ, πΈ) We (π
1βdom π§) β πΈ We (π
1βdom π§))) |
34 | 29, 33 | mpbird 257 |
. . . 4
β’ ((π β§ Β¬ dom π§ = βͺ
dom π§) β if(dom π§ = βͺ
dom π§, πΉ, πΈ) We (π
1βdom π§)) |
35 | 12, 34 | pm2.61dan 812 |
. . 3
β’ (π β if(dom π§ = βͺ dom π§, πΉ, πΈ) We (π
1βdom π§)) |
36 | | weinxp 5721 |
. . 3
β’ (if(dom
π§ = βͺ dom π§, πΉ, πΈ) We (π
1βdom π§) β (if(dom π§ = βͺ
dom π§, πΉ, πΈ) β© ((π
1βdom
π§) Γ
(π
1βdom π§))) We (π
1βdom π§)) |
37 | 35, 36 | sylib 217 |
. 2
β’ (π β (if(dom π§ = βͺ dom π§, πΉ, πΈ) β© ((π
1βdom
π§) Γ
(π
1βdom π§))) We (π
1βdom π§)) |
38 | | aomclem5.g |
. . 3
β’ πΊ = (if(dom π§ = βͺ dom π§, πΉ, πΈ) β© ((π
1βdom
π§) Γ
(π
1βdom π§))) |
39 | | weeq1 5626 |
. . 3
β’ (πΊ = (if(dom π§ = βͺ dom π§, πΉ, πΈ) β© ((π
1βdom
π§) Γ
(π
1βdom π§))) β (πΊ We (π
1βdom π§) β (if(dom π§ = βͺ
dom π§, πΉ, πΈ) β© ((π
1βdom
π§) Γ
(π
1βdom π§))) We (π
1βdom π§))) |
40 | 38, 39 | ax-mp 5 |
. 2
β’ (πΊ We
(π
1βdom π§) β (if(dom π§ = βͺ dom π§, πΉ, πΈ) β© ((π
1βdom
π§) Γ
(π
1βdom π§))) We (π
1βdom π§)) |
41 | 37, 40 | sylibr 233 |
1
β’ (π β πΊ We (π
1βdom π§)) |