Description: The union of functions with disjoint domains is a function, deduction version of fun2 . (Contributed by AV, 11-Oct-2020) (Revised by AV, 24-Oct-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | fun2d.f | |- ( ph -> F : A --> C ) |
|
| fun2d.g | |- ( ph -> G : B --> C ) |
||
| fun2d.i | |- ( ph -> ( A i^i B ) = (/) ) |
||
| Assertion | fun2d | |- ( ph -> ( F u. G ) : ( A u. B ) --> C ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fun2d.f | |- ( ph -> F : A --> C ) |
|
| 2 | fun2d.g | |- ( ph -> G : B --> C ) |
|
| 3 | fun2d.i | |- ( ph -> ( A i^i B ) = (/) ) |
|
| 4 | fun2 | |- ( ( ( F : A --> C /\ G : B --> C ) /\ ( A i^i B ) = (/) ) -> ( F u. G ) : ( A u. B ) --> C ) |
|
| 5 | 1 2 3 4 | syl21anc | |- ( ph -> ( F u. G ) : ( A u. B ) --> C ) |