Theorem fmptpr

Description: Express a pair function in maps-to notation. (Contributed by Thierry Arnoux, 3-Jan-2017)

	Ref	Expression
Hypotheses	fmptpr.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	fmptpr.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	fmptpr.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
	fmptpr.4	⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
	fmptpr.5	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐸 = 𝐶 )
	fmptpr.6	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝐸 = 𝐷 )
Assertion	fmptpr	⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ( 𝑥 ∈ { 𝐴 , 𝐵 } ↦ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		fmptpr.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		fmptpr.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		fmptpr.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
4		fmptpr.4	⊢ ( 𝜑 → 𝐷 ∈ 𝑌 )
5		fmptpr.5	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐸 = 𝐶 )
6		fmptpr.6	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐵 ) → 𝐸 = 𝐷 )
7		df-pr	⊢ { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } )
8	7	a1i	⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) )
9	5 1 3	fmptsnd	⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐶 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐸 ) )
10	9	uneq1d	⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( ( 𝑥 ∈ { 𝐴 } ↦ 𝐸 ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) )
11		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
12	11	eqcomi	⊢ ( { 𝐴 } ∪ { 𝐵 } ) = { 𝐴 , 𝐵 }
13	12	a1i	⊢ ( 𝜑 → ( { 𝐴 } ∪ { 𝐵 } ) = { 𝐴 , 𝐵 } )
14	2 4 13 6	fmptapd	⊢ ( 𝜑 → ( ( 𝑥 ∈ { 𝐴 } ↦ 𝐸 ) ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( 𝑥 ∈ { 𝐴 , 𝐵 } ↦ 𝐸 ) )
15	8 10 14	3eqtrd	⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ( 𝑥 ∈ { 𝐴 , 𝐵 } ↦ 𝐸 ) )