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 ( ( 𝐴 ∈ 𝑀 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑐 ( ( 𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 nfsbc1v ⊢ Ⅎ 𝑦 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑
2 sbceq1a ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
3 1 2 ac6gf ⊢ ( ( 𝐴 ∈ 𝑀 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
4 fdm ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → dom 𝑓 = 𝐴 )
5 vex ⊢ 𝑓 ∈ V
6 5 dmex ⊢ dom 𝑓 ∈ V
7 4 6 eqeltrrdi ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝐴 ∈ V )
8 ffn ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝑓 Fn 𝐴 )
9 fnrndomg ⊢ ( 𝐴 ∈ V → ( 𝑓 Fn 𝐴 → ran 𝑓 ≼ 𝐴 ) )
10 7 8 9 sylc ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → ran 𝑓 ≼ 𝐴 )
11 10 adantr ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ran 𝑓 ≼ 𝐴 )
12 frn ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → ran 𝑓 ⊆ 𝐵 )
13 12 adantr ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ran 𝑓 ⊆ 𝐵 )
14 nfv ⊢ Ⅎ 𝑥 𝑓 : 𝐴 ⟶ 𝐵
15 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑
16 14 15 nfan ⊢ Ⅎ 𝑥 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 )
17 ffun ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → Fun 𝑓 )
18 17 adantr ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → Fun 𝑓 )
19 4 eleq2d ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → ( 𝑥 ∈ dom 𝑓 ↔ 𝑥 ∈ 𝐴 ) )
20 19 biimpar ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom 𝑓 )
21 fvelrn ⊢ ( ( Fun 𝑓 ∧ 𝑥 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 )
22 18 20 21 syl2anc ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 )
23 22 adantlr ⊢ ( ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 )
24 rspa ⊢ ( ( ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ∧ 𝑥 ∈ 𝐴 ) → [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 )
25 24 adantll ⊢ ( ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ∧ 𝑥 ∈ 𝐴 ) → [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 )
26 rspesbca ⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 ∧ [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ∃ 𝑦 ∈ ran 𝑓 𝜑 )
27 23 25 26 syl2anc ⊢ ( ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ran 𝑓 𝜑 )
28 27 ex ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ( 𝑥 ∈ 𝐴 → ∃ 𝑦 ∈ ran 𝑓 𝜑 ) )
29 16 28 ralrimi ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ran 𝑓 𝜑 )
30 nfv ⊢ Ⅎ 𝑦 𝑓 : 𝐴 ⟶ 𝐵
31 nfcv ⊢ Ⅎ 𝑦 𝐴
32 31 1 nfralw ⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑
33 30 32 nfan ⊢ Ⅎ 𝑦 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 )
34 fvelrnb ⊢ ( 𝑓 Fn 𝐴 → ( 𝑦 ∈ ran 𝑓 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) = 𝑦 ) )
35 8 34 syl ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → ( 𝑦 ∈ ran 𝑓 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) = 𝑦 ) )
36 35 adantr ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ( 𝑦 ∈ ran 𝑓 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) = 𝑦 ) )
37 rsp ⊢ ( ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 → ( 𝑥 ∈ 𝐴 → [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
38 37 adantl ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ( 𝑥 ∈ 𝐴 → [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
39 2 eqcoms ⊢ ( ( 𝑓 ‘ 𝑥 ) = 𝑦 → ( 𝜑 ↔ [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
40 39 biimprcd ⊢ ( [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 → ( ( 𝑓 ‘ 𝑥 ) = 𝑦 → 𝜑 ) )
41 38 40 syl6 ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ( 𝑥 ∈ 𝐴 → ( ( 𝑓 ‘ 𝑥 ) = 𝑦 → 𝜑 ) ) )
42 16 41 reximdai ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ( ∃ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) = 𝑦 → ∃ 𝑥 ∈ 𝐴 𝜑 ) )
43 36 42 sylbid ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ( 𝑦 ∈ ran 𝑓 → ∃ 𝑥 ∈ 𝐴 𝜑 ) )
44 33 43 ralrimi ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ∀ 𝑦 ∈ ran 𝑓 ∃ 𝑥 ∈ 𝐴 𝜑 )
45 5 rnex ⊢ ran 𝑓 ∈ V
46 breq1 ⊢ ( 𝑐 = ran 𝑓 → ( 𝑐 ≼ 𝐴 ↔ ran 𝑓 ≼ 𝐴 ) )
47 sseq1 ⊢ ( 𝑐 = ran 𝑓 → ( 𝑐 ⊆ 𝐵 ↔ ran 𝑓 ⊆ 𝐵 ) )
48 46 47 anbi12d ⊢ ( 𝑐 = ran 𝑓 → ( ( 𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵 ) ↔ ( ran 𝑓 ≼ 𝐴 ∧ ran 𝑓 ⊆ 𝐵 ) ) )
49 rexeq ⊢ ( 𝑐 = ran 𝑓 → ( ∃ 𝑦 ∈ 𝑐 𝜑 ↔ ∃ 𝑦 ∈ ran 𝑓 𝜑 ) )
50 49 ralbidv ⊢ ( 𝑐 = ran 𝑓 → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ran 𝑓 𝜑 ) )
51 raleq ⊢ ( 𝑐 = ran 𝑓 → ( ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ ran 𝑓 ∃ 𝑥 ∈ 𝐴 𝜑 ) )
52 50 51 anbi12d ⊢ ( 𝑐 = ran 𝑓 → ( ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ran 𝑓 𝜑 ∧ ∀ 𝑦 ∈ ran 𝑓 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
53 48 52 anbi12d ⊢ ( 𝑐 = ran 𝑓 → ( ( ( 𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) ↔ ( ( ran 𝑓 ≼ 𝐴 ∧ ran 𝑓 ⊆ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ran 𝑓 𝜑 ∧ ∀ 𝑦 ∈ ran 𝑓 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) ) )
54 45 53 spcev ⊢ ( ( ( ran 𝑓 ≼ 𝐴 ∧ ran 𝑓 ⊆ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ran 𝑓 𝜑 ∧ ∀ 𝑦 ∈ ran 𝑓 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) → ∃ 𝑐 ( ( 𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
55 11 13 29 44 54 syl22anc ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ∃ 𝑐 ( ( 𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
56 55 exlimiv ⊢ ( ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ∃ 𝑐 ( ( 𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
57 3 56 syl ⊢ ( ( 𝐴 ∈ 𝑀 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑐 ( ( 𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )