Step | Hyp | Ref
| Expression |
1 | | sseq2 3971 |
. . . . . 6
β’ (π¦ = π β (πΆ β π¦ β πΆ β π)) |
2 | | fveq2 6843 |
. . . . . . 7
β’ (π¦ = π β (πΊβπ¦) = (πΊβπ)) |
3 | 2 | sseq2d 3977 |
. . . . . 6
β’ (π¦ = π β ((πΊβπΆ) β (πΊβπ¦) β (πΊβπΆ) β (πΊβπ))) |
4 | 1, 3 | imbi12d 345 |
. . . . 5
β’ (π¦ = π β ((πΆ β π¦ β (πΊβπΆ) β (πΊβπ¦)) β (πΆ β π β (πΊβπΆ) β (πΊβπ)))) |
5 | 4 | imbi2d 341 |
. . . 4
β’ (π¦ = π β (((π β§ πΆ β On) β (πΆ β π¦ β (πΊβπΆ) β (πΊβπ¦))) β ((π β§ πΆ β On) β (πΆ β π β (πΊβπΆ) β (πΊβπ))))) |
6 | | sseq2 3971 |
. . . . . 6
β’ (π¦ = π· β (πΆ β π¦ β πΆ β π·)) |
7 | | fveq2 6843 |
. . . . . . 7
β’ (π¦ = π· β (πΊβπ¦) = (πΊβπ·)) |
8 | 7 | sseq2d 3977 |
. . . . . 6
β’ (π¦ = π· β ((πΊβπΆ) β (πΊβπ¦) β (πΊβπΆ) β (πΊβπ·))) |
9 | 6, 8 | imbi12d 345 |
. . . . 5
β’ (π¦ = π· β ((πΆ β π¦ β (πΊβπΆ) β (πΊβπ¦)) β (πΆ β π· β (πΊβπΆ) β (πΊβπ·)))) |
10 | 9 | imbi2d 341 |
. . . 4
β’ (π¦ = π· β (((π β§ πΆ β On) β (πΆ β π¦ β (πΊβπΆ) β (πΊβπ¦))) β ((π β§ πΆ β On) β (πΆ β π· β (πΊβπΆ) β (πΊβπ·))))) |
11 | | r19.21v 3177 |
. . . . 5
β’
(βπ β
π¦ ((π β§ πΆ β On) β (πΆ β π β (πΊβπΆ) β (πΊβπ))) β ((π β§ πΆ β On) β βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)))) |
12 | | onsseleq 6359 |
. . . . . . . . . 10
β’ ((πΆ β On β§ π¦ β On) β (πΆ β π¦ β (πΆ β π¦ β¨ πΆ = π¦))) |
13 | 12 | ad4ant23 752 |
. . . . . . . . 9
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ))) β (πΆ β π¦ β (πΆ β π¦ β¨ πΆ = π¦))) |
14 | | sseq2 3971 |
. . . . . . . . . . . . 13
β’ (if(π¦ = β
, π΅, βͺ (πΊ β π¦)) = if(π¦ = βͺ π¦, if(π¦ = β
, π΅, βͺ (πΊ β π¦)), ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)}, β
))) β ((πΊβπΆ) β if(π¦ = β
, π΅, βͺ (πΊ β π¦)) β (πΊβπΆ) β if(π¦ = βͺ π¦, if(π¦ = β
, π΅, βͺ (πΊ β π¦)), ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)},
β
))))) |
15 | | sseq2 3971 |
. . . . . . . . . . . . 13
β’ (((πΊββͺ π¦)
βͺ if(((πΊββͺ π¦)
βͺ {(πΉββͺ π¦)})
β π΄, {(πΉββͺ π¦)},
β
)) = if(π¦ = βͺ π¦,
if(π¦ = β
, π΅, βͺ
(πΊ β π¦)), ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)}, β
))) β ((πΊβπΆ) β ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)}, β
)) β (πΊβπΆ) β if(π¦ = βͺ π¦, if(π¦ = β
, π΅, βͺ (πΊ β π¦)), ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)},
β
))))) |
16 | | ttukeylem.4 |
. . . . . . . . . . . . . . . . . 18
β’ πΊ = recs((π§ β V β¦ if(dom π§ = βͺ dom π§, if(dom π§ = β
, π΅, βͺ ran π§), ((π§ββͺ dom π§) βͺ if(((π§ββͺ dom π§) βͺ {(πΉββͺ dom
π§)}) β π΄, {(πΉββͺ dom
π§)},
β
))))) |
17 | 16 | tfr1 8344 |
. . . . . . . . . . . . . . . . 17
β’ πΊ Fn On |
18 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β π¦ β On) |
19 | | onss 7720 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β On β π¦ β On) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β π¦ β On) |
21 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β πΆ β π¦) |
22 | | fnfvima 7184 |
. . . . . . . . . . . . . . . . 17
β’ ((πΊ Fn On β§ π¦ β On β§ πΆ β π¦) β (πΊβπΆ) β (πΊ β π¦)) |
23 | 17, 20, 21, 22 | mp3an2i 1467 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β (πΊβπΆ) β (πΊ β π¦)) |
24 | | elssuni 4899 |
. . . . . . . . . . . . . . . 16
β’ ((πΊβπΆ) β (πΊ β π¦) β (πΊβπΆ) β βͺ
(πΊ β π¦)) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β (πΊβπΆ) β βͺ
(πΊ β π¦)) |
26 | | n0i 4294 |
. . . . . . . . . . . . . . . 16
β’ (πΆ β π¦ β Β¬ π¦ = β
) |
27 | | iffalse 4496 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π¦ = β
β if(π¦ = β
, π΅, βͺ (πΊ β π¦)) = βͺ (πΊ β π¦)) |
28 | 21, 26, 27 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β if(π¦ = β
, π΅, βͺ (πΊ β π¦)) = βͺ (πΊ β π¦)) |
29 | 25, 28 | sseqtrrd 3986 |
. . . . . . . . . . . . . 14
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β (πΊβπΆ) β if(π¦ = β
, π΅, βͺ (πΊ β π¦))) |
30 | 29 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β§ π¦ = βͺ π¦) β (πΊβπΆ) β if(π¦ = β
, π΅, βͺ (πΊ β π¦))) |
31 | 21 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β§ Β¬ π¦ = βͺ π¦) β πΆ β π¦) |
32 | | elssuni 4899 |
. . . . . . . . . . . . . . . 16
β’ (πΆ β π¦ β πΆ β βͺ π¦) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β§ Β¬ π¦ = βͺ π¦) β πΆ β βͺ π¦) |
34 | | sseq2 3971 |
. . . . . . . . . . . . . . . . 17
β’ (π = βͺ
π¦ β (πΆ β π β πΆ β βͺ π¦)) |
35 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . 18
β’ (π = βͺ
π¦ β (πΊβπ) = (πΊββͺ π¦)) |
36 | 35 | sseq2d 3977 |
. . . . . . . . . . . . . . . . 17
β’ (π = βͺ
π¦ β ((πΊβπΆ) β (πΊβπ) β (πΊβπΆ) β (πΊββͺ π¦))) |
37 | 34, 36 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
β’ (π = βͺ
π¦ β ((πΆ β π β (πΊβπΆ) β (πΊβπ)) β (πΆ β βͺ π¦ β (πΊβπΆ) β (πΊββͺ π¦)))) |
38 | | simplrl 776 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β§ Β¬ π¦ = βͺ π¦) β βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ))) |
39 | | vuniex 7677 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ π¦
β V |
40 | 39 | sucid 6400 |
. . . . . . . . . . . . . . . . 17
β’ βͺ π¦
β suc βͺ π¦ |
41 | | eloni 6328 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β On β Ord π¦) |
42 | | orduniorsuc 7766 |
. . . . . . . . . . . . . . . . . . 19
β’ (Ord
π¦ β (π¦ = βͺ
π¦ β¨ π¦ = suc βͺ π¦)) |
43 | 18, 41, 42 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β (π¦ = βͺ π¦ β¨ π¦ = suc βͺ π¦)) |
44 | 43 | orcanai 1002 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β§ Β¬ π¦ = βͺ π¦) β π¦ = suc βͺ π¦) |
45 | 40, 44 | eleqtrrid 2845 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β§ Β¬ π¦ = βͺ π¦) β βͺ π¦
β π¦) |
46 | 37, 38, 45 | rspcdva 3583 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β§ Β¬ π¦ = βͺ π¦) β (πΆ β βͺ π¦ β (πΊβπΆ) β (πΊββͺ π¦))) |
47 | 33, 46 | mpd 15 |
. . . . . . . . . . . . . 14
β’
(((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β§ Β¬ π¦ = βͺ π¦) β (πΊβπΆ) β (πΊββͺ π¦)) |
48 | | ssun1 4133 |
. . . . . . . . . . . . . 14
β’ (πΊββͺ π¦)
β ((πΊββͺ π¦)
βͺ if(((πΊββͺ π¦)
βͺ {(πΉββͺ π¦)})
β π΄, {(πΉββͺ π¦)},
β
)) |
49 | 47, 48 | sstrdi 3957 |
. . . . . . . . . . . . 13
β’
(((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β§ Β¬ π¦ = βͺ π¦) β (πΊβπΆ) β ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)}, β
))) |
50 | 14, 15, 30, 49 | ifbothda 4525 |
. . . . . . . . . . . 12
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β (πΊβπΆ) β if(π¦ = βͺ π¦, if(π¦ = β
, π΅, βͺ (πΊ β π¦)), ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)}, β
)))) |
51 | | ttukeylem.1 |
. . . . . . . . . . . . . 14
β’ (π β πΉ:(cardβ(βͺ
π΄ β π΅))β1-1-ontoβ(βͺ π΄ β π΅)) |
52 | | ttukeylem.2 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β π΄) |
53 | | ttukeylem.3 |
. . . . . . . . . . . . . 14
β’ (π β βπ₯(π₯ β π΄ β (π« π₯ β© Fin) β π΄)) |
54 | 51, 52, 53, 16 | ttukeylem3 10448 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β On) β (πΊβπ¦) = if(π¦ = βͺ π¦, if(π¦ = β
, π΅, βͺ (πΊ β π¦)), ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)}, β
)))) |
55 | 54 | ad4ant13 750 |
. . . . . . . . . . . 12
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β (πΊβπ¦) = if(π¦ = βͺ π¦, if(π¦ = β
, π΅, βͺ (πΊ β π¦)), ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)}, β
)))) |
56 | 50, 55 | sseqtrrd 3986 |
. . . . . . . . . . 11
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β§ πΆ β π¦)) β (πΊβπΆ) β (πΊβπ¦)) |
57 | 56 | expr 458 |
. . . . . . . . . 10
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ))) β (πΆ β π¦ β (πΊβπΆ) β (πΊβπ¦))) |
58 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (πΆ = π¦ β (πΊβπΆ) = (πΊβπ¦)) |
59 | | eqimss 4001 |
. . . . . . . . . . . 12
β’ ((πΊβπΆ) = (πΊβπ¦) β (πΊβπΆ) β (πΊβπ¦)) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . 11
β’ (πΆ = π¦ β (πΊβπΆ) β (πΊβπ¦)) |
61 | 60 | a1i 11 |
. . . . . . . . . 10
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ))) β (πΆ = π¦ β (πΊβπΆ) β (πΊβπ¦))) |
62 | 57, 61 | jaod 858 |
. . . . . . . . 9
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ))) β ((πΆ β π¦ β¨ πΆ = π¦) β (πΊβπΆ) β (πΊβπ¦))) |
63 | 13, 62 | sylbid 239 |
. . . . . . . 8
β’ ((((π β§ πΆ β On) β§ π¦ β On) β§ βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ))) β (πΆ β π¦ β (πΊβπΆ) β (πΊβπ¦))) |
64 | 63 | ex 414 |
. . . . . . 7
β’ (((π β§ πΆ β On) β§ π¦ β On) β (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β (πΆ β π¦ β (πΊβπΆ) β (πΊβπ¦)))) |
65 | 64 | expcom 415 |
. . . . . 6
β’ (π¦ β On β ((π β§ πΆ β On) β (βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ)) β (πΆ β π¦ β (πΊβπΆ) β (πΊβπ¦))))) |
66 | 65 | a2d 29 |
. . . . 5
β’ (π¦ β On β (((π β§ πΆ β On) β βπ β π¦ (πΆ β π β (πΊβπΆ) β (πΊβπ))) β ((π β§ πΆ β On) β (πΆ β π¦ β (πΊβπΆ) β (πΊβπ¦))))) |
67 | 11, 66 | biimtrid 241 |
. . . 4
β’ (π¦ β On β (βπ β π¦ ((π β§ πΆ β On) β (πΆ β π β (πΊβπΆ) β (πΊβπ))) β ((π β§ πΆ β On) β (πΆ β π¦ β (πΊβπΆ) β (πΊβπ¦))))) |
68 | 5, 10, 67 | tfis3 7795 |
. . 3
β’ (π· β On β ((π β§ πΆ β On) β (πΆ β π· β (πΊβπΆ) β (πΊβπ·)))) |
69 | 68 | expdcom 416 |
. 2
β’ (π β (πΆ β On β (π· β On β (πΆ β π· β (πΊβπΆ) β (πΊβπ·))))) |
70 | 69 | 3imp2 1350 |
1
β’ ((π β§ (πΆ β On β§ π· β On β§ πΆ β π·)) β (πΊβπΆ) β (πΊβπ·)) |