This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ( 𝑥 ∈ { 𝐴 , 𝐵 } ↦ 𝐸 ) )