Theorem dmdm

Description: The double domain of a function on a Cartesian square. (Contributed by Zhi Wang, 1-Nov-2025)

	Ref	Expression
Assertion	dmdm	⊢ ( 𝐴 Fn ( 𝐵 × 𝐵 ) → 𝐵 = dom dom 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fndm	⊢ ( 𝐴 Fn ( 𝐵 × 𝐵 ) → dom 𝐴 = ( 𝐵 × 𝐵 ) )
2	1	dmeqd	⊢ ( 𝐴 Fn ( 𝐵 × 𝐵 ) → dom dom 𝐴 = dom ( 𝐵 × 𝐵 ) )
3		dmxpid	⊢ dom ( 𝐵 × 𝐵 ) = 𝐵
4	2 3	eqtr2di	⊢ ( 𝐴 Fn ( 𝐵 × 𝐵 ) → 𝐵 = dom dom 𝐴 )