Theorem acnlem

Description: Construct a mapping satisfying the consequent of isacn . (Contributed by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	acnlem	|- ( ( A e. V /\ A. x e. A B e. ( f ` x ) ) -> E. g A. x e. A ( g ` x ) e. ( f ` x ) )

Proof

Step	Hyp	Ref	Expression
1		fvssunirn	|- ( f ` x ) C_ U. ran f
2		simpr	|- ( ( x e. A /\ B e. ( f ` x ) ) -> B e. ( f ` x ) )
3	1 2	sseldi	|- ( ( x e. A /\ B e. ( f ` x ) ) -> B e. U. ran f )
4	3	ralimiaa	|- ( A. x e. A B e. ( f ` x ) -> A. x e. A B e. U. ran f )
5		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
6	5	fmpt	|- ( A. x e. A B e. U. ran f <-> ( x e. A |-> B ) : A --> U. ran f )
7	4 6	sylib	|- ( A. x e. A B e. ( f ` x ) -> ( x e. A |-> B ) : A --> U. ran f )
8		id	|- ( A e. V -> A e. V )
9		vex	|- f e. _V
10	9	rnex	|- ran f e. _V
11	10	uniex	|- U. ran f e. _V
12		fex2	|- ( ( ( x e. A |-> B ) : A --> U. ran f /\ A e. V /\ U. ran f e. _V ) -> ( x e. A |-> B ) e. _V )
13	11 12	mp3an3	|- ( ( ( x e. A |-> B ) : A --> U. ran f /\ A e. V ) -> ( x e. A |-> B ) e. _V )
14	7 8 13	syl2anr	|- ( ( A e. V /\ A. x e. A B e. ( f ` x ) ) -> ( x e. A |-> B ) e. _V )
15	5	fvmpt2	|- ( ( x e. A /\ B e. ( f ` x ) ) -> ( ( x e. A |-> B ) ` x ) = B )
16	15 2	eqeltrd	|- ( ( x e. A /\ B e. ( f ` x ) ) -> ( ( x e. A |-> B ) ` x ) e. ( f ` x ) )
17	16	ralimiaa	|- ( A. x e. A B e. ( f ` x ) -> A. x e. A ( ( x e. A |-> B ) ` x ) e. ( f ` x ) )
18	17	adantl	|- ( ( A e. V /\ A. x e. A B e. ( f ` x ) ) -> A. x e. A ( ( x e. A |-> B ) ` x ) e. ( f ` x ) )
19		nfmpt1	|- F/_ x ( x e. A |-> B )
20	19	nfeq2	|- F/ x g = ( x e. A |-> B )
21		fveq1	|- ( g = ( x e. A |-> B ) -> ( g ` x ) = ( ( x e. A |-> B ) ` x ) )
22	21	eleq1d	|- ( g = ( x e. A |-> B ) -> ( ( g ` x ) e. ( f ` x ) <-> ( ( x e. A |-> B ) ` x ) e. ( f ` x ) ) )
23	20 22	ralbid	|- ( g = ( x e. A |-> B ) -> ( A. x e. A ( g ` x ) e. ( f ` x ) <-> A. x e. A ( ( x e. A |-> B ) ` x ) e. ( f ` x ) ) )
24	14 18 23	spcedv	|- ( ( A e. V /\ A. x e. A B e. ( f ` x ) ) -> E. g A. x e. A ( g ` x ) e. ( f ` x ) )