Theorem afv2co2

Description: Value of a function composition, analogous to fvco2 . (Contributed by AV, 8-Sep-2022)

	Ref	Expression
Assertion	afv2co2	⊢ ( ( 𝐺 defAt 𝑋 ∧ 𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ( ( 𝐹 ∘ 𝐺 ) '''' 𝑋 ) = ( 𝐹 '''' ( 𝐺 '''' 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		imaco	⊢ ( ( 𝐹 ∘ 𝐺 ) “ { 𝑋 } ) = ( 𝐹 “ ( 𝐺 “ { 𝑋 } ) )
2		dfatsnafv2	⊢ ( 𝐺 defAt 𝑋 → { ( 𝐺 '''' 𝑋 ) } = ( 𝐺 “ { 𝑋 } ) )
3	2	adantr	⊢ ( ( 𝐺 defAt 𝑋 ∧ 𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → { ( 𝐺 '''' 𝑋 ) } = ( 𝐺 “ { 𝑋 } ) )
4	3	imaeq2d	⊢ ( ( 𝐺 defAt 𝑋 ∧ 𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ( 𝐹 “ { ( 𝐺 '''' 𝑋 ) } ) = ( 𝐹 “ ( 𝐺 “ { 𝑋 } ) ) )
5	1 4	eqtr4id	⊢ ( ( 𝐺 defAt 𝑋 ∧ 𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ( ( 𝐹 ∘ 𝐺 ) “ { 𝑋 } ) = ( 𝐹 “ { ( 𝐺 '''' 𝑋 ) } ) )
6	5	eleq2d	⊢ ( ( 𝐺 defAt 𝑋 ∧ 𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ( 𝑥 ∈ ( ( 𝐹 ∘ 𝐺 ) “ { 𝑋 } ) ↔ 𝑥 ∈ ( 𝐹 “ { ( 𝐺 '''' 𝑋 ) } ) ) )
7	6	iotabidv	⊢ ( ( 𝐺 defAt 𝑋 ∧ 𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ( ℩ 𝑥 𝑥 ∈ ( ( 𝐹 ∘ 𝐺 ) “ { 𝑋 } ) ) = ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { ( 𝐺 '''' 𝑋 ) } ) ) )
8		dfatco	⊢ ( ( 𝐺 defAt 𝑋 ∧ 𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ( 𝐹 ∘ 𝐺 ) defAt 𝑋 )
9		dfafv23	⊢ ( ( 𝐹 ∘ 𝐺 ) defAt 𝑋 → ( ( 𝐹 ∘ 𝐺 ) '''' 𝑋 ) = ( ℩ 𝑥 𝑥 ∈ ( ( 𝐹 ∘ 𝐺 ) “ { 𝑋 } ) ) )
10	8 9	syl	⊢ ( ( 𝐺 defAt 𝑋 ∧ 𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ( ( 𝐹 ∘ 𝐺 ) '''' 𝑋 ) = ( ℩ 𝑥 𝑥 ∈ ( ( 𝐹 ∘ 𝐺 ) “ { 𝑋 } ) ) )
11		dfafv23	⊢ ( 𝐹 defAt ( 𝐺 '''' 𝑋 ) → ( 𝐹 '''' ( 𝐺 '''' 𝑋 ) ) = ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { ( 𝐺 '''' 𝑋 ) } ) ) )
12	11	adantl	⊢ ( ( 𝐺 defAt 𝑋 ∧ 𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ( 𝐹 '''' ( 𝐺 '''' 𝑋 ) ) = ( ℩ 𝑥 𝑥 ∈ ( 𝐹 “ { ( 𝐺 '''' 𝑋 ) } ) ) )
13	7 10 12	3eqtr4d	⊢ ( ( 𝐺 defAt 𝑋 ∧ 𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ( ( 𝐹 ∘ 𝐺 ) '''' 𝑋 ) = ( 𝐹 '''' ( 𝐺 '''' 𝑋 ) ) )