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