# Metamath Proof Explorer

## Theorem ttukeylem4

Description: Lemma for ttukey . (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Hypotheses ttukeylem.1
`|- ( ph -> F : ( card ` ( U. A \ B ) ) -1-1-onto-> ( U. A \ B ) )`
ttukeylem.2
`|- ( ph -> B e. A )`
ttukeylem.3
`|- ( ph -> A. x ( x e. A <-> ( ~P x i^i Fin ) C_ A ) )`
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 ) } , (/) ) ) ) ) )`
Assertion ttukeylem4
`|- ( ph -> ( G ` (/) ) = B )`

### Proof

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 syl6eq
` |-  ( ph -> ( G ` (/) ) = B )`