Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Functions
fnco
Next ⟩
fnresdm
Metamath Proof Explorer
Ascii
Unicode
Theorem
fnco
Description:
Composition of two functions.
(Contributed by
NM
, 22-May-2006)
Ref
Expression
Assertion
fnco
⊢
F
Fn
A
∧
G
Fn
B
∧
ran
⁡
G
⊆
A
→
F
∘
G
Fn
B
Proof
Step
Hyp
Ref
Expression
1
fnfun
⊢
F
Fn
A
→
Fun
⁡
F
2
fnfun
⊢
G
Fn
B
→
Fun
⁡
G
3
funco
⊢
Fun
⁡
F
∧
Fun
⁡
G
→
Fun
⁡
F
∘
G
4
1
2
3
syl2an
⊢
F
Fn
A
∧
G
Fn
B
→
Fun
⁡
F
∘
G
5
4
3adant3
⊢
F
Fn
A
∧
G
Fn
B
∧
ran
⁡
G
⊆
A
→
Fun
⁡
F
∘
G
6
fndm
⊢
F
Fn
A
→
dom
⁡
F
=
A
7
6
sseq2d
⊢
F
Fn
A
→
ran
⁡
G
⊆
dom
⁡
F
↔
ran
⁡
G
⊆
A
8
7
biimpar
⊢
F
Fn
A
∧
ran
⁡
G
⊆
A
→
ran
⁡
G
⊆
dom
⁡
F
9
dmcosseq
⊢
ran
⁡
G
⊆
dom
⁡
F
→
dom
⁡
F
∘
G
=
dom
⁡
G
10
8
9
syl
⊢
F
Fn
A
∧
ran
⁡
G
⊆
A
→
dom
⁡
F
∘
G
=
dom
⁡
G
11
10
3adant2
⊢
F
Fn
A
∧
G
Fn
B
∧
ran
⁡
G
⊆
A
→
dom
⁡
F
∘
G
=
dom
⁡
G
12
fndm
⊢
G
Fn
B
→
dom
⁡
G
=
B
13
12
3ad2ant2
⊢
F
Fn
A
∧
G
Fn
B
∧
ran
⁡
G
⊆
A
→
dom
⁡
G
=
B
14
11
13
eqtrd
⊢
F
Fn
A
∧
G
Fn
B
∧
ran
⁡
G
⊆
A
→
dom
⁡
F
∘
G
=
B
15
df-fn
⊢
F
∘
G
Fn
B
↔
Fun
⁡
F
∘
G
∧
dom
⁡
F
∘
G
=
B
16
5
14
15
sylanbrc
⊢
F
Fn
A
∧
G
Fn
B
∧
ran
⁡
G
⊆
A
→
F
∘
G
Fn
B