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 )