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