Metamath Proof Explorer


Theorem indexdom

Description: If for every element of an indexing set A there exists a corresponding element of another set B , then there exists a subset of B consisting only of those elements which are indexed by A , and which is dominated by the set A . (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion indexdom
|- ( ( A e. M /\ A. x e. A E. y e. B ph ) -> E. c ( ( c ~<_ A /\ 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 nfsbc1v
 |-  F/ y [. ( f ` x ) / y ]. ph
2 sbceq1a
 |-  ( y = ( f ` x ) -> ( ph <-> [. ( f ` x ) / y ]. ph ) )
3 1 2 ac6gf
 |-  ( ( A e. M /\ A. x e. A E. y e. B ph ) -> E. f ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) )
4 fdm
 |-  ( f : A --> B -> dom f = A )
5 vex
 |-  f e. _V
6 5 dmex
 |-  dom f e. _V
7 4 6 eqeltrrdi
 |-  ( f : A --> B -> A e. _V )
8 ffn
 |-  ( f : A --> B -> f Fn A )
9 fnrndomg
 |-  ( A e. _V -> ( f Fn A -> ran f ~<_ A ) )
10 7 8 9 sylc
 |-  ( f : A --> B -> ran f ~<_ A )
11 10 adantr
 |-  ( ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) -> ran f ~<_ A )
12 frn
 |-  ( f : A --> B -> ran f C_ B )
13 12 adantr
 |-  ( ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) -> ran f C_ B )
14 nfv
 |-  F/ x f : A --> B
15 nfra1
 |-  F/ x A. x e. A [. ( f ` x ) / y ]. ph
16 14 15 nfan
 |-  F/ x ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph )
17 ffun
 |-  ( f : A --> B -> Fun f )
18 17 adantr
 |-  ( ( f : A --> B /\ x e. A ) -> Fun f )
19 4 eleq2d
 |-  ( f : A --> B -> ( x e. dom f <-> x e. A ) )
20 19 biimpar
 |-  ( ( f : A --> B /\ x e. A ) -> x e. dom f )
21 fvelrn
 |-  ( ( Fun f /\ x e. dom f ) -> ( f ` x ) e. ran f )
22 18 20 21 syl2anc
 |-  ( ( f : A --> B /\ x e. A ) -> ( f ` x ) e. ran f )
23 22 adantlr
 |-  ( ( ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) /\ x e. A ) -> ( f ` x ) e. ran f )
24 rspa
 |-  ( ( A. x e. A [. ( f ` x ) / y ]. ph /\ x e. A ) -> [. ( f ` x ) / y ]. ph )
25 24 adantll
 |-  ( ( ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) /\ x e. A ) -> [. ( f ` x ) / y ]. ph )
26 rspesbca
 |-  ( ( ( f ` x ) e. ran f /\ [. ( f ` x ) / y ]. ph ) -> E. y e. ran f ph )
27 23 25 26 syl2anc
 |-  ( ( ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) /\ x e. A ) -> E. y e. ran f ph )
28 27 ex
 |-  ( ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) -> ( x e. A -> E. y e. ran f ph ) )
29 16 28 ralrimi
 |-  ( ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) -> A. x e. A E. y e. ran f ph )
30 nfv
 |-  F/ y f : A --> B
31 nfcv
 |-  F/_ y A
32 31 1 nfralw
 |-  F/ y A. x e. A [. ( f ` x ) / y ]. ph
33 30 32 nfan
 |-  F/ y ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph )
34 fvelrnb
 |-  ( f Fn A -> ( y e. ran f <-> E. x e. A ( f ` x ) = y ) )
35 8 34 syl
 |-  ( f : A --> B -> ( y e. ran f <-> E. x e. A ( f ` x ) = y ) )
36 35 adantr
 |-  ( ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) -> ( y e. ran f <-> E. x e. A ( f ` x ) = y ) )
37 rsp
 |-  ( A. x e. A [. ( f ` x ) / y ]. ph -> ( x e. A -> [. ( f ` x ) / y ]. ph ) )
38 37 adantl
 |-  ( ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) -> ( x e. A -> [. ( f ` x ) / y ]. ph ) )
39 2 eqcoms
 |-  ( ( f ` x ) = y -> ( ph <-> [. ( f ` x ) / y ]. ph ) )
40 39 biimprcd
 |-  ( [. ( f ` x ) / y ]. ph -> ( ( f ` x ) = y -> ph ) )
41 38 40 syl6
 |-  ( ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) -> ( x e. A -> ( ( f ` x ) = y -> ph ) ) )
42 16 41 reximdai
 |-  ( ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) -> ( E. x e. A ( f ` x ) = y -> E. x e. A ph ) )
43 36 42 sylbid
 |-  ( ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) -> ( y e. ran f -> E. x e. A ph ) )
44 33 43 ralrimi
 |-  ( ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) -> A. y e. ran f E. x e. A ph )
45 5 rnex
 |-  ran f e. _V
46 breq1
 |-  ( c = ran f -> ( c ~<_ A <-> ran f ~<_ A ) )
47 sseq1
 |-  ( c = ran f -> ( c C_ B <-> ran f C_ B ) )
48 46 47 anbi12d
 |-  ( c = ran f -> ( ( c ~<_ A /\ c C_ B ) <-> ( ran f ~<_ A /\ ran f C_ B ) ) )
49 rexeq
 |-  ( c = ran f -> ( E. y e. c ph <-> E. y e. ran f ph ) )
50 49 ralbidv
 |-  ( c = ran f -> ( A. x e. A E. y e. c ph <-> A. x e. A E. y e. ran f ph ) )
51 raleq
 |-  ( c = ran f -> ( A. y e. c E. x e. A ph <-> A. y e. ran f E. x e. A ph ) )
52 50 51 anbi12d
 |-  ( c = ran f -> ( ( A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) <-> ( A. x e. A E. y e. ran f ph /\ A. y e. ran f E. x e. A ph ) ) )
53 48 52 anbi12d
 |-  ( c = ran f -> ( ( ( c ~<_ A /\ c C_ B ) /\ ( A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) ) <-> ( ( ran f ~<_ A /\ ran f C_ B ) /\ ( A. x e. A E. y e. ran f ph /\ A. y e. ran f E. x e. A ph ) ) ) )
54 45 53 spcev
 |-  ( ( ( ran f ~<_ A /\ 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 ( ( c ~<_ A /\ c C_ B ) /\ ( A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) ) )
55 11 13 29 44 54 syl22anc
 |-  ( ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) -> E. c ( ( c ~<_ A /\ c C_ B ) /\ ( A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) ) )
56 55 exlimiv
 |-  ( E. f ( f : A --> B /\ A. x e. A [. ( f ` x ) / y ]. ph ) -> E. c ( ( c ~<_ A /\ c C_ B ) /\ ( A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) ) )
57 3 56 syl
 |-  ( ( A e. M /\ A. x e. A E. y e. B ph ) -> E. c ( ( c ~<_ A /\ c C_ B ) /\ ( A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) ) )