Metamath Proof Explorer

Theorem indexfi

Description: If for every element of a finite indexing set A there exists a corresponding element of another set B , then there exists a finite subset of B consisting only of those elements which are indexed by A . Proven without the Axiom of Choice, unlike indexdom . (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion indexfi 
|- ( ( A e. Fin /\ B e. M /\ A. x e. A E. y e. B ph ) -> E. c e. Fin ( c C_ B /\ A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ z ph
2 nfsbc1v 
 |-  F/ y [. z / y ]. ph
3 sbceq1a 
 |-  ( y = z -> ( ph <-> [. z / y ]. ph ) )
4 1 2 3 cbvrexw 
 |-  ( E. y e. B ph <-> E. z e. B [. z / y ]. ph )
5 4 ralbii 
 |-  ( A. x e. A E. y e. B ph <-> A. x e. A E. z e. B [. z / y ]. ph )
6 dfsbcq 
 |-  ( z = ( f ` x ) -> ( [. z / y ]. ph <-> [. ( f ` x ) / y ]. ph ) )
7 6 ac6sfi 
 |-  ( ( A e. Fin /\ A. x e. A E. z e. B [. z / y ]. ph ) -> E. f ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) )
8 5 7 sylan2b 
 |-  ( ( A e. Fin /\ A. x e. A E. y e. B ph ) -> E. f ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) )
9 simpll 
 |-  ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) -> A e. Fin )
10 ffn 
 |-  ( f : A --> B -> f Fn A )
11 10 ad2antrl 
 |-  ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) -> f Fn A )
12 dffn4 
 |-  ( f Fn A <-> f : A -onto-> ran f )
13 11 12 sylib 
 |-  ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) -> f : A -onto-> ran f )
14 fofi 
 |-  ( ( A e. Fin /\ f : A -onto-> ran f ) -> ran f e. Fin )
15 9 13 14 syl2anc 
 |-  ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) -> ran f e. Fin )
16 frn 
 |-  ( f : A --> B -> ran f C_ B )
17 16 ad2antrl 
 |-  ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) -> ran f C_ B )
18 fnfvelrn 
 |-  ( ( f Fn A /\ x e. A ) -> ( f ` x ) e. ran f )
19 10 18 sylan 
 |-  ( ( f : A --> B /\ x e. A ) -> ( f ` x ) e. ran f )
20 rspesbca 
 |-  ( ( ( f ` x ) e. ran f /\ [. ( f ` x ) / y ]. ph ) -> E. y e. ran f ph )
21 20 ex 
 |-  ( ( f ` x ) e. ran f -> ( [. ( f ` x ) / y ]. ph -> E. y e. ran f ph ) )
22 19 21 syl 
 |-  ( ( f : A --> B /\ x e. A ) -> ( [. ( f ` x ) / y ]. ph -> E. y e. ran f ph ) )
23 22 ralimdva 
 |-  ( f : A --> B -> ( A. x e. A [. ( f ` x ) / y ]. ph -> A. x e. A E. y e. ran f ph ) )
24 23 imp 
 |-  ( ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) -> A. x e. A E. y e. ran f ph )
25 24 adantl 
 |-  ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) -> A. x e. A E. y e. ran f ph )
26 simpr 
 |-  ( ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) /\ w e. A ) -> w e. A )
27 simprr 
 |-  ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) -> A. x e. A [. ( f ` x ) / y ]. ph )
28 nfv 
 |-  F/ w [. ( f ` x ) / y ]. ph
29 nfsbc1v 
 |-  F/ x [. w / x ]. [. ( f ` w ) / y ]. ph
30 fveq2 
 |-  ( x = w -> ( f ` x ) = ( f ` w ) )
31 30 sbceq1d 
 |-  ( x = w -> ( [. ( f ` x ) / y ]. ph <-> [. ( f ` w ) / y ]. ph ) )
32 sbceq1a 
 |-  ( x = w -> ( [. ( f ` w ) / y ]. ph <-> [. w / x ]. [. ( f ` w ) / y ]. ph ) )
33 31 32 bitrd 
 |-  ( x = w -> ( [. ( f ` x ) / y ]. ph <-> [. w / x ]. [. ( f ` w ) / y ]. ph ) )
34 28 29 33 cbvralw 
 |-  ( A. x e. A [. ( f ` x ) / y ]. ph <-> A. w e. A [. w / x ]. [. ( f ` w ) / y ]. ph )
35 27 34 sylib 
 |-  ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) -> A. w e. A [. w / x ]. [. ( f ` w ) / y ]. ph )
