This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ 𝑧 𝜑
2 nfsbc1v ⊢ Ⅎ 𝑦 [ 𝑧 / 𝑦 ] 𝜑
3 sbceq1a ⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜑 ) )
4 1 2 3 cbvrexw ⊢ ( ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑧 ∈ 𝐵 [ 𝑧 / 𝑦 ] 𝜑 )
5 4 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 [ 𝑧 / 𝑦 ] 𝜑 )
6 dfsbcq ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑥 ) → ( [ 𝑧 / 𝑦 ] 𝜑 ↔ [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
7 6 ac6sfi ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 [ 𝑧 / 𝑦 ] 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
8 5 7 sylan2b ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) )
9 simpll ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) → 𝐴 ∈ Fin )
10 ffn ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝑓 Fn 𝐴 )
11 10 ad2antrl ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) → 𝑓 Fn 𝐴 )
12 dffn4 ⊢ ( 𝑓 Fn 𝐴 ↔ 𝑓 : 𝐴 –onto→ ran 𝑓 )
13 11 12 sylib ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) → 𝑓 : 𝐴 –onto→ ran 𝑓 )
14 fofi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑓 : 𝐴 –onto→ ran 𝑓 ) → ran 𝑓 ∈ Fin )
15 9 13 14 syl2anc ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) → ran 𝑓 ∈ Fin )
16 frn ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → ran 𝑓 ⊆ 𝐵 )
17 16 ad2antrl ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) → ran 𝑓 ⊆ 𝐵 )
18 fnfvelrn ⊢ ( ( 𝑓 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 )
19 10 18 sylan ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 )
20 rspesbca ⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 ∧ [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ∃ 𝑦 ∈ ran 𝑓 𝜑 )
21 20 ex ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 → ( [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 → ∃ 𝑦 ∈ ran 𝑓 𝜑 ) )
22 19 21 syl ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 → ∃ 𝑦 ∈ ran 𝑓 𝜑 ) )
23 22 ralimdva ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ran 𝑓 𝜑 ) )
24 23 imp ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ran 𝑓 𝜑 )
25 24 adantl ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ran 𝑓 𝜑 )
26 simpr ⊢ ( ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ 𝐴 )
27 simprr ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) → ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 )
28 nfv ⊢ Ⅎ 𝑤 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑
29 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝑤 / 𝑥 ] [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑
30 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑤 ) )
31 30 sbceq1d ⊢ ( 𝑥 = 𝑤 → ( [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ↔ [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑 ) )
32 sbceq1a ⊢ ( 𝑥 = 𝑤 → ( [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑 ↔ [ 𝑤 / 𝑥 ] [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑 ) )
33 31 32 bitrd ⊢ ( 𝑥 = 𝑤 → ( [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ↔ [ 𝑤 / 𝑥 ] [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑 ) )
34 28 29 33 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ↔ ∀ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑 )
35 27 34 sylib ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) → ∀ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑 )
36 35 r19.21bi ⊢ ( ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) ∧ 𝑤 ∈ 𝐴 ) → [ 𝑤 / 𝑥 ] [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑 )
37 rspesbca ⊢ ( ( 𝑤 ∈ 𝐴 ∧ [ 𝑤 / 𝑥 ] [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑 ) → ∃ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑 )
38 26 36 37 syl2anc ⊢ ( ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) ∧ 𝑤 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑 )
39 38 ralrimiva ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) → ∀ 𝑤 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑 )
40 dfsbcq ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑤 ) → ( [ 𝑧 / 𝑦 ] 𝜑 ↔ [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑 ) )
41 40 rexbidv ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑤 ) → ( ∃ 𝑥 ∈ 𝐴 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑 ) )
42 41 ralrn ⊢ ( 𝑓 Fn 𝐴 → ( ∀ 𝑧 ∈ ran 𝑓 ∃ 𝑥 ∈ 𝐴 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑤 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑 ) )
43 11 42 syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) → ( ∀ 𝑧 ∈ ran 𝑓 ∃ 𝑥 ∈ 𝐴 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑤 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑤 ) / 𝑦 ] 𝜑 ) )
44 39 43 mpbird ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) → ∀ 𝑧 ∈ ran 𝑓 ∃ 𝑥 ∈ 𝐴 [ 𝑧 / 𝑦 ] 𝜑 )
45 nfv ⊢ Ⅎ 𝑧 ∃ 𝑥 ∈ 𝐴 𝜑
46 nfcv ⊢ Ⅎ 𝑦 𝐴
47 46 2 nfrexw ⊢ Ⅎ 𝑦 ∃ 𝑥 ∈ 𝐴 [ 𝑧 / 𝑦 ] 𝜑
48 3 rexbidv ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 [ 𝑧 / 𝑦 ] 𝜑 ) )
49 45 47 48 cbvralw ⊢ ( ∀ 𝑦 ∈ ran 𝑓 ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑧 ∈ ran 𝑓 ∃ 𝑥 ∈ 𝐴 [ 𝑧 / 𝑦 ] 𝜑 )
50 44 49 sylibr ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) → ∀ 𝑦 ∈ ran 𝑓 ∃ 𝑥 ∈ 𝐴 𝜑 )
51 sseq1 ⊢ ( 𝑐 = ran 𝑓 → ( 𝑐 ⊆ 𝐵 ↔ ran 𝑓 ⊆ 𝐵 ) )
52 rexeq ⊢ ( 𝑐 = ran 𝑓 → ( ∃ 𝑦 ∈ 𝑐 𝜑 ↔ ∃ 𝑦 ∈ ran 𝑓 𝜑 ) )
53 52 ralbidv ⊢ ( 𝑐 = ran 𝑓 → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ran 𝑓 𝜑 ) )
54 raleq ⊢ ( 𝑐 = ran 𝑓 → ( ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ ran 𝑓 ∃ 𝑥 ∈ 𝐴 𝜑 ) )
55 51 53 54 3anbi123d ⊢ ( 𝑐 = ran 𝑓 → ( ( 𝑐 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ran 𝑓 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ran 𝑓 𝜑 ∧ ∀ 𝑦 ∈ ran 𝑓 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
56 55 rspcev ⊢ ( ( ran 𝑓 ∈ Fin ∧ ( ran 𝑓 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ran 𝑓 𝜑 ∧ ∀ 𝑦 ∈ ran 𝑓 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) → ∃ 𝑐 ∈ Fin ( 𝑐 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) )
57 15 17 25 50 56 syl13anc ⊢ ( ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 [ ( 𝑓 ‘ 𝑥 ) / 𝑦 ] 𝜑 ) ) → ∃ 𝑐 ∈ Fin ( 𝑐 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) )
58 8 57 exlimddv ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑐 ∈ Fin ( 𝑐 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) )
59 58 3adant2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑀 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑐 ∈ Fin ( 𝑐 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) )