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 ⊢ φ → A ∈ V
brprop.b ⊢ φ → B ∈ W
brprop.c ⊢ φ → C ∈ V
brprop.d ⊢ φ → D ∈ W
mptprop.1 ⊢ φ → A ≠ C
Assertion mptprop ⊢ φ → A B C D = x ∈ A C ⟼ if x = A B D

Proof

Step Hyp Ref Expression
1 brprop.a ⊢ φ → A ∈ V
2 brprop.b ⊢ φ → B ∈ W
3 brprop.c ⊢ φ → C ∈ V
4 brprop.d ⊢ φ → D ∈ W
5 mptprop.1 ⊢ φ → A ≠ C
6 df-pr ⊢ A B C D = A B ∪ C D
7 fmptsn ⊢ A ∈ V ∧ B ∈ W → A B = x ∈ A ⟼ B
8 1 2 7 syl2anc ⊢ φ → A B = x ∈ A ⟼ B
9 incom ⊢ A ∩ A C = A C ∩ A
10 prid1g ⊢ A ∈ V → A ∈ A C
11 snssi ⊢ A ∈ A C → A ⊆ A C
12 1 10 11 3syl ⊢ φ → A ⊆ A C
13 df-ss ⊢ A ⊆ A C ↔ A ∩ A C = A
14 12 13 sylib ⊢ φ → A ∩ A C = A
15 9 14 eqtr3id ⊢ φ → A C ∩ A = A
16 15 mpteq1d ⊢ φ → x ∈ A C ∩ A ⟼ B = x ∈ A ⟼ B
17 8 16 eqtr4d ⊢ φ → A B = x ∈ A C ∩ A ⟼ B
18 fmptsn ⊢ C ∈ V ∧ D ∈ W → C D = x ∈ C ⟼ D
19 3 4 18 syl2anc ⊢ φ → C D = x ∈ C ⟼ D
20 difprsn1 ⊢ A ≠ C → A C ∖ A = C
21 5 20 syl ⊢ φ → A C ∖ A = C
22 21 mpteq1d ⊢ φ → x ∈ A C ∖ A ⟼ D = x ∈ C ⟼ D
23 19 22 eqtr4d ⊢ φ → C D = x ∈ A C ∖ A ⟼ D
24 17 23 uneq12d ⊢ φ → A B ∪ C D = x ∈ A C ∩ A ⟼ B ∪ x ∈ A C ∖ A ⟼ D
25 partfun ⊢ x ∈ A C ⟼ if x ∈ A B D = x ∈ A C ∩ A ⟼ B ∪ x ∈ A C ∖ A ⟼ D
26 24 25 eqtr4di ⊢ φ → A B ∪ C D = x ∈ A C ⟼ if x ∈ A B D
27 elsn2g ⊢ A ∈ V → x ∈ A ↔ x = A
28 1 27 syl ⊢ φ → x ∈ A ↔ x = A
29 28 ifbid ⊢ φ → if x ∈ A B D = if x = A B D
30 29 mpteq2dv ⊢ φ → x ∈ A C ⟼ if x ∈ A B D = x ∈ A C ⟼ if x = A B D
31 26 30 eqtrd ⊢ φ → A B ∪ C D = x ∈ A C ⟼ if x = A B D
32 6 31 syl5eq ⊢ φ → A B C D = x ∈ A C ⟼ if x = A B D