Theorem fpr

Description: A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Hypotheses	fpr.1	⊢ 𝐴 ∈ V
	fpr.2	⊢ 𝐵 ∈ V
	fpr.3	⊢ 𝐶 ∈ V
	fpr.4	⊢ 𝐷 ∈ V
Assertion	fpr	⊢ ( 𝐴 ≠ 𝐵 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } )

Proof

Step	Hyp	Ref	Expression
1		fpr.1	⊢ 𝐴 ∈ V
2		fpr.2	⊢ 𝐵 ∈ V
3		fpr.3	⊢ 𝐶 ∈ V
4		fpr.4	⊢ 𝐷 ∈ V
5	1 2 3 4	funpr	⊢ ( 𝐴 ≠ 𝐵 → Fun { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } )
6	3 4	dmprop	⊢ dom { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐴 , 𝐵 }
7		df-fn	⊢ ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } Fn { 𝐴 , 𝐵 } ↔ ( Fun { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ∧ dom { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐴 , 𝐵 } ) )
8	5 6 7	sylanblrc	⊢ ( 𝐴 ≠ 𝐵 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } Fn { 𝐴 , 𝐵 } )
9		df-pr	⊢ { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } )
10	9	rneqi	⊢ ran { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ran ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } )
11		rnun	⊢ ran ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( ran { ⟨ 𝐴 , 𝐶 ⟩ } ∪ ran { ⟨ 𝐵 , 𝐷 ⟩ } )
12	1	rnsnop	⊢ ran { ⟨ 𝐴 , 𝐶 ⟩ } = { 𝐶 }
13	2	rnsnop	⊢ ran { ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐷 }
14	12 13	uneq12i	⊢ ( ran { ⟨ 𝐴 , 𝐶 ⟩ } ∪ ran { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( { 𝐶 } ∪ { 𝐷 } )
15		df-pr	⊢ { 𝐶 , 𝐷 } = ( { 𝐶 } ∪ { 𝐷 } )
16	14 15	eqtr4i	⊢ ( ran { ⟨ 𝐴 , 𝐶 ⟩ } ∪ ran { ⟨ 𝐵 , 𝐷 ⟩ } ) = { 𝐶 , 𝐷 }
17	10 11 16	3eqtri	⊢ ran { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐶 , 𝐷 }
18	17	eqimssi	⊢ ran { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ⊆ { 𝐶 , 𝐷 }
19		df-f	⊢ ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } ↔ ( { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } Fn { 𝐴 , 𝐵 } ∧ ran { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } ⊆ { 𝐶 , 𝐷 } ) )
20	8 18 19	sylanblrc	⊢ ( 𝐴 ≠ 𝐵 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } : { 𝐴 , 𝐵 } ⟶ { 𝐶 , 𝐷 } )