This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvun

Description: Value of the union of two functions when the domains are separate. (Contributed by FL, 7-Nov-2011)

		Ref	Expression
	Assertion	fvun	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to (F \cup G) (A) = F (A) \cup G (A)$

Proof

Step	Hyp	Ref	Expression
1		funun	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to Fun (F \cup G)$
2		funfv	$⊢ Fun (F \cup G) \to (F \cup G) (A) = ⋃ (F \cup G) [\{A\}]$
3	1 2	syl	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to (F \cup G) (A) = ⋃ (F \cup G) [\{A\}]$
4		imaundir	$⊢ (F \cup G) [\{A\}] = F [\{A\}] \cup G [\{A\}]$
5	4	a1i	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to (F \cup G) [\{A\}] = F [\{A\}] \cup G [\{A\}]$
6	5	unieqd	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to ⋃ (F \cup G) [\{A\}] = ⋃ (F [\{A\}] \cup G [\{A\}])$
7		uniun	$⊢ ⋃ (F [\{A\}] \cup G [\{A\}]) = ⋃ F [\{A\}] \cup ⋃ G [\{A\}]$
8		funfv	$⊢ Fun F \to F (A) = ⋃ F [\{A\}]$
9	8	eqcomd	$⊢ Fun F \to ⋃ F [\{A\}] = F (A)$
10		funfv	$⊢ Fun G \to G (A) = ⋃ G [\{A\}]$
11	10	eqcomd	$⊢ Fun G \to ⋃ G [\{A\}] = G (A)$
12	9 11	anim12i	$⊢ (Fun F \land Fun G) \to (⋃ F [\{A\}] = F (A) \land ⋃ G [\{A\}] = G (A))$
13	12	adantr	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to (⋃ F [\{A\}] = F (A) \land ⋃ G [\{A\}] = G (A))$
14		uneq12	$⊢ (⋃ F [\{A\}] = F (A) \land ⋃ G [\{A\}] = G (A)) \to ⋃ F [\{A\}] \cup ⋃ G [\{A\}] = F (A) \cup G (A)$
15	13 14	syl	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to ⋃ F [\{A\}] \cup ⋃ G [\{A\}] = F (A) \cup G (A)$
16	7 15	eqtrid	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to ⋃ (F [\{A\}] \cup G [\{A\}]) = F (A) \cup G (A)$
17	3 6 16	3eqtrd	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to (F \cup G) (A) = F (A) \cup G (A)$