Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Alternative definitions of function values (2)
afv2co2
Next ⟩
rlimdmafv2
Metamath Proof Explorer
Ascii
Unicode
Theorem
afv2co2
Description:
Value of a function composition, analogous to
fvco2
.
(Contributed by
AV
, 8-Sep-2022)
Ref
Expression
Assertion
afv2co2
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
F
∘
G
''''
X
=
F
''''
G
''''
X
Proof
Step
Hyp
Ref
Expression
1
imaco
⊢
F
∘
G
X
=
F
G
X
2
dfatsnafv2
⊢
G
defAt
X
→
G
''''
X
=
G
X
3
2
adantr
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
G
''''
X
=
G
X
4
3
imaeq2d
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
F
G
''''
X
=
F
G
X
5
1
4
eqtr4id
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
F
∘
G
X
=
F
G
''''
X
6
5
eleq2d
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
x
∈
F
∘
G
X
↔
x
∈
F
G
''''
X
7
6
iotabidv
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
ι
x
|
x
∈
F
∘
G
X
=
ι
x
|
x
∈
F
G
''''
X
8
dfatco
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
F
∘
G
defAt
X
9
dfafv23
⊢
F
∘
G
defAt
X
→
F
∘
G
''''
X
=
ι
x
|
x
∈
F
∘
G
X
10
8
9
syl
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
F
∘
G
''''
X
=
ι
x
|
x
∈
F
∘
G
X
11
dfafv23
⊢
F
defAt
G
''''
X
→
F
''''
G
''''
X
=
ι
x
|
x
∈
F
G
''''
X
12
11
adantl
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
F
''''
G
''''
X
=
ι
x
|
x
∈
F
G
''''
X
13
7
10
12
3eqtr4d
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
F
∘
G
''''
X
=
F
''''
G
''''
X