![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvun1 | Structured version Visualization version GIF version |
Description: The value of a union when the argument is in the first domain. (Contributed by Scott Fenton, 29-Jun-2013.) |
Ref | Expression |
---|---|
fvun1 | ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐹‘𝑋)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnfun 6603 | . . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) | |
2 | 1 | 3ad2ant1 1134 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → Fun 𝐹) |
3 | fnfun 6603 | . . . 4 ⊢ (𝐺 Fn 𝐵 → Fun 𝐺) | |
4 | 3 | 3ad2ant2 1135 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → Fun 𝐺) |
5 | fndm 6606 | . . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
6 | fndm 6606 | . . . . . . . 8 ⊢ (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵) | |
7 | 5, 6 | ineqan12d 4175 | . . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (dom 𝐹 ∩ dom 𝐺) = (𝐴 ∩ 𝐵)) |
8 | 7 | eqeq1d 2739 | . . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((dom 𝐹 ∩ dom 𝐺) = ∅ ↔ (𝐴 ∩ 𝐵) = ∅)) |
9 | 8 | biimprd 248 | . . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((𝐴 ∩ 𝐵) = ∅ → (dom 𝐹 ∩ dom 𝐺) = ∅)) |
10 | 9 | adantrd 493 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴) → (dom 𝐹 ∩ dom 𝐺) = ∅)) |
11 | 10 | 3impia 1118 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → (dom 𝐹 ∩ dom 𝐺) = ∅) |
12 | fvun 6932 | . . 3 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((𝐹 ∪ 𝐺)‘𝑋) = ((𝐹‘𝑋) ∪ (𝐺‘𝑋))) | |
13 | 2, 4, 11, 12 | syl21anc 837 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∪ 𝐺)‘𝑋) = ((𝐹‘𝑋) ∪ (𝐺‘𝑋))) |
14 | disjel 4417 | . . . . . . . 8 ⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴) → ¬ 𝑋 ∈ 𝐵) | |
15 | 14 | adantl 483 | . . . . . . 7 ⊢ ((𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ¬ 𝑋 ∈ 𝐵) |
16 | 6 | eleq2d 2824 | . . . . . . . 8 ⊢ (𝐺 Fn 𝐵 → (𝑋 ∈ dom 𝐺 ↔ 𝑋 ∈ 𝐵)) |
17 | 16 | adantr 482 | . . . . . . 7 ⊢ ((𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → (𝑋 ∈ dom 𝐺 ↔ 𝑋 ∈ 𝐵)) |
18 | 15, 17 | mtbird 325 | . . . . . 6 ⊢ ((𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ¬ 𝑋 ∈ dom 𝐺) |
19 | 18 | 3adant1 1131 | . . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ¬ 𝑋 ∈ dom 𝐺) |
20 | ndmfv 6878 | . . . . 5 ⊢ (¬ 𝑋 ∈ dom 𝐺 → (𝐺‘𝑋) = ∅) | |
21 | 19, 20 | syl 17 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → (𝐺‘𝑋) = ∅) |
22 | 21 | uneq2d 4124 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ((𝐹‘𝑋) ∪ (𝐺‘𝑋)) = ((𝐹‘𝑋) ∪ ∅)) |
23 | un0 4351 | . . 3 ⊢ ((𝐹‘𝑋) ∪ ∅) = (𝐹‘𝑋) | |
24 | 22, 23 | eqtrdi 2793 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ((𝐹‘𝑋) ∪ (𝐺‘𝑋)) = (𝐹‘𝑋)) |
25 | 13, 24 | eqtrd 2777 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐹‘𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ∪ cun 3909 ∩ cin 3910 ∅c0 4283 dom cdm 5634 Fun wfun 6491 Fn wfn 6492 ‘cfv 6497 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2708 ax-sep 5257 ax-nul 5264 ax-pr 5385 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-ne 2945 df-ral 3066 df-rex 3075 df-rab 3409 df-v 3448 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-opab 5169 df-id 5532 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-iota 6449 df-fun 6499 df-fn 6500 df-fv 6505 |
This theorem is referenced by: fvun2 6934 fvun1d 6935 frrlem12 8229 enfixsn 9026 ptunhmeo 23162 noextenddif 27019 axlowdimlem6 27899 axlowdimlem8 27901 axlowdimlem11 27904 vtxdun 28432 isoun 31618 cycpmfv3 31967 lbsdiflsp0 32324 sseqfv1 32992 reprsuc 33231 breprexplema 33246 cvmliftlem5 33886 fullfunfv 34535 finixpnum 36066 poimirlem1 36082 poimirlem2 36083 poimirlem3 36084 poimirlem4 36085 poimirlem6 36087 poimirlem7 36088 poimirlem11 36092 poimirlem12 36093 poimirlem16 36097 poimirlem17 36098 poimirlem19 36100 poimirlem22 36103 poimirlem23 36104 poimirlem28 36109 aacllem 47255 |
Copyright terms: Public domain | W3C validator |