Description: Value of a function expressed as a union of a mapsto expression and a singleton on a couple (with disjoint domain) at the first component of that couple. (Contributed by BJ, 18-Mar-2023) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | bj-fvmptunsn.un | ⊢ ( 𝜑 → 𝐹 = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ) | |
| bj-fvmptunsn.nel | ⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐴 ) | ||
| bj-fvmptunsn1.ex1 | ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 ) | ||
| bj-fvmptunsn1.ex2 | ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 ) | ||
| Assertion | bj-fvmptunsn1 | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) = 𝐷 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-fvmptunsn.un | ⊢ ( 𝜑 → 𝐹 = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∪ { ⟨ 𝐶 , 𝐷 ⟩ } ) ) | |
| 2 | bj-fvmptunsn.nel | ⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐴 ) | |
| 3 | bj-fvmptunsn1.ex1 | ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 ) | |
| 4 | bj-fvmptunsn1.ex2 | ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 ) | |
| 5 | eqid | ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) | |
| 6 | 5 | dmmptss | ⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴 |
| 7 | 6 | sseli | ⊢ ( 𝐶 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝐶 ∈ 𝐴 ) |
| 8 | 2 7 | nsyl | ⊢ ( 𝜑 → ¬ 𝐶 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) |
| 9 | 1 8 3 4 | bj-fununsn2 | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) = 𝐷 ) |