Theorem fvun1 6969

Description: The value of a union when the argument is in the first domain. (Contributed by Scott Fenton, 29-Jun-2013.)

Assertion

Ref	Expression
fvun1	⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐹‘𝑋))

Proof of Theorem fvun1

Step	Hyp	Ref	Expression
1		fnfun 6632	. . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	3ad2ant1 1151	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → Fun 𝐹)
3		fnfun 6632	. . . 4 ⊢ (𝐺 Fn 𝐵 → Fun 𝐺)
4	3	3ad2ant2 1152	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → Fun 𝐺)
5		fndm 6635	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
6		fndm 6635	. . . . . . . 8 ⊢ (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵)
7	5, 6	ineqan12d 4168	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (dom 𝐹 ∩ dom 𝐺) = (𝐴 ∩ 𝐵))
8	7	eqeq1d 2762	. . . . . 6 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((dom 𝐹 ∩ dom 𝐺) = ∅ ↔ (𝐴 ∩ 𝐵) = ∅))
9	8	biimprd 251	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((𝐴 ∩ 𝐵) = ∅ → (dom 𝐹 ∩ dom 𝐺) = ∅))
10	9	adantrd 497	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴) → (dom 𝐹 ∩ dom 𝐺) = ∅))
11	10	3impia 1135	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → (dom 𝐹 ∩ dom 𝐺) = ∅)
12		fvun 6968	. . 3 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((𝐹 ∪ 𝐺)‘𝑋) = ((𝐹‘𝑋) ∪ (𝐺‘𝑋)))
13	2, 4, 11, 12	syl21anc 851	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∪ 𝐺)‘𝑋) = ((𝐹‘𝑋) ∪ (𝐺‘𝑋)))
14		disjel 4410	. . . . . . . 8 ⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴) → ¬ 𝑋 ∈ 𝐵)
15	14	adantl 487	. . . . . . 7 ⊢ ((𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ¬ 𝑋 ∈ 𝐵)
16	6	eleq2d 2846	. . . . . . . 8 ⊢ (𝐺 Fn 𝐵 → (𝑋 ∈ dom 𝐺 ↔ 𝑋 ∈ 𝐵))
17	16	adantr 486	. . . . . . 7 ⊢ ((𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → (𝑋 ∈ dom 𝐺 ↔ 𝑋 ∈ 𝐵))
18	15, 17	mtbird 328	. . . . . 6 ⊢ ((𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ¬ 𝑋 ∈ dom 𝐺)
19	18	3adant1 1148	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ¬ 𝑋 ∈ dom 𝐺)
20		ndmfv 6910	. . . . 5 ⊢ (¬ 𝑋 ∈ dom 𝐺 → (𝐺‘𝑋) = ∅)
21	19, 20	syl 18	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → (𝐺‘𝑋) = ∅)
22	21	uneq2d 4115	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ((𝐹‘𝑋) ∪ (𝐺‘𝑋)) = ((𝐹‘𝑋) ∪ ∅))
23		un0 4344	. . 3 ⊢ ((𝐹‘𝑋) ∪ ∅) = (𝐹‘𝑋)
24	22, 23	eqtrdi 2811	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ((𝐹‘𝑋) ∪ (𝐺‘𝑋)) = (𝐹‘𝑋))
25	13, 24	eqtrd 2795	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∪ 𝐺)‘𝑋) = (𝐹‘𝑋))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ∪ cun 3897   ∩ cin 3898  ∅c0 4279  dom cdm 5655  Fun wfun 6527   Fn wfn 6528  ‘cfv 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-fv 6541

This theorem is used by:  fvun2  6970  fvun1d  6971  frrlem12  8296  enfixsn  9084  ptunhmeo  24034  noextenddif  27904  axlowdimlem6  29404  axlowdimlem8  29406  axlowdimlem11  29409  vtxdun  29941  isoun  33174  cycpmfv3  33555  lbsdiflsp0  34136  sseqfv1  34900  reprsuc  35123  breprexplema  35138  cvmliftlem5  35868  fullfunfv  36526  finixpnum  38359  poimirlem1  38370  poimirlem2  38371  poimirlem3  38372  poimirlem4  38373  poimirlem6  38375  poimirlem7  38376  poimirlem11  38380  poimirlem12  38381  poimirlem16  38385  poimirlem17  38386  poimirlem19  38388  poimirlem22  38391  poimirlem23  38392  poimirlem28  38397  aacllem  50772