unfi

Description: The union of two finite sets is finite. Part of Corollary 6K of Enderton p. 144. (Contributed by NM, 16-Nov-2002)

		Ref	Expression
	Assertion	unfi	$⊢ (A \in Fin \land B \in Fin) \to A \cup B \in Fin$

Proof

Step	Hyp	Ref	Expression
1		diffi	$⊢ B \in Fin \to B ∖ A \in Fin$
2		reeanv	$⊢ \exists x \in ω \exists y \in ω (A \approx x \land (B ∖ A) \approx y) \leftrightarrow (\exists x \in ω A \approx x \land \exists y \in ω (B ∖ A) \approx y)$
3		isfi	$⊢ A \in Fin \leftrightarrow \exists x \in ω A \approx x$
4		isfi	$⊢ B ∖ A \in Fin \leftrightarrow \exists y \in ω (B ∖ A) \approx y$
5	3 4	anbi12i	$⊢ (A \in Fin \land B ∖ A \in Fin) \leftrightarrow (\exists x \in ω A \approx x \land \exists y \in ω (B ∖ A) \approx y)$
6	2 5	bitr4i	$⊢ \exists x \in ω \exists y \in ω (A \approx x \land (B ∖ A) \approx y) \leftrightarrow (A \in Fin \land B ∖ A \in Fin)$
7		nnacl	$⊢ (x \in ω \land y \in ω) \to x +_{𝑜} y \in ω$
8		unfilem3	$⊢ (x \in ω \land y \in ω) \to y \approx ((x +_{𝑜} y) ∖ x)$
9		entr	$⊢ ((B ∖ A) \approx y \land y \approx ((x +_{𝑜} y) ∖ x)) \to (B ∖ A) \approx ((x +_{𝑜} y) ∖ x)$
10	9	expcom	$⊢ y \approx ((x +_{𝑜} y) ∖ x) \to ((B ∖ A) \approx y \to (B ∖ A) \approx ((x +_{𝑜} y) ∖ x))$
11	8 10	syl	$⊢ (x \in ω \land y \in ω) \to ((B ∖ A) \approx y \to (B ∖ A) \approx ((x +_{𝑜} y) ∖ x))$
12		disjdif	$⊢ A \cap (B ∖ A) = \emptyset$
13		disjdif	$⊢ x \cap ((x +_{𝑜} y) ∖ x) = \emptyset$
14		unen	$⊢ ((A \approx x \land (B ∖ A) \approx ((x +_{𝑜} y) ∖ x)) \land (A \cap (B ∖ A) = \emptyset \land x \cap ((x +_{𝑜} y) ∖ x) = \emptyset)) \to (A \cup (B ∖ A)) \approx (x \cup ((x +_{𝑜} y) ∖ x))$
15	12 13 14	mpanr12	$⊢ (A \approx x \land (B ∖ A) \approx ((x +_{𝑜} y) ∖ x)) \to (A \cup (B ∖ A)) \approx (x \cup ((x +_{𝑜} y) ∖ x))$
16		undif2	$⊢ A \cup (B ∖ A) = A \cup B$
17	16	a1i	$⊢ (x \in ω \land y \in ω) \to A \cup (B ∖ A) = A \cup B$
18		nnaword1	$⊢ (x \in ω \land y \in ω) \to x \subseteq x +_{𝑜} y$
19		undif	$⊢ x \subseteq x +_{𝑜} y \leftrightarrow x \cup ((x +_{𝑜} y) ∖ x) = x +_{𝑜} y$
20	18 19	sylib	$⊢ (x \in ω \land y \in ω) \to x \cup ((x +_{𝑜} y) ∖ x) = x +_{𝑜} y$
21	17 20	breq12d	$⊢ (x \in ω \land y \in ω) \to ((A \cup (B ∖ A)) \approx (x \cup ((x +_{𝑜} y) ∖ x)) \leftrightarrow (A \cup B) \approx (x +_{𝑜} y))$
22	15 21	syl5ib	$⊢ (x \in ω \land y \in ω) \to ((A \approx x \land (B ∖ A) \approx ((x +_{𝑜} y) ∖ x)) \to (A \cup B) \approx (x +_{𝑜} y))$
23	11 22	sylan2d	$⊢ (x \in ω \land y \in ω) \to ((A \approx x \land (B ∖ A) \approx y) \to (A \cup B) \approx (x +_{𝑜} y))$
24		breq2	$⊢ z = x +_{𝑜} y \to ((A \cup B) \approx z \leftrightarrow (A \cup B) \approx (x +_{𝑜} y))$
25	24	rspcev	$⊢ (x +_{𝑜} y \in ω \land (A \cup B) \approx (x +_{𝑜} y)) \to \exists z \in ω (A \cup B) \approx z$
26		isfi	$⊢ A \cup B \in Fin \leftrightarrow \exists z \in ω (A \cup B) \approx z$
27	25 26	sylibr	$⊢ (x +_{𝑜} y \in ω \land (A \cup B) \approx (x +_{𝑜} y)) \to A \cup B \in Fin$
28	7 23 27	syl6an	$⊢ (x \in ω \land y \in ω) \to ((A \approx x \land (B ∖ A) \approx y) \to A \cup B \in Fin)$
29	28	rexlimivv	$⊢ \exists x \in ω \exists y \in ω (A \approx x \land (B ∖ A) \approx y) \to A \cup B \in Fin$
30	6 29	sylbir	$⊢ (A \in Fin \land B ∖ A \in Fin) \to A \cup B \in Fin$
31	1 30	sylan2	$⊢ (A \in Fin \land B \in Fin) \to A \cup B \in Fin$

Metamath Proof Explorer

Theorem unfi

Proof