Theorem fmpodg

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Zhi Wang, 29-Sep-2025)

	Ref	Expression
Hypotheses	fmpodg.1	|- ( ph -> F = ( x e. A , y e. B |-> C ) )
	fmpodg.2	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C e. S )
	fmpodg.3	|- ( ph -> R = ( A X. B ) )
Assertion	fmpodg	|- ( ph -> F : R --> S )

Proof

Step	Hyp	Ref	Expression
1		fmpodg.1	|- ( ph -> F = ( x e. A , y e. B |-> C ) )
2		fmpodg.2	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C e. S )
3		fmpodg.3	|- ( ph -> R = ( A X. B ) )
4	2	ralrimivva	|- ( ph -> A. x e. A A. y e. B C e. S )
5		eqid	|- ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> C )
6	5	fmpo	|- ( A. x e. A A. y e. B C e. S <-> ( x e. A , y e. B |-> C ) : ( A X. B ) --> S )
7	4 6	sylib	|- ( ph -> ( x e. A , y e. B |-> C ) : ( A X. B ) --> S )
8	1 3	feq12d	|- ( ph -> ( F : R --> S <-> ( x e. A , y e. B |-> C ) : ( A X. B ) --> S ) )
9	7 8	mpbird	|- ( ph -> F : R --> S )