Description: Value of a function expressed as a union of a function 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-fununsn.un | ⊢ ( 𝜑 → 𝐹 = ( 𝐺 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) ) | |
| bj-fununsn2.neldm | ⊢ ( 𝜑 → ¬ 𝐵 ∈ dom 𝐺 ) | ||
| bj-fununsn2.ex1 | ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 ) | ||
| bj-fununsn2.ex2 | ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 ) | ||
| Assertion | bj-fununsn2 | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) = 𝐶 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-fununsn.un | ⊢ ( 𝜑 → 𝐹 = ( 𝐺 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) ) | |
| 2 | bj-fununsn2.neldm | ⊢ ( 𝜑 → ¬ 𝐵 ∈ dom 𝐺 ) | |
| 3 | bj-fununsn2.ex1 | ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 ) | |
| 4 | bj-fununsn2.ex2 | ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 ) | |
| 5 | uncom | ⊢ ( 𝐺 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) = ( { ⟨ 𝐵 , 𝐶 ⟩ } ∪ 𝐺 ) | |
| 6 | 1 5 | eqtrdi | ⊢ ( 𝜑 → 𝐹 = ( { ⟨ 𝐵 , 𝐶 ⟩ } ∪ 𝐺 ) ) |
| 7 | 6 2 | bj-funun | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) = ( { ⟨ 𝐵 , 𝐶 ⟩ } ‘ 𝐵 ) ) |
| 8 | fvsng | ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( { ⟨ 𝐵 , 𝐶 ⟩ } ‘ 𝐵 ) = 𝐶 ) | |
| 9 | 3 4 8 | syl2anc | ⊢ ( 𝜑 → ( { ⟨ 𝐵 , 𝐶 ⟩ } ‘ 𝐵 ) = 𝐶 ) |
| 10 | 7 9 | eqtrd | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) = 𝐶 ) |