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