Metamath Proof Explorer

Theorem fipreima

Description: Given a finite subset A of the range of a function, there exists a finite subset of the domain whose image is A . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion fipreima ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) → ∃ 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝐹 “ 𝑐 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 simp3 ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) → 𝐴 ∈ Fin )
2 dfss3 ⊢ ( 𝐴 ⊆ ran 𝐹 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ran 𝐹 )
3 fvelrnb ⊢ ( 𝐹 Fn 𝐵 → ( 𝑥 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ) )
4 3 ralbidv ⊢ ( 𝐹 Fn 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ran 𝐹 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ) )
5 2 4 bitrid ⊢ ( 𝐹 Fn 𝐵 → ( 𝐴 ⊆ ran 𝐹 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ) )
6 5 biimpa ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 )
7 6 3adant3 ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 )
8 fveqeq2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑦 ) = 𝑥 ↔ ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) )
9 8 ac6sfi ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑦 ) = 𝑥 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) )
10 1 7 9 syl2anc ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) )
11 fimass ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → ( 𝑓 “ 𝐴 ) ⊆ 𝐵 )
12 vex ⊢ 𝑓 ∈ V
13 12 imaex ⊢ ( 𝑓 “ 𝐴 ) ∈ V
14 13 elpw ⊢ ( ( 𝑓 “ 𝐴 ) ∈ 𝒫 𝐵 ↔ ( 𝑓 “ 𝐴 ) ⊆ 𝐵 )
15 11 14 sylibr ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → ( 𝑓 “ 𝐴 ) ∈ 𝒫 𝐵 )
16 15 ad2antrl ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) → ( 𝑓 “ 𝐴 ) ∈ 𝒫 𝐵 )
17 ffun ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → Fun 𝑓 )
18 17 ad2antrl ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) → Fun 𝑓 )
19 simpl3 ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) → 𝐴 ∈ Fin )
20 imafi ⊢ ( ( Fun 𝑓 ∧ 𝐴 ∈ Fin ) → ( 𝑓 “ 𝐴 ) ∈ Fin )
21 18 19 20 syl2anc ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) → ( 𝑓 “ 𝐴 ) ∈ Fin )
22 16 21 elind ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) → ( 𝑓 “ 𝐴 ) ∈ ( 𝒫 𝐵 ∩ Fin ) )
23 fvco3 ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) )
24 fvresi ⊢ ( 𝑥 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝑥 ) = 𝑥 )
25 24 adantl ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( I ↾ 𝐴 ) ‘ 𝑥 ) = 𝑥 )
26 23 25 eqeq12d ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ↔ ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) )
27 26 ralbidva ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) )
28 27 biimprd ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 → ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ) )
29 28 adantl ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ 𝑓 : 𝐴 ⟶ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 → ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ) )
30 29 impr ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) )
31 simpl1 ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) → 𝐹 Fn 𝐵 )
32 ffn ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝑓 Fn 𝐴 )
33 32 ad2antrl ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) → 𝑓 Fn 𝐴 )
34 frn ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → ran 𝑓 ⊆ 𝐵 )
35 34 ad2antrl ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) → ran 𝑓 ⊆ 𝐵 )
36 fnco ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝑓 Fn 𝐴 ∧ ran 𝑓 ⊆ 𝐵 ) → ( 𝐹 ∘ 𝑓 ) Fn 𝐴 )
37 31 33 35 36 syl3anc ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) → ( 𝐹 ∘ 𝑓 ) Fn 𝐴 )
38 fnresi ⊢ ( I ↾ 𝐴 ) Fn 𝐴
39 eqfnfv ⊢ ( ( ( 𝐹 ∘ 𝑓 ) Fn 𝐴 ∧ ( I ↾ 𝐴 ) Fn 𝐴 ) → ( ( 𝐹 ∘ 𝑓 ) = ( I ↾ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ) )
40 37 38 39 sylancl ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) → ( ( 𝐹 ∘ 𝑓 ) = ( I ↾ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑥 ) = ( ( I ↾ 𝐴 ) ‘ 𝑥 ) ) )
41 30 40 mpbird ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) → ( 𝐹 ∘ 𝑓 ) = ( I ↾ 𝐴 ) )
42 41 imaeq1d ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) → ( ( 𝐹 ∘ 𝑓 ) “ 𝐴 ) = ( ( I ↾ 𝐴 ) “ 𝐴 ) )
43 imaco ⊢ ( ( 𝐹 ∘ 𝑓 ) “ 𝐴 ) = ( 𝐹 “ ( 𝑓 “ 𝐴 ) )
44 ssid ⊢ 𝐴 ⊆ 𝐴
45 resiima ⊢ ( 𝐴 ⊆ 𝐴 → ( ( I ↾ 𝐴 ) “ 𝐴 ) = 𝐴 )
46 44 45 ax-mp ⊢ ( ( I ↾ 𝐴 ) “ 𝐴 ) = 𝐴
47 42 43 46 3eqtr3g ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) → ( 𝐹 “ ( 𝑓 “ 𝐴 ) ) = 𝐴 )
48 imaeq2 ⊢ ( 𝑐 = ( 𝑓 “ 𝐴 ) → ( 𝐹 “ 𝑐 ) = ( 𝐹 “ ( 𝑓 “ 𝐴 ) ) )
49 48 eqeq1d ⊢ ( 𝑐 = ( 𝑓 “ 𝐴 ) → ( ( 𝐹 “ 𝑐 ) = 𝐴 ↔ ( 𝐹 “ ( 𝑓 “ 𝐴 ) ) = 𝐴 ) )
50 49 rspcev ⊢ ( ( ( 𝑓 “ 𝐴 ) ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ ( 𝐹 “ ( 𝑓 “ 𝐴 ) ) = 𝐴 ) → ∃ 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝐹 “ 𝑐 ) = 𝐴 )
51 22 47 50 syl2anc ⊢ ( ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) ∧ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) → ∃ 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝐹 “ 𝑐 ) = 𝐴 )
52 10 51 exlimddv ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ ran 𝐹 ∧ 𝐴 ∈ Fin ) → ∃ 𝑐 ∈ ( 𝒫 𝐵 ∩ Fin ) ( 𝐹 “ 𝑐 ) = 𝐴 )