Description: Value of a function expressed as a union of a mapsto expression and a singleton on a couple (with disjoint domain) at a point in the domain of the mapsto construction. (Contributed by BJ, 18-Mar-2023) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | bj-fvmptunsn.un | ⊢ ( 𝜑 → 𝐹 = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ) | |
| bj-fvmptunsn.nel | ⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐴 ) | ||
| bj-fvmptunsn2.el | ⊢ ( 𝜑 → 𝐸 ∈ 𝐴 ) | ||
| bj-fvmptunsn2.ex | ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 ) | ||
| bj-fvmptunsn2.is | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐸 ) → 𝐵 = 𝐺 ) | ||
| Assertion | bj-fvmptunsn2 | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐸 ) = 𝐺 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-fvmptunsn.un | ⊢ ( 𝜑 → 𝐹 = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ) | |
| 2 | bj-fvmptunsn.nel | ⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐴 ) | |
| 3 | bj-fvmptunsn2.el | ⊢ ( 𝜑 → 𝐸 ∈ 𝐴 ) | |
| 4 | bj-fvmptunsn2.ex | ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 ) | |
| 5 | bj-fvmptunsn2.is | ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐸 ) → 𝐵 = 𝐺 ) | |
| 6 | nelneq | ⊢ ( ( 𝐸 ∈ 𝐴 ∧ ¬ 𝐶 ∈ 𝐴 ) → ¬ 𝐸 = 𝐶 ) | |
| 7 | 3 2 6 | syl2anc | ⊢ ( 𝜑 → ¬ 𝐸 = 𝐶 ) |
| 8 | 1 7 | bj-fununsn1 | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐸 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝐸 ) ) |
| 9 | eqidd | ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) | |
| 10 | 9 5 3 4 | fvmptd | ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝐸 ) = 𝐺 ) |
| 11 | 8 10 | eqtrd | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐸 ) = 𝐺 ) |