Theorem rnfdmpr

Description: The range of a one-to-one function F of an unordered pair into a set is the unordered pair of the function values. (Contributed by Alexander van der Vekens, 2-Feb-2018)

	Ref	Expression
Assertion	rnfdmpr	|- ( ( X e. V /\ Y e. W ) -> ( F Fn { X , Y } -> ran F = { ( F ` X ) , ( F ` Y ) } ) )

Proof

Step	Hyp	Ref	Expression
1		fnrnfv	|- ( F Fn { X , Y } -> ran F = { x | E. i e. { X , Y } x = ( F ` i ) } )
2	1	adantl	|- ( ( ( X e. V /\ Y e. W ) /\ F Fn { X , Y } ) -> ran F = { x | E. i e. { X , Y } x = ( F ` i ) } )
3		fveq2	|- ( i = X -> ( F ` i ) = ( F ` X ) )
4	3	eqeq2d	|- ( i = X -> ( x = ( F ` i ) <-> x = ( F ` X ) ) )
5	4	abbidv	|- ( i = X -> { x | x = ( F ` i ) } = { x | x = ( F ` X ) } )
6		fveq2	|- ( i = Y -> ( F ` i ) = ( F ` Y ) )
7	6	eqeq2d	|- ( i = Y -> ( x = ( F ` i ) <-> x = ( F ` Y ) ) )
8	7	abbidv	|- ( i = Y -> { x | x = ( F ` i ) } = { x | x = ( F ` Y ) } )
9	5 8	iunxprg	|- ( ( X e. V /\ Y e. W ) -> U_ i e. { X , Y } { x | x = ( F ` i ) } = ( { x | x = ( F ` X ) } u. { x | x = ( F ` Y ) } ) )
10	9	adantr	|- ( ( ( X e. V /\ Y e. W ) /\ F Fn { X , Y } ) -> U_ i e. { X , Y } { x | x = ( F ` i ) } = ( { x | x = ( F ` X ) } u. { x | x = ( F ` Y ) } ) )
11		iunab	|- U_ i e. { X , Y } { x | x = ( F ` i ) } = { x | E. i e. { X , Y } x = ( F ` i ) }
12		df-sn	|- { ( F ` X ) } = { x | x = ( F ` X ) }
13	12	eqcomi	|- { x | x = ( F ` X ) } = { ( F ` X ) }
14		df-sn	|- { ( F ` Y ) } = { x | x = ( F ` Y ) }
15	14	eqcomi	|- { x | x = ( F ` Y ) } = { ( F ` Y ) }
16	13 15	uneq12i	|- ( { x | x = ( F ` X ) } u. { x | x = ( F ` Y ) } ) = ( { ( F ` X ) } u. { ( F ` Y ) } )
17		df-pr	|- { ( F ` X ) , ( F ` Y ) } = ( { ( F ` X ) } u. { ( F ` Y ) } )
18	16 17	eqtr4i	|- ( { x | x = ( F ` X ) } u. { x | x = ( F ` Y ) } ) = { ( F ` X ) , ( F ` Y ) }
19	10 11 18	3eqtr3g	|- ( ( ( X e. V /\ Y e. W ) /\ F Fn { X , Y } ) -> { x | E. i e. { X , Y } x = ( F ` i ) } = { ( F ` X ) , ( F ` Y ) } )
20	2 19	eqtrd	|- ( ( ( X e. V /\ Y e. W ) /\ F Fn { X , Y } ) -> ran F = { ( F ` X ) , ( F ` Y ) } )
21	20	ex	|- ( ( X e. V /\ Y e. W ) -> ( F Fn { X , Y } -> ran F = { ( F ` X ) , ( F ` Y ) } ) )