Metamath Proof Explorer


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