unfilem1

Description: Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 10-Nov-2002) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypotheses	unfilem1.1	$⊢ A \in ω$
	unfilem1.2	$⊢ B \in ω$
	unfilem1.3	$⊢ F = (x \in B ⟼ A +_{𝑜} x)$
Assertion	unfilem1	$⊢ ran F = (A +_{𝑜} B) ∖ A$

Proof

Step	Hyp	Ref	Expression
1		unfilem1.1	$⊢ A \in ω$
2		unfilem1.2	$⊢ B \in ω$
3		unfilem1.3	$⊢ F = (x \in B ⟼ A +_{𝑜} x)$
4		elnn	$⊢ (x \in B \land B \in ω) \to x \in ω$
5	2 4	mpan2	$⊢ x \in B \to x \in ω$
6		nnaord	$⊢ (x \in ω \land B \in ω \land A \in ω) \to (x \in B \leftrightarrow A +_{𝑜} x \in (A +_{𝑜} B))$
7	2 1 6	mp3an23	$⊢ x \in ω \to (x \in B \leftrightarrow A +_{𝑜} x \in (A +_{𝑜} B))$
8	5 7	syl	$⊢ x \in B \to (x \in B \leftrightarrow A +_{𝑜} x \in (A +_{𝑜} B))$
9	8	ibi	$⊢ x \in B \to A +_{𝑜} x \in (A +_{𝑜} B)$
10		nnaword1	$⊢ (A \in ω \land x \in ω) \to A \subseteq A +_{𝑜} x$
11		nnord	$⊢ A \in ω \to Ord A$
12		nnacl	$⊢ (A \in ω \land x \in ω) \to A +_{𝑜} x \in ω$
13		nnord	$⊢ A +_{𝑜} x \in ω \to Ord (A +_{𝑜} x)$
14	12 13	syl	$⊢ (A \in ω \land x \in ω) \to Ord (A +_{𝑜} x)$
15		ordtri1	$⊢ (Ord A \land Ord (A +_{𝑜} x)) \to (A \subseteq A +_{𝑜} x \leftrightarrow \neg A +_{𝑜} x \in A)$
16	11 14 15	syl2an2r	$⊢ (A \in ω \land x \in ω) \to (A \subseteq A +_{𝑜} x \leftrightarrow \neg A +_{𝑜} x \in A)$
17	10 16	mpbid	$⊢ (A \in ω \land x \in ω) \to \neg A +_{𝑜} x \in A$
18	1 5 17	sylancr	$⊢ x \in B \to \neg A +_{𝑜} x \in A$
19	9 18	jca	$⊢ x \in B \to (A +_{𝑜} x \in (A +_{𝑜} B) \land \neg A +_{𝑜} x \in A)$
20		eleq1	$⊢ y = A +_{𝑜} x \to (y \in (A +_{𝑜} B) \leftrightarrow A +_{𝑜} x \in (A +_{𝑜} B))$
21		eleq1	$⊢ y = A +_{𝑜} x \to (y \in A \leftrightarrow A +_{𝑜} x \in A)$
22	21	notbid	$⊢ y = A +_{𝑜} x \to (\neg y \in A \leftrightarrow \neg A +_{𝑜} x \in A)$
23	20 22	anbi12d	$⊢ y = A +_{𝑜} x \to ((y \in (A +_{𝑜} B) \land \neg y \in A) \leftrightarrow (A +_{𝑜} x \in (A +_{𝑜} B) \land \neg A +_{𝑜} x \in A))$
24	23	biimparc	$⊢ ((A +_{𝑜} x \in (A +_{𝑜} B) \land \neg A +_{𝑜} x \in A) \land y = A +_{𝑜} x) \to (y \in (A +_{𝑜} B) \land \neg y \in A)$
25	19 24	sylan	$⊢ (x \in B \land y = A +_{𝑜} x) \to (y \in (A +_{𝑜} B) \land \neg y \in A)$
26	25	rexlimiva	$⊢ \exists x \in B y = A +_{𝑜} x \to (y \in (A +_{𝑜} B) \land \neg y \in A)$
27	1 2	nnacli	$⊢ A +_{𝑜} B \in ω$
28		elnn	$⊢ (y \in (A +_{𝑜} B) \land A +_{𝑜} B \in ω) \to y \in ω$
29	27 28	mpan2	$⊢ y \in (A +_{𝑜} B) \to y \in ω$
30		nnord	$⊢ y \in ω \to Ord y$
31		ordtri1	$⊢ (Ord A \land Ord y) \to (A \subseteq y \leftrightarrow \neg y \in A)$
32	11 30 31	syl2an	$⊢ (A \in ω \land y \in ω) \to (A \subseteq y \leftrightarrow \neg y \in A)$
33		nnawordex	$⊢ (A \in ω \land y \in ω) \to (A \subseteq y \leftrightarrow \exists x \in ω A +_{𝑜} x = y)$
34	32 33	bitr3d	$⊢ (A \in ω \land y \in ω) \to (\neg y \in A \leftrightarrow \exists x \in ω A +_{𝑜} x = y)$
35	1 29 34	sylancr	$⊢ y \in (A +_{𝑜} B) \to (\neg y \in A \leftrightarrow \exists x \in ω A +_{𝑜} x = y)$
36		eleq1	$⊢ A +_{𝑜} x = y \to (A +_{𝑜} x \in (A +_{𝑜} B) \leftrightarrow y \in (A +_{𝑜} B))$
37	7 36	sylan9bb	$⊢ (x \in ω \land A +_{𝑜} x = y) \to (x \in B \leftrightarrow y \in (A +_{𝑜} B))$
38	37	biimprcd	$⊢ y \in (A +_{𝑜} B) \to ((x \in ω \land A +_{𝑜} x = y) \to x \in B)$
39		eqcom	$⊢ A +_{𝑜} x = y \leftrightarrow y = A +_{𝑜} x$
40	39	bilani	$⊢ (x \in ω \land A +_{𝑜} x = y) \to y = A +_{𝑜} x$
41	38 40	jca2	$⊢ y \in (A +_{𝑜} B) \to ((x \in ω \land A +_{𝑜} x = y) \to (x \in B \land y = A +_{𝑜} x))$
42	41	reximdv2	$⊢ y \in (A +_{𝑜} B) \to (\exists x \in ω A +_{𝑜} x = y \to \exists x \in B y = A +_{𝑜} x)$
43	35 42	sylbid	$⊢ y \in (A +_{𝑜} B) \to (\neg y \in A \to \exists x \in B y = A +_{𝑜} x)$
44	43	imp	$⊢ (y \in (A +_{𝑜} B) \land \neg y \in A) \to \exists x \in B y = A +_{𝑜} x$
45	26 44	impbii	$⊢ \exists x \in B y = A +_{𝑜} x \leftrightarrow (y \in (A +_{𝑜} B) \land \neg y \in A)$
46		ovex	$⊢ A +_{𝑜} x \in V$
47	3 46	elrnmpti	$⊢ y \in ran F \leftrightarrow \exists x \in B y = A +_{𝑜} x$
48		eldif	$⊢ y \in ((A +_{𝑜} B) ∖ A) \leftrightarrow (y \in (A +_{𝑜} B) \land \neg y \in A)$
49	45 47 48	3bitr4i	$⊢ y \in ran F \leftrightarrow y \in ((A +_{𝑜} B) ∖ A)$
50	49	eqriv	$⊢ ran F = (A +_{𝑜} B) ∖ A$

Metamath Proof Explorer

Theorem unfilem1

Proof