Theorem mptssALT

Description: Deduce subset relation of mapping-to function graphs from a subset relation of domains. Alternative proof of mptss . (Contributed by Thierry Arnoux, 30-May-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	mptssALT	|- ( A C_ B -> ( x e. A |-> C ) C_ ( x e. B |-> C ) )

Proof

Step	Hyp	Ref	Expression
1		ssel	|- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d	|- ( A C_ B -> ( ( x e. A /\ y = C ) -> ( x e. B /\ y = C ) ) )
3	2	ssopab2dv	|- ( A C_ B -> { <. x , y >. | ( x e. A /\ y = C ) } C_ { <. x , y >. | ( x e. B /\ y = C ) } )
4		df-mpt	|- ( x e. A |-> C ) = { <. x , y >. | ( x e. A /\ y = C ) }
5		df-mpt	|- ( x e. B |-> C ) = { <. x , y >. | ( x e. B /\ y = C ) }
6	3 4 5	3sstr4g	|- ( A C_ B -> ( x e. A |-> C ) C_ ( x e. B |-> C ) )