Theorem fprmappr

Description: A function with a domain of two elements as element of the mapping operator applied to a pair. (Contributed by AV, 20-May-2024)

	Ref	Expression
Assertion	fprmappr	|- ( ( X e. V /\ ( A e. U /\ B e. W /\ A =/= B ) /\ ( C e. X /\ D e. X ) ) -> { <. A , C >. , <. B , D >. } e. ( X ^m { A , B } ) )

Proof

Step	Hyp	Ref	Expression
1		3simpa	|- ( ( A e. U /\ B e. W /\ A =/= B ) -> ( A e. U /\ B e. W ) )
2	1	adantr	|- ( ( ( A e. U /\ B e. W /\ A =/= B ) /\ ( C e. X /\ D e. X ) ) -> ( A e. U /\ B e. W ) )
3		simpr	|- ( ( ( A e. U /\ B e. W /\ A =/= B ) /\ ( C e. X /\ D e. X ) ) -> ( C e. X /\ D e. X ) )
4		simpl3	|- ( ( ( A e. U /\ B e. W /\ A =/= B ) /\ ( C e. X /\ D e. X ) ) -> A =/= B )
5		fprg	|- ( ( ( A e. U /\ B e. W ) /\ ( C e. X /\ D e. X ) /\ A =/= B ) -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } )
6	2 3 4 5	syl3anc	|- ( ( ( A e. U /\ B e. W /\ A =/= B ) /\ ( C e. X /\ D e. X ) ) -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } )
7		prssi	|- ( ( C e. X /\ D e. X ) -> { C , D } C_ X )
8	7	adantl	|- ( ( ( A e. U /\ B e. W /\ A =/= B ) /\ ( C e. X /\ D e. X ) ) -> { C , D } C_ X )
9	6 8	fssd	|- ( ( ( A e. U /\ B e. W /\ A =/= B ) /\ ( C e. X /\ D e. X ) ) -> { <. A , C >. , <. B , D >. } : { A , B } --> X )
10	9	3adant1	|- ( ( X e. V /\ ( A e. U /\ B e. W /\ A =/= B ) /\ ( C e. X /\ D e. X ) ) -> { <. A , C >. , <. B , D >. } : { A , B } --> X )
11		simp1	|- ( ( X e. V /\ ( A e. U /\ B e. W /\ A =/= B ) /\ ( C e. X /\ D e. X ) ) -> X e. V )
12		prex	|- { A , B } e. _V
13	12	a1i	|- ( ( X e. V /\ ( A e. U /\ B e. W /\ A =/= B ) /\ ( C e. X /\ D e. X ) ) -> { A , B } e. _V )
14	11 13	elmapd	|- ( ( X e. V /\ ( A e. U /\ B e. W /\ A =/= B ) /\ ( C e. X /\ D e. X ) ) -> ( { <. A , C >. , <. B , D >. } e. ( X ^m { A , B } ) <-> { <. A , C >. , <. B , D >. } : { A , B } --> X ) )
15	10 14	mpbird	|- ( ( X e. V /\ ( A e. U /\ B e. W /\ A =/= B ) /\ ( C e. X /\ D e. X ) ) -> { <. A , C >. , <. B , D >. } e. ( X ^m { A , B } ) )