Metamath Proof Explorer

Theorem mptprop

Description: Rewrite pairs of ordered pairs as mapping to functions. (Contributed by Thierry Arnoux, 24-Sep-2023)

Ref Expression
Hypotheses brprop.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
brprop.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
brprop.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
brprop.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
mptprop.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
Assertion mptprop ( 𝜑 → { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ( 𝑥 ∈ { 𝐴 , 𝐶 } ↦ if ( 𝑥 = 𝐴 , 𝐵 , 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 brprop.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 brprop.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 brprop.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4 brprop.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5 mptprop.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
6 df-pr ⊢ { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } )
7 fmptsn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) )
8 1 2 7 syl2anc ⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐵 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) )
9 incom ⊢ ( { 𝐴 } ∩ { 𝐴 , 𝐶 } ) = ( { 𝐴 , 𝐶 } ∩ { 𝐴 } )
10 prid1g ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 , 𝐶 } )
11 snssi ⊢ ( 𝐴 ∈ { 𝐴 , 𝐶 } → { 𝐴 } ⊆ { 𝐴 , 𝐶 } )
12 1 10 11 3syl ⊢ ( 𝜑 → { 𝐴 } ⊆ { 𝐴 , 𝐶 } )
13 df-ss ⊢ ( { 𝐴 } ⊆ { 𝐴 , 𝐶 } ↔ ( { 𝐴 } ∩ { 𝐴 , 𝐶 } ) = { 𝐴 } )
14 12 13 sylib ⊢ ( 𝜑 → ( { 𝐴 } ∩ { 𝐴 , 𝐶 } ) = { 𝐴 } )
15 9 14 eqtr3id ⊢ ( 𝜑 → ( { 𝐴 , 𝐶 } ∩ { 𝐴 } ) = { 𝐴 } )
16 15 mpteq1d ⊢ ( 𝜑 → ( 𝑥 ∈ ( { 𝐴 , 𝐶 } ∩ { 𝐴 } ) ↦ 𝐵 ) = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) )
17 8 16 eqtr4d ⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐵 ⟩ } = ( 𝑥 ∈ ( { 𝐴 , 𝐶 } ∩ { 𝐴 } ) ↦ 𝐵 ) )
18 fmptsn ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) → { ⟨ 𝐶 , 𝐷 ⟩ } = ( 𝑥 ∈ { 𝐶 } ↦ 𝐷 ) )
19 3 4 18 syl2anc ⊢ ( 𝜑 → { ⟨ 𝐶 , 𝐷 ⟩ } = ( 𝑥 ∈ { 𝐶 } ↦ 𝐷 ) )
20 difprsn1 ⊢ ( 𝐴 ≠ 𝐶 → ( { 𝐴 , 𝐶 } ∖ { 𝐴 } ) = { 𝐶 } )
21 5 20 syl ⊢ ( 𝜑 → ( { 𝐴 , 𝐶 } ∖ { 𝐴 } ) = { 𝐶 } )
22 21 mpteq1d ⊢ ( 𝜑 → ( 𝑥 ∈ ( { 𝐴 , 𝐶 } ∖ { 𝐴 } ) ↦ 𝐷 ) = ( 𝑥 ∈ { 𝐶 } ↦ 𝐷 ) )
23 19 22 eqtr4d ⊢ ( 𝜑 → { ⟨ 𝐶 , 𝐷 ⟩ } = ( 𝑥 ∈ ( { 𝐴 , 𝐶 } ∖ { 𝐴 } ) ↦ 𝐷 ) )
24 17 23 uneq12d ⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) = ( ( 𝑥 ∈ ( { 𝐴 , 𝐶 } ∩ { 𝐴 } ) ↦ 𝐵 ) ∪ ( 𝑥 ∈ ( { 𝐴 , 𝐶 } ∖ { 𝐴 } ) ↦ 𝐷 ) ) )
25 partfun ⊢ ( 𝑥 ∈ { 𝐴 , 𝐶 } ↦ if ( 𝑥 ∈ { 𝐴 } , 𝐵 , 𝐷 ) ) = ( ( 𝑥 ∈ ( { 𝐴 , 𝐶 } ∩ { 𝐴 } ) ↦ 𝐵 ) ∪ ( 𝑥 ∈ ( { 𝐴 , 𝐶 } ∖ { 𝐴 } ) ↦ 𝐷 ) )
26 24 25 eqtr4di ⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) = ( 𝑥 ∈ { 𝐴 , 𝐶 } ↦ if ( 𝑥 ∈ { 𝐴 } , 𝐵 , 𝐷 ) ) )
27 elsn2g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 ) )
28 1 27 syl ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 ) )
29 28 ifbid ⊢ ( 𝜑 → if ( 𝑥 ∈ { 𝐴 } , 𝐵 , 𝐷 ) = if ( 𝑥 = 𝐴 , 𝐵 , 𝐷 ) )
30 29 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝐴 , 𝐶 } ↦ if ( 𝑥 ∈ { 𝐴 } , 𝐵 , 𝐷 ) ) = ( 𝑥 ∈ { 𝐴 , 𝐶 } ↦ if ( 𝑥 = 𝐴 , 𝐵 , 𝐷 ) ) )
31 26 30 eqtrd ⊢ ( 𝜑 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) = ( 𝑥 ∈ { 𝐴 , 𝐶 } ↦ if ( 𝑥 = 𝐴 , 𝐵 , 𝐷 ) ) )
32 6 31 eqtrid ⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ( 𝑥 ∈ { 𝐴 , 𝐶 } ↦ if ( 𝑥 = 𝐴 , 𝐵 , 𝐷 ) ) )