Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Alternative definitions of function values (2)
dfatco
Next ⟩
afv2co2
Metamath Proof Explorer
Ascii
Unicode
Theorem
dfatco
Description:
The predicate "defined at" for a function composition.
(Contributed by
AV
, 8-Sep-2022)
Ref
Expression
Assertion
dfatco
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
F
∘
G
defAt
X
Proof
Step
Hyp
Ref
Expression
1
dfatcolem
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
∃!
y
X
F
∘
G
y
2
euex
⊢
∃!
y
X
F
∘
G
y
→
∃
y
X
F
∘
G
y
3
1
2
syl
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
∃
y
X
F
∘
G
y
4
df-dm
⊢
dom
⁡
F
∘
G
=
x
|
∃
y
x
F
∘
G
y
5
4
eleq2i
⊢
X
∈
dom
⁡
F
∘
G
↔
X
∈
x
|
∃
y
x
F
∘
G
y
6
df-dfat
⊢
G
defAt
X
↔
X
∈
dom
⁡
G
∧
Fun
⁡
G
↾
X
7
6
simplbi
⊢
G
defAt
X
→
X
∈
dom
⁡
G
8
7
adantr
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
X
∈
dom
⁡
G
9
breq1
⊢
x
=
X
→
x
F
∘
G
y
↔
X
F
∘
G
y
10
9
exbidv
⊢
x
=
X
→
∃
y
x
F
∘
G
y
↔
∃
y
X
F
∘
G
y
11
10
elabg
⊢
X
∈
dom
⁡
G
→
X
∈
x
|
∃
y
x
F
∘
G
y
↔
∃
y
X
F
∘
G
y
12
8
11
syl
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
X
∈
x
|
∃
y
x
F
∘
G
y
↔
∃
y
X
F
∘
G
y
13
5
12
syl5bb
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
X
∈
dom
⁡
F
∘
G
↔
∃
y
X
F
∘
G
y
14
3
13
mpbird
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
X
∈
dom
⁡
F
∘
G
15
dfdfat2
⊢
F
∘
G
defAt
X
↔
X
∈
dom
⁡
F
∘
G
∧
∃!
y
X
F
∘
G
y
16
14
1
15
sylanbrc
⊢
G
defAt
X
∧
F
defAt
G
''''
X
→
F
∘
G
defAt
X