Theorem fnxpdmdm

Description: The domain of the domain of a function over a Cartesian square. (Contributed by AV, 13-Jan-2020)

	Ref	Expression
Assertion	fnxpdmdm	⊢ ( 𝐹 Fn ( 𝐴 × 𝐴 ) → dom dom 𝐹 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fndm	⊢ ( 𝐹 Fn ( 𝐴 × 𝐴 ) → dom 𝐹 = ( 𝐴 × 𝐴 ) )
2		dmeq	⊢ ( dom 𝐹 = ( 𝐴 × 𝐴 ) → dom dom 𝐹 = dom ( 𝐴 × 𝐴 ) )
3		dmxpid	⊢ dom ( 𝐴 × 𝐴 ) = 𝐴
4	2 3	eqtrdi	⊢ ( dom 𝐹 = ( 𝐴 × 𝐴 ) → dom dom 𝐹 = 𝐴 )
5	1 4	syl	⊢ ( 𝐹 Fn ( 𝐴 × 𝐴 ) → dom dom 𝐹 = 𝐴 )