Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fun | Structured version Visualization version GIF version |
Description: The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.) |
Ref | Expression |
---|---|
fun | ⊢ (((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐷) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶(𝐶 ∪ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnun 6487 | . . . . 5 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵)) | |
2 | 1 | expcom 417 | . . . 4 ⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵))) |
3 | rnun 6006 | . . . . 5 ⊢ ran (𝐹 ∪ 𝐺) = (ran 𝐹 ∪ ran 𝐺) | |
4 | unss12 4093 | . . . . 5 ⊢ ((ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷) → (ran 𝐹 ∪ ran 𝐺) ⊆ (𝐶 ∪ 𝐷)) | |
5 | 3, 4 | eqsstrid 3946 | . . . 4 ⊢ ((ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷) → ran (𝐹 ∪ 𝐺) ⊆ (𝐶 ∪ 𝐷)) |
6 | 2, 5 | anim12d1 613 | . . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ → (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷)) → ((𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵) ∧ ran (𝐹 ∪ 𝐺) ⊆ (𝐶 ∪ 𝐷)))) |
7 | df-f 6381 | . . . . 5 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)) | |
8 | df-f 6381 | . . . . 5 ⊢ (𝐺:𝐵⟶𝐷 ↔ (𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐷)) | |
9 | 7, 8 | anbi12i 630 | . . . 4 ⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐷) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶) ∧ (𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐷))) |
10 | an4 656 | . . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶) ∧ (𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐷)) ↔ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷))) | |
11 | 9, 10 | bitri 278 | . . 3 ⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐷) ↔ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷))) |
12 | df-f 6381 | . . 3 ⊢ ((𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶(𝐶 ∪ 𝐷) ↔ ((𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵) ∧ ran (𝐹 ∪ 𝐺) ⊆ (𝐶 ∪ 𝐷))) | |
13 | 6, 11, 12 | 3imtr4g 299 | . 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐷) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶(𝐶 ∪ 𝐷))) |
14 | 13 | impcom 411 | 1 ⊢ (((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐷) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶(𝐶 ∪ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∪ cun 3861 ∩ cin 3862 ⊆ wss 3863 ∅c0 4234 ran crn 5549 Fn wfn 6372 ⟶wf 6373 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5189 ax-nul 5196 ax-pr 5319 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ral 3063 df-rab 3067 df-v 3407 df-dif 3866 df-un 3868 df-in 3870 df-ss 3880 df-nul 4235 df-if 4437 df-sn 4539 df-pr 4541 df-op 4545 df-br 5051 df-opab 5113 df-id 5452 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-fun 6379 df-fn 6380 df-f 6381 |
This theorem is referenced by: fun2 6579 ftpg 6968 fsnunf 6997 ralxpmap 8574 hashfxnn0 13900 cats1un 14283 pwssplit1 20093 axlowdimlem10 27039 wlkp1 27766 padct 30771 eulerpartlemt 32047 sseqf 32068 poimirlem3 35515 poimirlem16 35528 poimirlem19 35531 poimirlem22 35534 poimirlem23 35535 poimirlem24 35536 poimirlem25 35537 poimirlem28 35540 poimirlem29 35541 poimirlem31 35543 mapfzcons 40239 diophrw 40282 diophren 40336 pwssplit4 40615 aacllem 46174 |
Copyright terms: Public domain | W3C validator |