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	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( 𝐹 Fn { 𝑋 , 𝑌 } → ran 𝐹 = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		fnrnfv	⊢ ( 𝐹 Fn { 𝑋 , 𝑌 } → ran 𝐹 = { 𝑥 ∣ ∃ 𝑖 ∈ { 𝑋 , 𝑌 } 𝑥 = ( 𝐹 ‘ 𝑖 ) } )
2	1	adantl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ 𝐹 Fn { 𝑋 , 𝑌 } ) → ran 𝐹 = { 𝑥 ∣ ∃ 𝑖 ∈ { 𝑋 , 𝑌 } 𝑥 = ( 𝐹 ‘ 𝑖 ) } )
3		fveq2	⊢ ( 𝑖 = 𝑋 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑋 ) )
4	3	eqeq2d	⊢ ( 𝑖 = 𝑋 → ( 𝑥 = ( 𝐹 ‘ 𝑖 ) ↔ 𝑥 = ( 𝐹 ‘ 𝑋 ) ) )
5	4	abbidv	⊢ ( 𝑖 = 𝑋 → { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑖 ) } = { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑋 ) } )
6		fveq2	⊢ ( 𝑖 = 𝑌 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑌 ) )
7	6	eqeq2d	⊢ ( 𝑖 = 𝑌 → ( 𝑥 = ( 𝐹 ‘ 𝑖 ) ↔ 𝑥 = ( 𝐹 ‘ 𝑌 ) ) )
8	7	abbidv	⊢ ( 𝑖 = 𝑌 → { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑖 ) } = { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑌 ) } )
9	5 8	iunxprg	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ∪ 𝑖 ∈ { 𝑋 , 𝑌 } { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑖 ) } = ( { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑋 ) } ∪ { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑌 ) } ) )
10	9	adantr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ 𝐹 Fn { 𝑋 , 𝑌 } ) → ∪ 𝑖 ∈ { 𝑋 , 𝑌 } { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑖 ) } = ( { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑋 ) } ∪ { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑌 ) } ) )
11		iunab	⊢ ∪ 𝑖 ∈ { 𝑋 , 𝑌 } { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑖 ) } = { 𝑥 ∣ ∃ 𝑖 ∈ { 𝑋 , 𝑌 } 𝑥 = ( 𝐹 ‘ 𝑖 ) }
12		df-sn	⊢ { ( 𝐹 ‘ 𝑋 ) } = { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑋 ) }
13	12	eqcomi	⊢ { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑋 ) } = { ( 𝐹 ‘ 𝑋 ) }
14		df-sn	⊢ { ( 𝐹 ‘ 𝑌 ) } = { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑌 ) }
15	14	eqcomi	⊢ { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑌 ) } = { ( 𝐹 ‘ 𝑌 ) }
16	13 15	uneq12i	⊢ ( { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑋 ) } ∪ { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑌 ) } ) = ( { ( 𝐹 ‘ 𝑋 ) } ∪ { ( 𝐹 ‘ 𝑌 ) } )
17		df-pr	⊢ { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } = ( { ( 𝐹 ‘ 𝑋 ) } ∪ { ( 𝐹 ‘ 𝑌 ) } )
18	16 17	eqtr4i	⊢ ( { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑋 ) } ∪ { 𝑥 ∣ 𝑥 = ( 𝐹 ‘ 𝑌 ) } ) = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) }
19	10 11 18	3eqtr3g	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ 𝐹 Fn { 𝑋 , 𝑌 } ) → { 𝑥 ∣ ∃ 𝑖 ∈ { 𝑋 , 𝑌 } 𝑥 = ( 𝐹 ‘ 𝑖 ) } = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } )
20	2 19	eqtrd	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ 𝐹 Fn { 𝑋 , 𝑌 } ) → ran 𝐹 = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } )
21	20	ex	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( 𝐹 Fn { 𝑋 , 𝑌 } → ran 𝐹 = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) } ) )