Step | Hyp | Ref
| Expression |
1 | | ttukeylem.4 |
. . . 4
β’ πΊ = recs((π§ β V β¦ if(dom π§ = βͺ dom π§, if(dom π§ = β
, π΅, βͺ ran π§), ((π§ββͺ dom π§) βͺ if(((π§ββͺ dom π§) βͺ {(πΉββͺ dom
π§)}) β π΄, {(πΉββͺ dom
π§)},
β
))))) |
2 | 1 | tfr2 8345 |
. . 3
β’ (πΆ β On β (πΊβπΆ) = ((π§ β V β¦ if(dom π§ = βͺ dom π§, if(dom π§ = β
, π΅, βͺ ran π§), ((π§ββͺ dom π§) βͺ if(((π§ββͺ dom π§) βͺ {(πΉββͺ dom
π§)}) β π΄, {(πΉββͺ dom
π§)},
β
))))β(πΊ
βΎ πΆ))) |
3 | 2 | adantl 483 |
. 2
β’ ((π β§ πΆ β On) β (πΊβπΆ) = ((π§ β V β¦ if(dom π§ = βͺ dom π§, if(dom π§ = β
, π΅, βͺ ran π§), ((π§ββͺ dom π§) βͺ if(((π§ββͺ dom π§) βͺ {(πΉββͺ dom
π§)}) β π΄, {(πΉββͺ dom
π§)},
β
))))β(πΊ
βΎ πΆ))) |
4 | | eqidd 2738 |
. . 3
β’ ((π β§ πΆ β On) β (π§ β V β¦ if(dom π§ = βͺ dom π§, if(dom π§ = β
, π΅, βͺ ran π§), ((π§ββͺ dom π§) βͺ if(((π§ββͺ dom π§) βͺ {(πΉββͺ dom
π§)}) β π΄, {(πΉββͺ dom
π§)}, β
)))) = (π§ β V β¦ if(dom π§ = βͺ
dom π§, if(dom π§ = β
, π΅, βͺ ran π§), ((π§ββͺ dom π§) βͺ if(((π§ββͺ dom π§) βͺ {(πΉββͺ dom
π§)}) β π΄, {(πΉββͺ dom
π§)},
β
))))) |
5 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β π§ = (πΊ βΎ πΆ)) |
6 | 5 | dmeqd 5862 |
. . . . . . 7
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β dom π§ = dom (πΊ βΎ πΆ)) |
7 | 1 | tfr1 8344 |
. . . . . . . . 9
β’ πΊ Fn On |
8 | | onss 7720 |
. . . . . . . . . 10
β’ (πΆ β On β πΆ β On) |
9 | 8 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β πΆ β On) |
10 | | fnssres 6625 |
. . . . . . . . 9
β’ ((πΊ Fn On β§ πΆ β On) β (πΊ βΎ πΆ) Fn πΆ) |
11 | 7, 9, 10 | sylancr 588 |
. . . . . . . 8
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β (πΊ βΎ πΆ) Fn πΆ) |
12 | 11 | fndmd 6608 |
. . . . . . 7
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β dom (πΊ βΎ πΆ) = πΆ) |
13 | 6, 12 | eqtrd 2777 |
. . . . . 6
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β dom π§ = πΆ) |
14 | 13 | unieqd 4880 |
. . . . . 6
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β βͺ dom
π§ = βͺ πΆ) |
15 | 13, 14 | eqeq12d 2753 |
. . . . 5
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β (dom π§ = βͺ dom π§ β πΆ = βͺ πΆ)) |
16 | 13 | eqeq1d 2739 |
. . . . . 6
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β (dom π§ = β
β πΆ = β
)) |
17 | 5 | rneqd 5894 |
. . . . . . . 8
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β ran π§ = ran (πΊ βΎ πΆ)) |
18 | | df-ima 5647 |
. . . . . . . 8
β’ (πΊ β πΆ) = ran (πΊ βΎ πΆ) |
19 | 17, 18 | eqtr4di 2795 |
. . . . . . 7
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β ran π§ = (πΊ β πΆ)) |
20 | 19 | unieqd 4880 |
. . . . . 6
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β βͺ ran
π§ = βͺ (πΊ
β πΆ)) |
21 | 16, 20 | ifbieq2d 4513 |
. . . . 5
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β if(dom π§ = β
, π΅, βͺ ran π§) = if(πΆ = β
, π΅, βͺ (πΊ β πΆ))) |
22 | 5, 14 | fveq12d 6850 |
. . . . . 6
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β (π§ββͺ dom π§) = ((πΊ βΎ πΆ)ββͺ πΆ)) |
23 | 14 | fveq2d 6847 |
. . . . . . . . . 10
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β (πΉββͺ dom
π§) = (πΉββͺ πΆ)) |
24 | 23 | sneqd 4599 |
. . . . . . . . 9
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β {(πΉββͺ dom
π§)} = {(πΉββͺ πΆ)}) |
25 | 22, 24 | uneq12d 4125 |
. . . . . . . 8
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β ((π§ββͺ dom π§) βͺ {(πΉββͺ dom
π§)}) = (((πΊ βΎ πΆ)ββͺ πΆ) βͺ {(πΉββͺ πΆ)})) |
26 | 25 | eleq1d 2823 |
. . . . . . 7
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β (((π§ββͺ dom π§) βͺ {(πΉββͺ dom
π§)}) β π΄ β (((πΊ βΎ πΆ)ββͺ πΆ) βͺ {(πΉββͺ πΆ)}) β π΄)) |
27 | | eqidd 2738 |
. . . . . . 7
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β β
=
β
) |
28 | 26, 24, 27 | ifbieq12d 4515 |
. . . . . 6
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β if(((π§ββͺ dom π§) βͺ {(πΉββͺ dom
π§)}) β π΄, {(πΉββͺ dom
π§)}, β
) = if((((πΊ βΎ πΆ)ββͺ πΆ) βͺ {(πΉββͺ πΆ)}) β π΄, {(πΉββͺ πΆ)}, β
)) |
29 | 22, 28 | uneq12d 4125 |
. . . . 5
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β ((π§ββͺ dom π§) βͺ if(((π§ββͺ dom π§) βͺ {(πΉββͺ dom
π§)}) β π΄, {(πΉββͺ dom
π§)}, β
)) = (((πΊ βΎ πΆ)ββͺ πΆ) βͺ if((((πΊ βΎ πΆ)ββͺ πΆ) βͺ {(πΉββͺ πΆ)}) β π΄, {(πΉββͺ πΆ)}, β
))) |
30 | 15, 21, 29 | ifbieq12d 4515 |
. . . 4
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β if(dom π§ = βͺ dom π§, if(dom π§ = β
, π΅, βͺ ran π§), ((π§ββͺ dom π§) βͺ if(((π§ββͺ dom π§) βͺ {(πΉββͺ dom
π§)}) β π΄, {(πΉββͺ dom
π§)}, β
))) = if(πΆ = βͺ
πΆ, if(πΆ = β
, π΅, βͺ (πΊ β πΆ)), (((πΊ βΎ πΆ)ββͺ πΆ) βͺ if((((πΊ βΎ πΆ)ββͺ πΆ) βͺ {(πΉββͺ πΆ)}) β π΄, {(πΉββͺ πΆ)}, β
)))) |
31 | | onuni 7724 |
. . . . . . . . . 10
β’ (πΆ β On β βͺ πΆ
β On) |
32 | 31 | ad3antlr 730 |
. . . . . . . . 9
β’ ((((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β§ Β¬ πΆ = βͺ πΆ) β βͺ πΆ
β On) |
33 | | sucidg 6399 |
. . . . . . . . 9
β’ (βͺ πΆ
β On β βͺ πΆ β suc βͺ
πΆ) |
34 | 32, 33 | syl 17 |
. . . . . . . 8
β’ ((((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β§ Β¬ πΆ = βͺ πΆ) β βͺ πΆ
β suc βͺ πΆ) |
35 | | eloni 6328 |
. . . . . . . . . . 11
β’ (πΆ β On β Ord πΆ) |
36 | 35 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β Ord πΆ) |
37 | | orduniorsuc 7766 |
. . . . . . . . . 10
β’ (Ord
πΆ β (πΆ = βͺ πΆ β¨ πΆ = suc βͺ πΆ)) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β (πΆ = βͺ πΆ β¨ πΆ = suc βͺ πΆ)) |
39 | 38 | orcanai 1002 |
. . . . . . . 8
β’ ((((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β§ Β¬ πΆ = βͺ πΆ) β πΆ = suc βͺ πΆ) |
40 | 34, 39 | eleqtrrd 2841 |
. . . . . . 7
β’ ((((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β§ Β¬ πΆ = βͺ πΆ) β βͺ πΆ
β πΆ) |
41 | 40 | fvresd 6863 |
. . . . . 6
β’ ((((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β§ Β¬ πΆ = βͺ πΆ) β ((πΊ βΎ πΆ)ββͺ πΆ) = (πΊββͺ πΆ)) |
42 | 41 | uneq1d 4123 |
. . . . . . . 8
β’ ((((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β§ Β¬ πΆ = βͺ πΆ) β (((πΊ βΎ πΆ)ββͺ πΆ) βͺ {(πΉββͺ πΆ)}) = ((πΊββͺ πΆ) βͺ {(πΉββͺ πΆ)})) |
43 | 42 | eleq1d 2823 |
. . . . . . 7
β’ ((((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β§ Β¬ πΆ = βͺ πΆ) β ((((πΊ βΎ πΆ)ββͺ πΆ) βͺ {(πΉββͺ πΆ)}) β π΄ β ((πΊββͺ πΆ) βͺ {(πΉββͺ πΆ)}) β π΄)) |
44 | 43 | ifbid 4510 |
. . . . . 6
β’ ((((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β§ Β¬ πΆ = βͺ πΆ) β if((((πΊ βΎ πΆ)ββͺ πΆ) βͺ {(πΉββͺ πΆ)}) β π΄, {(πΉββͺ πΆ)}, β
) = if(((πΊββͺ πΆ)
βͺ {(πΉββͺ πΆ)})
β π΄, {(πΉββͺ πΆ)},
β
)) |
45 | 41, 44 | uneq12d 4125 |
. . . . 5
β’ ((((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β§ Β¬ πΆ = βͺ πΆ) β (((πΊ βΎ πΆ)ββͺ πΆ) βͺ if((((πΊ βΎ πΆ)ββͺ πΆ) βͺ {(πΉββͺ πΆ)}) β π΄, {(πΉββͺ πΆ)}, β
)) = ((πΊββͺ πΆ)
βͺ if(((πΊββͺ πΆ)
βͺ {(πΉββͺ πΆ)})
β π΄, {(πΉββͺ πΆ)},
β
))) |
46 | 45 | ifeq2da 4519 |
. . . 4
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β if(πΆ = βͺ πΆ, if(πΆ = β
, π΅, βͺ (πΊ β πΆ)), (((πΊ βΎ πΆ)ββͺ πΆ) βͺ if((((πΊ βΎ πΆ)ββͺ πΆ) βͺ {(πΉββͺ πΆ)}) β π΄, {(πΉββͺ πΆ)}, β
))) = if(πΆ = βͺ
πΆ, if(πΆ = β
, π΅, βͺ (πΊ β πΆ)), ((πΊββͺ πΆ) βͺ if(((πΊββͺ πΆ) βͺ {(πΉββͺ πΆ)}) β π΄, {(πΉββͺ πΆ)}, β
)))) |
47 | 30, 46 | eqtrd 2777 |
. . 3
β’ (((π β§ πΆ β On) β§ π§ = (πΊ βΎ πΆ)) β if(dom π§ = βͺ dom π§, if(dom π§ = β
, π΅, βͺ ran π§), ((π§ββͺ dom π§) βͺ if(((π§ββͺ dom π§) βͺ {(πΉββͺ dom
π§)}) β π΄, {(πΉββͺ dom
π§)}, β
))) = if(πΆ = βͺ
πΆ, if(πΆ = β
, π΅, βͺ (πΊ β πΆ)), ((πΊββͺ πΆ) βͺ if(((πΊββͺ πΆ) βͺ {(πΉββͺ πΆ)}) β π΄, {(πΉββͺ πΆ)}, β
)))) |
48 | | fnfun 6603 |
. . . . 5
β’ (πΊ Fn On β Fun πΊ) |
49 | 7, 48 | ax-mp 5 |
. . . 4
β’ Fun πΊ |
50 | | simpr 486 |
. . . 4
β’ ((π β§ πΆ β On) β πΆ β On) |
51 | | resfunexg 7166 |
. . . 4
β’ ((Fun
πΊ β§ πΆ β On) β (πΊ βΎ πΆ) β V) |
52 | 49, 50, 51 | sylancr 588 |
. . 3
β’ ((π β§ πΆ β On) β (πΊ βΎ πΆ) β V) |
53 | | ttukeylem.2 |
. . . . . 6
β’ (π β π΅ β π΄) |
54 | 53 | elexd 3466 |
. . . . 5
β’ (π β π΅ β V) |
55 | | funimaexg 6588 |
. . . . . . 7
β’ ((Fun
πΊ β§ πΆ β On) β (πΊ β πΆ) β V) |
56 | 49, 55 | mpan 689 |
. . . . . 6
β’ (πΆ β On β (πΊ β πΆ) β V) |
57 | 56 | uniexd 7680 |
. . . . 5
β’ (πΆ β On β βͺ (πΊ
β πΆ) β
V) |
58 | | ifcl 4532 |
. . . . 5
β’ ((π΅ β V β§ βͺ (πΊ
β πΆ) β V) β
if(πΆ = β
, π΅, βͺ
(πΊ β πΆ)) β V) |
59 | 54, 57, 58 | syl2an 597 |
. . . 4
β’ ((π β§ πΆ β On) β if(πΆ = β
, π΅, βͺ (πΊ β πΆ)) β V) |
60 | | fvex 6856 |
. . . . 5
β’ (πΊββͺ πΆ)
β V |
61 | | snex 5389 |
. . . . . 6
β’ {(πΉββͺ πΆ)}
β V |
62 | | 0ex 5265 |
. . . . . 6
β’ β
β V |
63 | 61, 62 | ifex 4537 |
. . . . 5
β’
if(((πΊββͺ πΆ)
βͺ {(πΉββͺ πΆ)})
β π΄, {(πΉββͺ πΆ)},
β
) β V |
64 | 60, 63 | unex 7681 |
. . . 4
β’ ((πΊββͺ πΆ)
βͺ if(((πΊββͺ πΆ)
βͺ {(πΉββͺ πΆ)})
β π΄, {(πΉββͺ πΆ)},
β
)) β V |
65 | | ifcl 4532 |
. . . 4
β’
((if(πΆ = β
,
π΅, βͺ (πΊ
β πΆ)) β V β§
((πΊββͺ πΆ)
βͺ if(((πΊββͺ πΆ)
βͺ {(πΉββͺ πΆ)})
β π΄, {(πΉββͺ πΆ)},
β
)) β V) β if(πΆ = βͺ πΆ, if(πΆ = β
, π΅, βͺ (πΊ β πΆ)), ((πΊββͺ πΆ) βͺ if(((πΊββͺ πΆ) βͺ {(πΉββͺ πΆ)}) β π΄, {(πΉββͺ πΆ)}, β
))) β
V) |
66 | 59, 64, 65 | sylancl 587 |
. . 3
β’ ((π β§ πΆ β On) β if(πΆ = βͺ πΆ, if(πΆ = β
, π΅, βͺ (πΊ β πΆ)), ((πΊββͺ πΆ) βͺ if(((πΊββͺ πΆ) βͺ {(πΉββͺ πΆ)}) β π΄, {(πΉββͺ πΆ)}, β
))) β
V) |
67 | 4, 47, 52, 66 | fvmptd 6956 |
. 2
β’ ((π β§ πΆ β On) β ((π§ β V β¦ if(dom π§ = βͺ dom π§, if(dom π§ = β
, π΅, βͺ ran π§), ((π§ββͺ dom π§) βͺ if(((π§ββͺ dom π§) βͺ {(πΉββͺ dom
π§)}) β π΄, {(πΉββͺ dom
π§)},
β
))))β(πΊ
βΎ πΆ)) = if(πΆ = βͺ
πΆ, if(πΆ = β
, π΅, βͺ (πΊ β πΆ)), ((πΊββͺ πΆ) βͺ if(((πΊββͺ πΆ) βͺ {(πΉββͺ πΆ)}) β π΄, {(πΉββͺ πΆ)}, β
)))) |
68 | 3, 67 | eqtrd 2777 |
1
β’ ((π β§ πΆ β On) β (πΊβπΆ) = if(πΆ = βͺ πΆ, if(πΆ = β
, π΅, βͺ (πΊ β πΆ)), ((πΊββͺ πΆ) βͺ if(((πΊββͺ πΆ) βͺ {(πΉββͺ πΆ)}) β π΄, {(πΉββͺ πΆ)}, β
)))) |