| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ttukeylem.1 |
|- ( ph -> F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) ) |
| 2 |
|
ttukeylem.2 |
|- ( ph -> B e. A ) |
| 3 |
|
ttukeylem.3 |
|- ( ph -> A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) ) |
| 4 |
|
ttukeylem.4 |
|- G = recs ( ( z e. _V |-> if ( dom z = U. dom z , if ( dom z = (/) , B , U. ran z ) , ( ( z ` U. dom z ) u. if ( ( ( z ` U. dom z ) u. { ( F ` U. dom z ) } ) e. A , { ( F ` U. dom z ) } , (/) ) ) ) ) ) |
| 5 |
|
0elon |
|- (/) e. On |
| 6 |
1 2 3 4
|
ttukeylem3 |
|- ( ( ph /\ (/) e. On ) -> ( G ` (/) ) = if ( (/) = U. (/) , if ( (/) = (/) , B , U. ( G " (/) ) ) , ( ( G ` U. (/) ) u. if ( ( ( G ` U. (/) ) u. { ( F ` U. (/) ) } ) e. A , { ( F ` U. (/) ) } , (/) ) ) ) ) |
| 7 |
5 6
|
mpan2 |
|- ( ph -> ( G ` (/) ) = if ( (/) = U. (/) , if ( (/) = (/) , B , U. ( G " (/) ) ) , ( ( G ` U. (/) ) u. if ( ( ( G ` U. (/) ) u. { ( F ` U. (/) ) } ) e. A , { ( F ` U. (/) ) } , (/) ) ) ) ) |
| 8 |
|
uni0 |
|- U. (/) = (/) |
| 9 |
8
|
eqcomi |
|- (/) = U. (/) |
| 10 |
9
|
iftruei |
|- if ( (/) = U. (/) , if ( (/) = (/) , B , U. ( G " (/) ) ) , ( ( G ` U. (/) ) u. if ( ( ( G ` U. (/) ) u. { ( F ` U. (/) ) } ) e. A , { ( F ` U. (/) ) } , (/) ) ) ) = if ( (/) = (/) , B , U. ( G " (/) ) ) |
| 11 |
|
eqid |
|- (/) = (/) |
| 12 |
11
|
iftruei |
|- if ( (/) = (/) , B , U. ( G " (/) ) ) = B |
| 13 |
10 12
|
eqtri |
|- if ( (/) = U. (/) , if ( (/) = (/) , B , U. ( G " (/) ) ) , ( ( G ` U. (/) ) u. if ( ( ( G ` U. (/) ) u. { ( F ` U. (/) ) } ) e. A , { ( F ` U. (/) ) } , (/) ) ) ) = B |
| 14 |
7 13
|
eqtrdi |
|- ( ph -> ( G ` (/) ) = B ) |