This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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