Metamath Proof Explorer


Theorem dfatco

Description: The predicate "defined at" for a function composition. (Contributed by AV, 8-Sep-2022)

Ref Expression
Assertion dfatco ( ( 𝐺 defAt 𝑋𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ( 𝐹𝐺 ) defAt 𝑋 )

Proof

Step Hyp Ref Expression
1 dfatcolem ( ( 𝐺 defAt 𝑋𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ∃! 𝑦 𝑋 ( 𝐹𝐺 ) 𝑦 )
2 euex ( ∃! 𝑦 𝑋 ( 𝐹𝐺 ) 𝑦 → ∃ 𝑦 𝑋 ( 𝐹𝐺 ) 𝑦 )
3 1 2 syl ( ( 𝐺 defAt 𝑋𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ∃ 𝑦 𝑋 ( 𝐹𝐺 ) 𝑦 )
4 df-dm dom ( 𝐹𝐺 ) = { 𝑥 ∣ ∃ 𝑦 𝑥 ( 𝐹𝐺 ) 𝑦 }
5 4 eleq2i ( 𝑋 ∈ dom ( 𝐹𝐺 ) ↔ 𝑋 ∈ { 𝑥 ∣ ∃ 𝑦 𝑥 ( 𝐹𝐺 ) 𝑦 } )
6 df-dfat ( 𝐺 defAt 𝑋 ↔ ( 𝑋 ∈ dom 𝐺 ∧ Fun ( 𝐺 ↾ { 𝑋 } ) ) )
7 6 simplbi ( 𝐺 defAt 𝑋𝑋 ∈ dom 𝐺 )
8 7 adantr ( ( 𝐺 defAt 𝑋𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → 𝑋 ∈ dom 𝐺 )
9 breq1 ( 𝑥 = 𝑋 → ( 𝑥 ( 𝐹𝐺 ) 𝑦𝑋 ( 𝐹𝐺 ) 𝑦 ) )
10 9 exbidv ( 𝑥 = 𝑋 → ( ∃ 𝑦 𝑥 ( 𝐹𝐺 ) 𝑦 ↔ ∃ 𝑦 𝑋 ( 𝐹𝐺 ) 𝑦 ) )
11 10 elabg ( 𝑋 ∈ dom 𝐺 → ( 𝑋 ∈ { 𝑥 ∣ ∃ 𝑦 𝑥 ( 𝐹𝐺 ) 𝑦 } ↔ ∃ 𝑦 𝑋 ( 𝐹𝐺 ) 𝑦 ) )
12 8 11 syl ( ( 𝐺 defAt 𝑋𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ( 𝑋 ∈ { 𝑥 ∣ ∃ 𝑦 𝑥 ( 𝐹𝐺 ) 𝑦 } ↔ ∃ 𝑦 𝑋 ( 𝐹𝐺 ) 𝑦 ) )
13 5 12 syl5bb ( ( 𝐺 defAt 𝑋𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ( 𝑋 ∈ dom ( 𝐹𝐺 ) ↔ ∃ 𝑦 𝑋 ( 𝐹𝐺 ) 𝑦 ) )
14 3 13 mpbird ( ( 𝐺 defAt 𝑋𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → 𝑋 ∈ dom ( 𝐹𝐺 ) )
15 dfdfat2 ( ( 𝐹𝐺 ) defAt 𝑋 ↔ ( 𝑋 ∈ dom ( 𝐹𝐺 ) ∧ ∃! 𝑦 𝑋 ( 𝐹𝐺 ) 𝑦 ) )
16 14 1 15 sylanbrc ( ( 𝐺 defAt 𝑋𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ( 𝐹𝐺 ) defAt 𝑋 )