Description: If the union of classes is a function, the classes themselves are functions. (Contributed by AV, 18-Jul-2019) Shorten proof and remove dependency on ax-sep and ax-pr . (Revised by Eric Schmidt, 24-Oct-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fununfun | |- ( Fun ( F u. G ) -> ( Fun F /\ Fun G ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssun1 | |- F C_ ( F u. G ) |
|
| 2 | funss | |- ( F C_ ( F u. G ) -> ( Fun ( F u. G ) -> Fun F ) ) |
|
| 3 | 1 2 | ax-mp | |- ( Fun ( F u. G ) -> Fun F ) |
| 4 | ssun2 | |- G C_ ( F u. G ) |
|
| 5 | funss | |- ( G C_ ( F u. G ) -> ( Fun ( F u. G ) -> Fun G ) ) |
|
| 6 | 4 5 | ax-mp | |- ( Fun ( F u. G ) -> Fun G ) |
| 7 | 3 6 | jca | |- ( Fun ( F u. G ) -> ( Fun F /\ Fun G ) ) |