| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: The union of functions with disjoint domains is a function. Theorem 4.6 of [Monk1] p. 43. |
| Ref | Expression |
|---|---|
| funun |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dffun4 4433 |
. 2
| |
| 2 | funrel 4438 |
. . . . 5
| |
| 3 | funrel 4438 |
. . . . 5
| |
| 4 | 2, 3 | anim12i 360 |
. . . 4
|
| 5 | relun 4097 |
. . . 4
| |
| 6 | 4, 5 | sylibr 217 |
. . 3
|
| 7 | 6 | adantr 425 |
. 2
|
| 8 | disj1 2915 |
. . . . . . . . . . . . 13
| |
| 9 | 8 | biimpi 168 |
. . . . . . . . . . . 12
|
| 10 | 9 | 19.21bi 1408 |
. . . . . . . . . . 11
|
| 11 | imnan 261 |
. . . . . . . . . . 11
| |
| 12 | 10, 11 | sylib 215 |
. . . . . . . . . 10
|
| 13 | visset 2295 |
. . . . . . . . . . . 12
| |
| 14 | 13 | opeldm 4160 |
. . . . . . . . . . 11
|
| 15 | 13 | opeldm 4160 |
. . . . . . . . . . 11
|
| 16 | 14, 15 | anim12i 360 |
. . . . . . . . . 10
|
| 17 | 12, 16 | nsyl 131 |
. . . . . . . . 9
|
| 18 | orel2 272 |
. . . . . . . . 9
| |
| 19 | 17, 18 | syl 12 |
. . . . . . . 8
|
| 20 | 10 | con2d 107 |
. . . . . . . . . . 11
|
| 21 | imnan 261 |
. . . . . . . . . . 11
| |
| 22 | 20, 21 | sylib 215 |
. . . . . . . . . 10
|
| 23 | 13 | opeldm 4160 |
. . . . . . . . . . 11
|
| 24 | 13 | opeldm 4160 |
. . . . . . . . . . 11
|
| 25 | 23, 24 | anim12i 360 |
. . . . . . . . . 10
|
| 26 | 22, 25 | nsyl 131 |
. . . . . . . . 9
|
| 27 | orel1 271 |
. . . . . . . . 9
| |
| 28 | 26, 27 | syl 12 |
. . . . . . . 8
|
| 29 | 19, 28 | orim12d 624 |
. . . . . . 7
|
| 30 | 29 | adantl 424 |
. . . . . 6
|
| 31 | elun 2741 |
. . . . . . . 8
| |
| 32 | elun 2741 |
. . . . . . . 8
| |
| 33 | 31, 32 | anbi12i 540 |
. . . . . . 7
|
| 34 | anddi 668 |
. . . . . . 7
| |
| 35 | 33, 34 | bitri 190 |
. . . . . 6
|
| 36 | 30, 35 | syl5ib 223 |
. . . . 5
|
| 37 | dffun4 4433 |
. . . . . . . . . 10
| |
| 38 | 37 | simprbi 353 |
. . . . . . . . 9
|
| 39 | 38 | 19.21bi 1408 |
. . . . . . . 8
|
| 40 | 39 | 19.21bbi 1409 |
. . . . . . 7
|
| 41 | dffun4 4433 |
. . . . . . . . . 10
| |
| 42 | 41 | simprbi 353 |
. . . . . . . . 9
|
| 43 | 42 | 19.21bi 1408 |
. . . . . . . 8
|
| 44 | 43 | 19.21bbi 1409 |
. . . . . . 7
|
| 45 | 40, 44 | jaao 472 |
. . . . . 6
|
| 46 | 45 | adantr 425 |
. . . . 5
|
| 47 | 36, 46 | syld 30 |
. . . 4
|
| 48 | 47 | 19.21aiv 1664 |
. . 3
|
| 49 | 48 | 19.21aivv 1665 |
. 2
|
| 50 | 1, 7, 49 | sylanbrc 527 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: funprg 4466 funtp 4468 fnun 4520 tfrlem10 5128 sbthlem7 5516 sbthlem8 5517 fodomr 5547 bnj1421 13532 wfrlem13 13969 valfunun 14460 repfuntw 14502 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 |
| This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-v 2294 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-nul 2876 df-pw 3035 df-sn 3049 df-pr 3050 df-op 3053 df-br 3339 df-opab 3396 df-id 3586 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-fun 4008 |