Description: Composition of onto functions. (Contributed by NM, 22-Mar-2006) (Proof shortened by AV, 29-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | foco | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl | |
|
2 | fofun | |
|
3 | 2 | adantl | |
4 | forn | |
|
5 | eqimss2 | |
|
6 | 4 5 | syl | |
7 | 6 | adantl | |
8 | focofo | |
|
9 | 1 3 7 8 | syl3anc | |
10 | focnvimacdmdm | |
|
11 | 10 | eqcomd | |
12 | 11 | adantl | |
13 | foeq2 | |
|
14 | 12 13 | syl | |
15 | 9 14 | mpbird | |