Proof of Theorem mptprop
| Step | Hyp | Ref
| Expression |
| 1 | | df-pr 4629 |
. 2
⊢
{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = ({〈𝐴, 𝐵〉} ∪ {〈𝐶, 𝐷〉}) |
| 2 | | brprop.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 3 | | brprop.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
| 4 | | fmptsn 7187 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {〈𝐴, 𝐵〉} = (𝑥 ∈ {𝐴} ↦ 𝐵)) |
| 5 | 2, 3, 4 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → {〈𝐴, 𝐵〉} = (𝑥 ∈ {𝐴} ↦ 𝐵)) |
| 6 | | incom 4209 |
. . . . . . . 8
⊢ ({𝐴} ∩ {𝐴, 𝐶}) = ({𝐴, 𝐶} ∩ {𝐴}) |
| 7 | | prid1g 4760 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐶}) |
| 8 | | snssi 4808 |
. . . . . . . . . 10
⊢ (𝐴 ∈ {𝐴, 𝐶} → {𝐴} ⊆ {𝐴, 𝐶}) |
| 9 | 2, 7, 8 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → {𝐴} ⊆ {𝐴, 𝐶}) |
| 10 | | dfss2 3969 |
. . . . . . . . 9
⊢ ({𝐴} ⊆ {𝐴, 𝐶} ↔ ({𝐴} ∩ {𝐴, 𝐶}) = {𝐴}) |
| 11 | 9, 10 | sylib 218 |
. . . . . . . 8
⊢ (𝜑 → ({𝐴} ∩ {𝐴, 𝐶}) = {𝐴}) |
| 12 | 6, 11 | eqtr3id 2791 |
. . . . . . 7
⊢ (𝜑 → ({𝐴, 𝐶} ∩ {𝐴}) = {𝐴}) |
| 13 | 12 | mpteq1d 5237 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ({𝐴, 𝐶} ∩ {𝐴}) ↦ 𝐵) = (𝑥 ∈ {𝐴} ↦ 𝐵)) |
| 14 | 5, 13 | eqtr4d 2780 |
. . . . 5
⊢ (𝜑 → {〈𝐴, 𝐵〉} = (𝑥 ∈ ({𝐴, 𝐶} ∩ {𝐴}) ↦ 𝐵)) |
| 15 | | brprop.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
| 16 | | brprop.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝑊) |
| 17 | | fmptsn 7187 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → {〈𝐶, 𝐷〉} = (𝑥 ∈ {𝐶} ↦ 𝐷)) |
| 18 | 15, 16, 17 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → {〈𝐶, 𝐷〉} = (𝑥 ∈ {𝐶} ↦ 𝐷)) |
| 19 | | mptprop.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≠ 𝐶) |
| 20 | | difprsn1 4800 |
. . . . . . . 8
⊢ (𝐴 ≠ 𝐶 → ({𝐴, 𝐶} ∖ {𝐴}) = {𝐶}) |
| 21 | 19, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ({𝐴, 𝐶} ∖ {𝐴}) = {𝐶}) |
| 22 | 21 | mpteq1d 5237 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ({𝐴, 𝐶} ∖ {𝐴}) ↦ 𝐷) = (𝑥 ∈ {𝐶} ↦ 𝐷)) |
| 23 | 18, 22 | eqtr4d 2780 |
. . . . 5
⊢ (𝜑 → {〈𝐶, 𝐷〉} = (𝑥 ∈ ({𝐴, 𝐶} ∖ {𝐴}) ↦ 𝐷)) |
| 24 | 14, 23 | uneq12d 4169 |
. . . 4
⊢ (𝜑 → ({〈𝐴, 𝐵〉} ∪ {〈𝐶, 𝐷〉}) = ((𝑥 ∈ ({𝐴, 𝐶} ∩ {𝐴}) ↦ 𝐵) ∪ (𝑥 ∈ ({𝐴, 𝐶} ∖ {𝐴}) ↦ 𝐷))) |
| 25 | | partfun 6715 |
. . . 4
⊢ (𝑥 ∈ {𝐴, 𝐶} ↦ if(𝑥 ∈ {𝐴}, 𝐵, 𝐷)) = ((𝑥 ∈ ({𝐴, 𝐶} ∩ {𝐴}) ↦ 𝐵) ∪ (𝑥 ∈ ({𝐴, 𝐶} ∖ {𝐴}) ↦ 𝐷)) |
| 26 | 24, 25 | eqtr4di 2795 |
. . 3
⊢ (𝜑 → ({〈𝐴, 𝐵〉} ∪ {〈𝐶, 𝐷〉}) = (𝑥 ∈ {𝐴, 𝐶} ↦ if(𝑥 ∈ {𝐴}, 𝐵, 𝐷))) |
| 27 | | elsn2g 4664 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)) |
| 28 | 2, 27 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)) |
| 29 | 28 | ifbid 4549 |
. . . 4
⊢ (𝜑 → if(𝑥 ∈ {𝐴}, 𝐵, 𝐷) = if(𝑥 = 𝐴, 𝐵, 𝐷)) |
| 30 | 29 | mpteq2dv 5244 |
. . 3
⊢ (𝜑 → (𝑥 ∈ {𝐴, 𝐶} ↦ if(𝑥 ∈ {𝐴}, 𝐵, 𝐷)) = (𝑥 ∈ {𝐴, 𝐶} ↦ if(𝑥 = 𝐴, 𝐵, 𝐷))) |
| 31 | 26, 30 | eqtrd 2777 |
. 2
⊢ (𝜑 → ({〈𝐴, 𝐵〉} ∪ {〈𝐶, 𝐷〉}) = (𝑥 ∈ {𝐴, 𝐶} ↦ if(𝑥 = 𝐴, 𝐵, 𝐷))) |
| 32 | 1, 31 | eqtrid 2789 |
1
⊢ (𝜑 → {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = (𝑥 ∈ {𝐴, 𝐶} ↦ if(𝑥 = 𝐴, 𝐵, 𝐷))) |