Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Finite sets
imafi
Next ⟩
pwfilem
Metamath Proof Explorer
Ascii
Unicode
Theorem
imafi
Description:
Images of finite sets are finite.
(Contributed by
Stefan O'Rear
, 22-Feb-2015)
Ref
Expression
Assertion
imafi
⊢
Fun
⁡
F
∧
X
∈
Fin
→
F
X
∈
Fin
Proof
Step
Hyp
Ref
Expression
1
imadmres
⊢
F
dom
⁡
F
↾
X
=
F
X
2
simpr
⊢
Fun
⁡
F
∧
X
∈
Fin
→
X
∈
Fin
3
dmres
⊢
dom
⁡
F
↾
X
=
X
∩
dom
⁡
F
4
inss1
⊢
X
∩
dom
⁡
F
⊆
X
5
3
4
eqsstri
⊢
dom
⁡
F
↾
X
⊆
X
6
ssfi
⊢
X
∈
Fin
∧
dom
⁡
F
↾
X
⊆
X
→
dom
⁡
F
↾
X
∈
Fin
7
2
5
6
sylancl
⊢
Fun
⁡
F
∧
X
∈
Fin
→
dom
⁡
F
↾
X
∈
Fin
8
resss
⊢
F
↾
X
⊆
F
9
dmss
⊢
F
↾
X
⊆
F
→
dom
⁡
F
↾
X
⊆
dom
⁡
F
10
8
9
mp1i
⊢
Fun
⁡
F
∧
X
∈
Fin
→
dom
⁡
F
↾
X
⊆
dom
⁡
F
11
fores
⊢
Fun
⁡
F
∧
dom
⁡
F
↾
X
⊆
dom
⁡
F
→
F
↾
dom
⁡
F
↾
X
:
dom
⁡
F
↾
X
⟶
onto
F
dom
⁡
F
↾
X
12
10
11
syldan
⊢
Fun
⁡
F
∧
X
∈
Fin
→
F
↾
dom
⁡
F
↾
X
:
dom
⁡
F
↾
X
⟶
onto
F
dom
⁡
F
↾
X
13
fofi
⊢
dom
⁡
F
↾
X
∈
Fin
∧
F
↾
dom
⁡
F
↾
X
:
dom
⁡
F
↾
X
⟶
onto
F
dom
⁡
F
↾
X
→
F
dom
⁡
F
↾
X
∈
Fin
14
7
12
13
syl2anc
⊢
Fun
⁡
F
∧
X
∈
Fin
→
F
dom
⁡
F
↾
X
∈
Fin
15
1
14
eqeltrrid
⊢
Fun
⁡
F
∧
X
∈
Fin
→
F
X
∈
Fin