fvun1

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

		Ref	Expression
	Assertion	fvun1	$⊢ (F Fn A \land G Fn B \land (A \cap B = \emptyset \land X \in A)) \to (F \cup G) (X) = F (X)$

Proof

Step	Hyp	Ref	Expression
1		fnfun	$⊢ F Fn A \to Fun F$
2	1	3ad2ant1	$⊢ (F Fn A \land G Fn B \land (A \cap B = \emptyset \land X \in A)) \to Fun F$
3		fnfun	$⊢ G Fn B \to Fun G$
4	3	3ad2ant2	$⊢ (F Fn A \land G Fn B \land (A \cap B = \emptyset \land X \in A)) \to Fun G$
5		fndm	$⊢ F Fn A \to dom F = A$
6		fndm	$⊢ G Fn B \to dom G = B$
7	5 6	ineqan12d	$⊢ (F Fn A \land G Fn B) \to dom F \cap dom G = A \cap B$
8	7	eqeq1d	$⊢ (F Fn A \land G Fn B) \to (dom F \cap dom G = \emptyset \leftrightarrow A \cap B = \emptyset)$
9	8	biimprd	$⊢ (F Fn A \land G Fn B) \to (A \cap B = \emptyset \to dom F \cap dom G = \emptyset)$
10	9	adantrd	$⊢ (F Fn A \land G Fn B) \to ((A \cap B = \emptyset \land X \in A) \to dom F \cap dom G = \emptyset)$
11	10	3impia	$⊢ (F Fn A \land G Fn B \land (A \cap B = \emptyset \land X \in A)) \to dom F \cap dom G = \emptyset$
12		fvun	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to (F \cup G) (X) = F (X) \cup G (X)$
13	2 4 11 12	syl21anc	$⊢ (F Fn A \land G Fn B \land (A \cap B = \emptyset \land X \in A)) \to (F \cup G) (X) = F (X) \cup G (X)$
14		disjel	$⊢ (A \cap B = \emptyset \land X \in A) \to \neg X \in B$
15	14	adantl	$⊢ (G Fn B \land (A \cap B = \emptyset \land X \in A)) \to \neg X \in B$
16	6	eleq2d	$⊢ G Fn B \to (X \in dom G \leftrightarrow X \in B)$
17	16	adantr	$⊢ (G Fn B \land (A \cap B = \emptyset \land X \in A)) \to (X \in dom G \leftrightarrow X \in B)$
18	15 17	mtbird	$⊢ (G Fn B \land (A \cap B = \emptyset \land X \in A)) \to \neg X \in dom G$
19	18	3adant1	$⊢ (F Fn A \land G Fn B \land (A \cap B = \emptyset \land X \in A)) \to \neg X \in dom G$
20		ndmfv	$⊢ \neg X \in dom G \to G (X) = \emptyset$
21	19 20	syl	$⊢ (F Fn A \land G Fn B \land (A \cap B = \emptyset \land X \in A)) \to G (X) = \emptyset$
22	21	uneq2d	$⊢ (F Fn A \land G Fn B \land (A \cap B = \emptyset \land X \in A)) \to F (X) \cup G (X) = F (X) \cup \emptyset$
23		un0	$⊢ F (X) \cup \emptyset = F (X)$
24	22 23	eqtrdi	$⊢ (F Fn A \land G Fn B \land (A \cap B = \emptyset \land X \in A)) \to F (X) \cup G (X) = F (X)$
25	13 24	eqtrd	$⊢ (F Fn A \land G Fn B \land (A \cap B = \emptyset \land X \in A)) \to (F \cup G) (X) = F (X)$

Metamath Proof Explorer

Theorem fvun1

Proof