Metamath Proof Explorer

Theorem dnnumch1

Description: Define an enumeration of a set from a choice function; second part, it restricts to a bijection.EDITORIAL: overlaps dfac8a . (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypotheses dnnumch.f 
|- F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )
dnnumch.a 
|- ( ph -> A e. V )
dnnumch.g 
|- ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )
Assertion dnnumch1 
|- ( ph -> E. x e. On ( F |` x ) : x -1-1-onto-> A )

Proof

Step Hyp Ref Expression
1 dnnumch.f 
 |-  F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )
2 dnnumch.a 
 |-  ( ph -> A e. V )
3 dnnumch.g 
 |-  ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )
4 recsval 
 |-  ( x e. On -> ( recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) ) ` x ) = ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) ` ( recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) ) |` x ) ) )
5 1 fveq1i 
 |-  ( F ` x ) = ( recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) ) ` x )
6 1 tfr1 
 |-  F Fn On
7 fnfun 
 |-  ( F Fn On -> Fun F )
8 6 7 ax-mp 
 |-  Fun F
9 vex 
 |-  x e. _V
10 resfunexg 
 |-  ( ( Fun F /\ x e. _V ) -> ( F |` x ) e. _V )
11 8 9 10 mp2an 
 |-  ( F |` x ) e. _V
12 rneq 
 |-  ( w = ( F |` x ) -> ran w = ran ( F |` x ) )
13 df-ima 
 |-  ( F " x ) = ran ( F |` x )
14 12 13 eqtr4di 
 |-  ( w = ( F |` x ) -> ran w = ( F " x ) )
15 14 difeq2d 
 |-  ( w = ( F |` x ) -> ( A \ ran w ) = ( A \ ( F " x ) ) )
16 15 fveq2d 
 |-  ( w = ( F |` x ) -> ( G ` ( A \ ran w ) ) = ( G ` ( A \ ( F " x ) ) ) )
17 rneq 
 |-  ( z = w -> ran z = ran w )
18 17 difeq2d 
 |-  ( z = w -> ( A \ ran z ) = ( A \ ran w ) )
19 18 fveq2d 
 |-  ( z = w -> ( G ` ( A \ ran z ) ) = ( G ` ( A \ ran w ) ) )
20 19 cbvmptv 
 |-  ( z e. _V |-> ( G ` ( A \ ran z ) ) ) = ( w e. _V |-> ( G ` ( A \ ran w ) ) )
21 fvex 
 |-  ( G ` ( A \ ( F " x ) ) ) e. _V
22 16 20 21 fvmpt 
 |-  ( ( F |` x ) e. _V -> ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) ` ( F |` x ) ) = ( G ` ( A \ ( F " x ) ) ) )
23 11 22 ax-mp 
 |-  ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) ` ( F |` x ) ) = ( G ` ( A \ ( F " x ) ) )
24 1 reseq1i 
 |-  ( F |` x ) = ( recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) ) |` x )
25 24 fveq2i 
 |-  ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) ` ( F |` x ) ) = ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) ` ( recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) ) |` x ) )
26 23 25 eqtr3i 
 |-  ( G ` ( A \ ( F " x ) ) ) = ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) ` ( recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) ) |` x ) )
27 4 5 26 3eqtr4g 
 |-  ( x e. On -> ( F ` x ) = ( G ` ( A \ ( F " x ) ) ) )
28 27 ad2antlr 
 |-  ( ( ( ph /\ x e. On ) /\ ( A \ ( F " x ) ) =/= (/) ) -> ( F ` x ) = ( G ` ( A \ ( F " x ) ) ) )
29 difss 
 |-  ( A \ ( F " x ) ) C_ A
30 elpw2g 
 |-  ( A e. V -> ( ( A \ ( F " x ) ) e. ~P A <-> ( A \ ( F " x ) ) C_ A ) )
31 2 30 syl 
 |-  ( ph -> ( ( A \ ( F " x ) ) e. ~P A <-> ( A \ ( F " x ) ) C_ A ) )
32 29 31 mpbiri 
 |-  ( ph -> ( A \ ( F " x ) ) e. ~P A )
33 neeq1 
 |-  ( y = ( A \ ( F " x ) ) -> ( y =/= (/) <-> ( A \ ( F " x ) ) =/= (/) ) )
34 fveq2 
 |-  ( y = ( A \ ( F " x ) ) -> ( G ` y ) = ( G ` ( A \ ( F " x ) ) ) )
35 id 
 |-  ( y = ( A \ ( F " x ) ) -> y = ( A \ ( F " x ) ) )
36 34 35 eleq12d 
 |-  ( y = ( A \ ( F " x ) ) -> ( ( G ` y ) e. y <-> ( G ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) )
37 33 36 imbi12d 
 |-  ( y = ( A \ ( F " x ) ) -> ( ( y =/= (/) -> ( G ` y ) e. y ) <-> ( ( A \ ( F " x ) ) =/= (/) -> ( G ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) ) )
38 37 rspcva 
 |-  ( ( ( A \ ( F " x ) ) e. ~P A /\ A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) ) -> ( ( A \ ( F " x ) ) =/= (/) -> ( G ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) )
39 32 3 38 syl2anc 
 |-  ( ph -> ( ( A \ ( F " x ) ) =/= (/) -> ( G ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) )
40 39 adantr 
 |-  ( ( ph /\ x e. On ) -> ( ( A \ ( F " x ) ) =/= (/) -> ( G ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) )
41 40 imp 
 |-  ( ( ( ph /\ x e. On ) /\ ( A \ ( F " x ) ) =/= (/) ) -> ( G ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) )
42 28 41 eqeltrd 
 |-  ( ( ( ph /\ x e. On ) /\ ( A \ ( F " x ) ) =/= (/) ) -> ( F ` x ) e. ( A \ ( F " x ) ) )
43 42 ex 
 |-  ( ( ph /\ x e. On ) -> ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) )
44 43 ralrimiva 
 |-  ( ph -> A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) )
45 6 tz7.49c 
 |-  ( ( A e. V /\ A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) ) -> E. x e. On ( F |` x ) : x -1-1-onto-> A )
46 2 44 45 syl2anc 
 |-  ( ph -> E. x e. On ( F |` x ) : x -1-1-onto-> A )