Proof of Theorem fmptpr
Step | Hyp | Ref
| Expression |
1 | | df-pr 3588 |
. . 3
⊢
{〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = ({〈𝐴, 𝐶〉} ∪ {〈𝐵, 𝐷〉}) |
2 | 1 | a1i 9 |
. 2
⊢ (𝜑 → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = ({〈𝐴, 𝐶〉} ∪ {〈𝐵, 𝐷〉})) |
3 | | mpt0 5323 |
. . . . . 6
⊢ (𝑥 ∈ ∅ ↦ 𝐸) = ∅ |
4 | 3 | uneq1i 3277 |
. . . . 5
⊢ ((𝑥 ∈ ∅ ↦ 𝐸) ∪ {〈𝐴, 𝐶〉}) = (∅ ∪ {〈𝐴, 𝐶〉}) |
5 | | uncom 3271 |
. . . . 5
⊢ (∅
∪ {〈𝐴, 𝐶〉}) = ({〈𝐴, 𝐶〉} ∪ ∅) |
6 | | un0 3447 |
. . . . 5
⊢
({〈𝐴, 𝐶〉} ∪ ∅) =
{〈𝐴, 𝐶〉} |
7 | 4, 5, 6 | 3eqtri 2195 |
. . . 4
⊢ ((𝑥 ∈ ∅ ↦ 𝐸) ∪ {〈𝐴, 𝐶〉}) = {〈𝐴, 𝐶〉} |
8 | | fmptpr.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
9 | | elex 2741 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
10 | 8, 9 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ V) |
11 | | fmptpr.3 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
12 | | elex 2741 |
. . . . . 6
⊢ (𝐶 ∈ 𝑋 → 𝐶 ∈ V) |
13 | 11, 12 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ V) |
14 | | uncom 3271 |
. . . . . . 7
⊢ ({𝐴} ∪ ∅) = (∅
∪ {𝐴}) |
15 | | un0 3447 |
. . . . . . 7
⊢ ({𝐴} ∪ ∅) = {𝐴} |
16 | 14, 15 | eqtr3i 2193 |
. . . . . 6
⊢ (∅
∪ {𝐴}) = {𝐴} |
17 | 16 | a1i 9 |
. . . . 5
⊢ (𝜑 → (∅ ∪ {𝐴}) = {𝐴}) |
18 | | fmptpr.5 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐸 = 𝐶) |
19 | 10, 13, 17, 18 | fmptapd 5685 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ ∅ ↦ 𝐸) ∪ {〈𝐴, 𝐶〉}) = (𝑥 ∈ {𝐴} ↦ 𝐸)) |
20 | 7, 19 | eqtr3id 2217 |
. . 3
⊢ (𝜑 → {〈𝐴, 𝐶〉} = (𝑥 ∈ {𝐴} ↦ 𝐸)) |
21 | 20 | uneq1d 3280 |
. 2
⊢ (𝜑 → ({〈𝐴, 𝐶〉} ∪ {〈𝐵, 𝐷〉}) = ((𝑥 ∈ {𝐴} ↦ 𝐸) ∪ {〈𝐵, 𝐷〉})) |
22 | | fmptpr.2 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
23 | | elex 2741 |
. . . 4
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) |
24 | 22, 23 | syl 14 |
. . 3
⊢ (𝜑 → 𝐵 ∈ V) |
25 | | fmptpr.4 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑌) |
26 | | elex 2741 |
. . . 4
⊢ (𝐷 ∈ 𝑌 → 𝐷 ∈ V) |
27 | 25, 26 | syl 14 |
. . 3
⊢ (𝜑 → 𝐷 ∈ V) |
28 | | df-pr 3588 |
. . . . 5
⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
29 | 28 | eqcomi 2174 |
. . . 4
⊢ ({𝐴} ∪ {𝐵}) = {𝐴, 𝐵} |
30 | 29 | a1i 9 |
. . 3
⊢ (𝜑 → ({𝐴} ∪ {𝐵}) = {𝐴, 𝐵}) |
31 | | fmptpr.6 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐸 = 𝐷) |
32 | 24, 27, 30, 31 | fmptapd 5685 |
. 2
⊢ (𝜑 → ((𝑥 ∈ {𝐴} ↦ 𝐸) ∪ {〈𝐵, 𝐷〉}) = (𝑥 ∈ {𝐴, 𝐵} ↦ 𝐸)) |
33 | 2, 21, 32 | 3eqtrd 2207 |
1
⊢ (𝜑 → {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = (𝑥 ∈ {𝐴, 𝐵} ↦ 𝐸)) |