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	bitrid	⊢ ( ( 𝐺 defAt 𝑋 ∧ 𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑦 𝑋 ( 𝐹 ∘ 𝐺 ) 𝑦 ) )
14	3 13	mpbird	⊢ ( ( 𝐺 defAt 𝑋 ∧ 𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) )
15		dfdfat2	⊢ ( ( 𝐹 ∘ 𝐺 ) defAt 𝑋 ↔ ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ ∃! 𝑦 𝑋 ( 𝐹 ∘ 𝐺 ) 𝑦 ) )
16	14 1 15	sylanbrc	⊢ ( ( 𝐺 defAt 𝑋 ∧ 𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ( 𝐹 ∘ 𝐺 ) defAt 𝑋 )