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 o. G ) defAt X )

Proof

Step Hyp Ref Expression
1 dfatcolem 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> E! y X ( F o. G ) y )
2 euex 
 |-  ( E! y X ( F o. G ) y -> E. y X ( F o. G ) y )
3 1 2 syl 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> E. y X ( F o. G ) y )
4 df-dm 
 |-  dom ( F o. G ) = { x | E. y x ( F o. G ) y }
5 4 eleq2i 
 |-  ( X e. dom ( F o. G ) <-> X e. { x | E. y x ( F o. G ) y } )
6 df-dfat 
 |-  ( G defAt X <-> ( X e. dom G /\ Fun ( G |` { X } ) ) )
7 6 simplbi 
 |-  ( G defAt X -> X e. dom G )
8 7 adantr 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> X e. dom G )
9 breq1 
 |-  ( x = X -> ( x ( F o. G ) y <-> X ( F o. G ) y ) )
10 9 exbidv 
 |-  ( x = X -> ( E. y x ( F o. G ) y <-> E. y X ( F o. G ) y ) )
11 10 elabg 
 |-  ( X e. dom G -> ( X e. { x | E. y x ( F o. G ) y } <-> E. y X ( F o. G ) y ) )
12 8 11 syl 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( X e. { x | E. y x ( F o. G ) y } <-> E. y X ( F o. G ) y ) )
13 5 12 bitrid 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( X e. dom ( F o. G ) <-> E. y X ( F o. G ) y ) )
14 3 13 mpbird 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> X e. dom ( F o. G ) )
15 dfdfat2 
 |-  ( ( F o. G ) defAt X <-> ( X e. dom ( F o. G ) /\ E! y X ( F o. G ) y ) )
16 14 1 15 sylanbrc 
 |-  ( ( G defAt X /\ F defAt ( G '''' X ) ) -> ( F o. G ) defAt X )