djuinf

Description: A set is infinite iff the cardinal sum with itself is infinite. (Contributed by NM, 22-Oct-2004) (Revised by Mario Carneiro, 29-Apr-2015)

		Ref	Expression
	Assertion	djuinf	$⊢ ω ≼ A \leftrightarrow ω ≼ (A ⊔︀ A)$

Proof

Step	Hyp	Ref	Expression
1		reldom	$⊢ Rel ≼$
2	1	brrelex2i	$⊢ ω ≼ A \to A \in V$
3		djudoml	$⊢ (A \in V \land A \in V) \to A ≼ (A ⊔︀ A)$
4	2 2 3	syl2anc	$⊢ ω ≼ A \to A ≼ (A ⊔︀ A)$
5		domtr	$⊢ (ω ≼ A \land A ≼ (A ⊔︀ A)) \to ω ≼ (A ⊔︀ A)$
6	4 5	mpdan	$⊢ ω ≼ A \to ω ≼ (A ⊔︀ A)$
7	1	brrelex2i	$⊢ ω ≼ (A ⊔︀ A) \to (A ⊔︀ A) \in V$
8		anidm	$⊢ (A \in V \land A \in V) \leftrightarrow A \in V$
9		djuexb	$⊢ (A \in V \land A \in V) \leftrightarrow (A ⊔︀ A) \in V$
10	8 9	bitr3i	$⊢ A \in V \leftrightarrow (A ⊔︀ A) \in V$
11	7 10	sylibr	$⊢ ω ≼ (A ⊔︀ A) \to A \in V$
12		domeng	$⊢ (A ⊔︀ A) \in V \to (ω ≼ (A ⊔︀ A) \leftrightarrow \exists x (ω \approx x \land x \subseteq (A ⊔︀ A)))$
13	7 12	syl	$⊢ ω ≼ (A ⊔︀ A) \to (ω ≼ (A ⊔︀ A) \leftrightarrow \exists x (ω \approx x \land x \subseteq (A ⊔︀ A)))$
14	13	ibi	$⊢ ω ≼ (A ⊔︀ A) \to \exists x (ω \approx x \land x \subseteq (A ⊔︀ A))$
15		indi	$⊢ x \cap ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times A)) = (x \cap (\{\emptyset\} \times A)) \cup (x \cap (\{1_{𝑜}\} \times A))$
16		simpr	$⊢ (ω \approx x \land x \subseteq (A ⊔︀ A)) \to x \subseteq (A ⊔︀ A)$
17		df-dju	$⊢ (A ⊔︀ A) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times A)$
18	16 17	sseqtrdi	$⊢ (ω \approx x \land x \subseteq (A ⊔︀ A)) \to x \subseteq (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times A)$
19		dfss2	$⊢ x \subseteq (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times A) \leftrightarrow x \cap ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times A)) = x$
20	18 19	sylib	$⊢ (ω \approx x \land x \subseteq (A ⊔︀ A)) \to x \cap ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times A)) = x$
21	15 20	eqtr3id	$⊢ (ω \approx x \land x \subseteq (A ⊔︀ A)) \to (x \cap (\{\emptyset\} \times A)) \cup (x \cap (\{1_{𝑜}\} \times A)) = x$
22		ensym	$⊢ ω \approx x \to x \approx ω$
23	22	adantr	$⊢ (ω \approx x \land x \subseteq (A ⊔︀ A)) \to x \approx ω$
24	21 23	eqbrtrd	$⊢ (ω \approx x \land x \subseteq (A ⊔︀ A)) \to ((x \cap (\{\emptyset\} \times A)) \cup (x \cap (\{1_{𝑜}\} \times A))) \approx ω$
25		cdainflem	$⊢ ((x \cap (\{\emptyset\} \times A)) \cup (x \cap (\{1_{𝑜}\} \times A))) \approx ω \to ((x \cap (\{\emptyset\} \times A)) \approx ω \lor (x \cap (\{1_{𝑜}\} \times A)) \approx ω)$
26		snex	$⊢ \{\emptyset\} \in V$
27		xpexg	$⊢ (\{\emptyset\} \in V \land A \in V) \to \{\emptyset\} \times A \in V$
28	26 27	mpan	$⊢ A \in V \to \{\emptyset\} \times A \in V$
29		inss2	$⊢ x \cap (\{\emptyset\} \times A) \subseteq \{\emptyset\} \times A$
30		ssdomg	$⊢ \{\emptyset\} \times A \in V \to (x \cap (\{\emptyset\} \times A) \subseteq \{\emptyset\} \times A \to (x \cap (\{\emptyset\} \times A)) ≼ (\{\emptyset\} \times A))$
31	28 29 30	mpisyl	$⊢ A \in V \to (x \cap (\{\emptyset\} \times A)) ≼ (\{\emptyset\} \times A)$
32		0ex	$⊢ \emptyset \in V$
33		xpsnen2g	$⊢ (\emptyset \in V \land A \in V) \to (\{\emptyset\} \times A) \approx A$
34	32 33	mpan	$⊢ A \in V \to (\{\emptyset\} \times A) \approx A$
35		domentr	$⊢ ((x \cap (\{\emptyset\} \times A)) ≼ (\{\emptyset\} \times A) \land (\{\emptyset\} \times A) \approx A) \to (x \cap (\{\emptyset\} \times A)) ≼ A$
36	31 34 35	syl2anc	$⊢ A \in V \to (x \cap (\{\emptyset\} \times A)) ≼ A$
37		domen1	$⊢ (x \cap (\{\emptyset\} \times A)) \approx ω \to ((x \cap (\{\emptyset\} \times A)) ≼ A \leftrightarrow ω ≼ A)$
38	36 37	syl5ibcom	$⊢ A \in V \to ((x \cap (\{\emptyset\} \times A)) \approx ω \to ω ≼ A)$
39		snex	$⊢ \{1_{𝑜}\} \in V$
40		xpexg	$⊢ (\{1_{𝑜}\} \in V \land A \in V) \to \{1_{𝑜}\} \times A \in V$
41	39 40	mpan	$⊢ A \in V \to \{1_{𝑜}\} \times A \in V$
42		inss2	$⊢ x \cap (\{1_{𝑜}\} \times A) \subseteq \{1_{𝑜}\} \times A$
43		ssdomg	$⊢ \{1_{𝑜}\} \times A \in V \to (x \cap (\{1_{𝑜}\} \times A) \subseteq \{1_{𝑜}\} \times A \to (x \cap (\{1_{𝑜}\} \times A)) ≼ (\{1_{𝑜}\} \times A))$
44	41 42 43	mpisyl	$⊢ A \in V \to (x \cap (\{1_{𝑜}\} \times A)) ≼ (\{1_{𝑜}\} \times A)$
45		1on	$⊢ 1_{𝑜} \in On$
46		xpsnen2g	$⊢ (1_{𝑜} \in On \land A \in V) \to (\{1_{𝑜}\} \times A) \approx A$
47	45 46	mpan	$⊢ A \in V \to (\{1_{𝑜}\} \times A) \approx A$
48		domentr	$⊢ ((x \cap (\{1_{𝑜}\} \times A)) ≼ (\{1_{𝑜}\} \times A) \land (\{1_{𝑜}\} \times A) \approx A) \to (x \cap (\{1_{𝑜}\} \times A)) ≼ A$
49	44 47 48	syl2anc	$⊢ A \in V \to (x \cap (\{1_{𝑜}\} \times A)) ≼ A$
50		domen1	$⊢ (x \cap (\{1_{𝑜}\} \times A)) \approx ω \to ((x \cap (\{1_{𝑜}\} \times A)) ≼ A \leftrightarrow ω ≼ A)$
51	49 50	syl5ibcom	$⊢ A \in V \to ((x \cap (\{1_{𝑜}\} \times A)) \approx ω \to ω ≼ A)$
52	38 51	jaod	$⊢ A \in V \to (((x \cap (\{\emptyset\} \times A)) \approx ω \lor (x \cap (\{1_{𝑜}\} \times A)) \approx ω) \to ω ≼ A)$
53	25 52	syl5	$⊢ A \in V \to (((x \cap (\{\emptyset\} \times A)) \cup (x \cap (\{1_{𝑜}\} \times A))) \approx ω \to ω ≼ A)$
54	24 53	syl5	$⊢ A \in V \to ((ω \approx x \land x \subseteq (A ⊔︀ A)) \to ω ≼ A)$
55	54	exlimdv	$⊢ A \in V \to (\exists x (ω \approx x \land x \subseteq (A ⊔︀ A)) \to ω ≼ A)$
56	11 14 55	sylc	$⊢ ω ≼ (A ⊔︀ A) \to ω ≼ A$
57	6 56	impbii	$⊢ ω ≼ A \leftrightarrow ω ≼ (A ⊔︀ A)$

Metamath Proof Explorer

Theorem djuinf

Proof