36 35 r19.21bi 
 |-  ( ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) /\ w e. A ) -> [. w / x ]. [. ( f ` w ) / y ]. ph )
37 rspesbca 
 |-  ( ( w e. A /\ [. w / x ]. [. ( f ` w ) / y ]. ph ) -> E. x e. A [. ( f ` w ) / y ]. ph )
38 26 36 37 syl2anc 
 |-  ( ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) /\ w e. A ) -> E. x e. A [. ( f ` w ) / y ]. ph )
39 38 ralrimiva 
 |-  ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) -> A. w e. A E. x e. A [. ( f ` w ) / y ]. ph )
40 dfsbcq 
 |-  ( z = ( f ` w ) -> ( [. z / y ]. ph <-> [. ( f ` w ) / y ]. ph ) )
41 40 rexbidv 
 |-  ( z = ( f ` w ) -> ( E. x e. A [. z / y ]. ph <-> E. x e. A [. ( f ` w ) / y ]. ph ) )
42 41 ralrn 
 |-  ( f Fn A -> ( A. z e. ran f E. x e. A [. z / y ]. ph <-> A. w e. A E. x e. A [. ( f ` w ) / y ]. ph ) )
43 11 42 syl 
 |-  ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) -> ( A. z e. ran f E. x e. A [. z / y ]. ph <-> A. w e. A E. x e. A [. ( f ` w ) / y ]. ph ) )
44 39 43 mpbird 
 |-  ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) -> A. z e. ran f E. x e. A [. z / y ]. ph )
45 nfv 
 |-  F/ z E. x e. A ph
46 nfcv 
 |-  F/_ y A
47 46 2 nfrexw 
 |-  F/ y E. x e. A [. z / y ]. ph
48 3 rexbidv 
 |-  ( y = z -> ( E. x e. A ph <-> E. x e. A [. z / y ]. ph ) )
49 45 47 48 cbvralw 
 |-  ( A. y e. ran f E. x e. A ph <-> A. z e. ran f E. x e. A [. z / y ]. ph )
50 44 49 sylibr 
 |-  ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) -> A. y e. ran f E. x e. A ph )
51 sseq1 
 |-  ( c = ran f -> ( c C_ B <-> ran f C_ B ) )
52 rexeq 
 |-  ( c = ran f -> ( E. y e. c ph <-> E. y e. ran f ph ) )
53 52 ralbidv 
 |-  ( c = ran f -> ( A. x e. A E. y e. c ph <-> A. x e. A E. y e. ran f ph ) )
54 raleq 
 |-  ( c = ran f -> ( A. y e. c E. x e. A ph <-> A. y e. ran f E. x e. A ph ) )
55 51 53 54 3anbi123d 
 |-  ( c = ran f -> ( ( c C_ B /\ A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) <-> ( ran f C_ B /\ A. x e. A E. y e. ran f ph /\ A. y e. ran f E. x e. A ph ) ) )
56 55 rspcev 
 |-  ( ( ran f e. Fin /\ ( ran f C_ B /\ A. x e. A E. y e. ran f ph /\ A. y e. ran f E. x e. A ph ) ) -> E. c e. Fin ( c C_ B /\ A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) )
57 15 17 25 50 56 syl13anc 
 |-  ( ( ( A e. Fin /\ A. x e. A E. y e. B ph ) /\ ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) ) -> E. c e. Fin ( c C_ B /\ A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) )
58 8 57 exlimddv 
 |-  ( ( A e. Fin /\ A. x e. A E. y e. B ph ) -> E. c e. Fin ( c C_ B /\ A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) )
59 58 3adant2 
 |-  ( ( A e. Fin /\ B e. M /\ A. x e. A E. y e. B ph ) -> E. c e. Fin ( c C_ B /\ A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) )