Theorem mapprop

Description: An unordered pair containing two ordered pairs as an element of the mapping operation. (Contributed by AV, 16-Apr-2019) (Proof shortened by AV, 2-Jun-2024)

	Ref	Expression
Hypothesis	mapprop.f	|- F = { <. X , A >. , <. Y , B >. }
Assertion	mapprop	|- ( ( ( X e. V /\ A e. R ) /\ ( Y e. V /\ B e. R ) /\ ( X =/= Y /\ R e. W ) ) -> F e. ( R ^m { X , Y } ) )

Proof

Step	Hyp	Ref	Expression
1		mapprop.f	|- F = { <. X , A >. , <. Y , B >. }
2		simp3r	|- ( ( ( X e. V /\ A e. R ) /\ ( Y e. V /\ B e. R ) /\ ( X =/= Y /\ R e. W ) ) -> R e. W )
3		simpl	|- ( ( X e. V /\ A e. R ) -> X e. V )
4		simpl	|- ( ( Y e. V /\ B e. R ) -> Y e. V )
5		simpl	|- ( ( X =/= Y /\ R e. W ) -> X =/= Y )
6	3 4 5	3anim123i	|- ( ( ( X e. V /\ A e. R ) /\ ( Y e. V /\ B e. R ) /\ ( X =/= Y /\ R e. W ) ) -> ( X e. V /\ Y e. V /\ X =/= Y ) )
7		simpr	|- ( ( X e. V /\ A e. R ) -> A e. R )
8		simpr	|- ( ( Y e. V /\ B e. R ) -> B e. R )
9	7 8	anim12i	|- ( ( ( X e. V /\ A e. R ) /\ ( Y e. V /\ B e. R ) ) -> ( A e. R /\ B e. R ) )
10	9	3adant3	|- ( ( ( X e. V /\ A e. R ) /\ ( Y e. V /\ B e. R ) /\ ( X =/= Y /\ R e. W ) ) -> ( A e. R /\ B e. R ) )
11		fprmappr	|- ( ( R e. W /\ ( X e. V /\ Y e. V /\ X =/= Y ) /\ ( A e. R /\ B e. R ) ) -> { <. X , A >. , <. Y , B >. } e. ( R ^m { X , Y } ) )
12	2 6 10 11	syl3anc	|- ( ( ( X e. V /\ A e. R ) /\ ( Y e. V /\ B e. R ) /\ ( X =/= Y /\ R e. W ) ) -> { <. X , A >. , <. Y , B >. } e. ( R ^m { X , Y } ) )
13	1 12	eqeltrid	|- ( ( ( X e. V /\ A e. R ) /\ ( Y e. V /\ B e. R ) /\ ( X =/= Y /\ R e. W ) ) -> F e. ( R ^m { X , Y } ) )