Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Functions
foco
Next ⟩
foconst
Metamath Proof Explorer
Ascii
Unicode
Theorem
foco
Description:
Composition of onto functions.
(Contributed by
NM
, 22-Mar-2006)
Ref
Expression
Assertion
foco
⊢
F
:
B
⟶
onto
C
∧
G
:
A
⟶
onto
B
→
F
∘
G
:
A
⟶
onto
C
Proof
Step
Hyp
Ref
Expression
1
dffo2
⊢
F
:
B
⟶
onto
C
↔
F
:
B
⟶
C
∧
ran
⁡
F
=
C
2
dffo2
⊢
G
:
A
⟶
onto
B
↔
G
:
A
⟶
B
∧
ran
⁡
G
=
B
3
fco
⊢
F
:
B
⟶
C
∧
G
:
A
⟶
B
→
F
∘
G
:
A
⟶
C
4
3
ad2ant2r
⊢
F
:
B
⟶
C
∧
ran
⁡
F
=
C
∧
G
:
A
⟶
B
∧
ran
⁡
G
=
B
→
F
∘
G
:
A
⟶
C
5
fdm
⊢
F
:
B
⟶
C
→
dom
⁡
F
=
B
6
eqtr3
⊢
dom
⁡
F
=
B
∧
ran
⁡
G
=
B
→
dom
⁡
F
=
ran
⁡
G
7
5
6
sylan
⊢
F
:
B
⟶
C
∧
ran
⁡
G
=
B
→
dom
⁡
F
=
ran
⁡
G
8
rncoeq
⊢
dom
⁡
F
=
ran
⁡
G
→
ran
⁡
F
∘
G
=
ran
⁡
F
9
8
eqeq1d
⊢
dom
⁡
F
=
ran
⁡
G
→
ran
⁡
F
∘
G
=
C
↔
ran
⁡
F
=
C
10
9
biimpar
⊢
dom
⁡
F
=
ran
⁡
G
∧
ran
⁡
F
=
C
→
ran
⁡
F
∘
G
=
C
11
7
10
sylan
⊢
F
:
B
⟶
C
∧
ran
⁡
G
=
B
∧
ran
⁡
F
=
C
→
ran
⁡
F
∘
G
=
C
12
11
an32s
⊢
F
:
B
⟶
C
∧
ran
⁡
F
=
C
∧
ran
⁡
G
=
B
→
ran
⁡
F
∘
G
=
C
13
12
adantrl
⊢
F
:
B
⟶
C
∧
ran
⁡
F
=
C
∧
G
:
A
⟶
B
∧
ran
⁡
G
=
B
→
ran
⁡
F
∘
G
=
C
14
4
13
jca
⊢
F
:
B
⟶
C
∧
ran
⁡
F
=
C
∧
G
:
A
⟶
B
∧
ran
⁡
G
=
B
→
F
∘
G
:
A
⟶
C
∧
ran
⁡
F
∘
G
=
C
15
1
2
14
syl2anb
⊢
F
:
B
⟶
onto
C
∧
G
:
A
⟶
onto
B
→
F
∘
G
:
A
⟶
C
∧
ran
⁡
F
∘
G
=
C
16
dffo2
⊢
F
∘
G
:
A
⟶
onto
C
↔
F
∘
G
:
A
⟶
C
∧
ran
⁡
F
∘
G
=
C
17
15
16
sylibr
⊢
F
:
B
⟶
onto
C
∧
G
:
A
⟶
onto
B
→
F
∘
G
:
A
⟶
onto
C