Metamath Proof Explorer


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 sselid
 |-  ( ( 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 ) )