pwxpndom2

Description: The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015) (Proof shortened by AV, 18-Jul-2022)

		Ref	Expression
	Assertion	pwxpndom2	$⊢ ω ≼ A \to \neg 𝒫 A ≼ (A ⊔︀ (A \times A))$

Proof

Step	Hyp	Ref	Expression
1		pwfseq	$⊢ ω ≼ A \to \neg 𝒫 A ≼ ⋃_{n \in ω} (A^{n})$
2		reldom	$⊢ Rel ≼$
3	2	brrelex2i	$⊢ ω ≼ A \to A \in V$
4		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
5	4	oveq2i	$⊢ A^{1_{𝑜}} = A^{\{\emptyset\}}$
6		id	$⊢ A \in V \to A \in V$
7		0ex	$⊢ \emptyset \in V$
8	7	a1i	$⊢ A \in V \to \emptyset \in V$
9	6 8	mapsnend	$⊢ A \in V \to (A^{\{\emptyset\}}) \approx A$
10	5 9	eqbrtrid	$⊢ A \in V \to (A^{1_{𝑜}}) \approx A$
11		ensym	$⊢ (A^{1_{𝑜}}) \approx A \to A \approx (A^{1_{𝑜}})$
12	3 10 11	3syl	$⊢ ω ≼ A \to A \approx (A^{1_{𝑜}})$
13		map2xp	$⊢ A \in V \to (A^{2_{𝑜}}) \approx (A \times A)$
14		ensym	$⊢ (A^{2_{𝑜}}) \approx (A \times A) \to (A \times A) \approx (A^{2_{𝑜}})$
15	3 13 14	3syl	$⊢ ω ≼ A \to (A \times A) \approx (A^{2_{𝑜}})$
16		elmapi	$⊢ x \in (A^{1_{𝑜}}) \to x : 1_{𝑜} ⟶ A$
17	16	fdmd	$⊢ x \in (A^{1_{𝑜}}) \to dom x = 1_{𝑜}$
18	17	adantr	$⊢ (x \in (A^{1_{𝑜}}) \land x \in (A^{2_{𝑜}})) \to dom x = 1_{𝑜}$
19		1oex	$⊢ 1_{𝑜} \in V$
20	19	sucid	$⊢ 1_{𝑜} \in suc 1_{𝑜}$
21		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
22	20 21	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
23		1on	$⊢ 1_{𝑜} \in On$
24	23	onirri	$⊢ \neg 1_{𝑜} \in 1_{𝑜}$
25		nelneq2	$⊢ (1_{𝑜} \in 2_{𝑜} \land \neg 1_{𝑜} \in 1_{𝑜}) \to \neg 2_{𝑜} = 1_{𝑜}$
26	22 24 25	mp2an	$⊢ \neg 2_{𝑜} = 1_{𝑜}$
27		elmapi	$⊢ x \in (A^{2_{𝑜}}) \to x : 2_{𝑜} ⟶ A$
28	27	fdmd	$⊢ x \in (A^{2_{𝑜}}) \to dom x = 2_{𝑜}$
29	28	adantl	$⊢ (x \in (A^{1_{𝑜}}) \land x \in (A^{2_{𝑜}})) \to dom x = 2_{𝑜}$
30	29	eqeq1d	$⊢ (x \in (A^{1_{𝑜}}) \land x \in (A^{2_{𝑜}})) \to (dom x = 1_{𝑜} \leftrightarrow 2_{𝑜} = 1_{𝑜})$
31	26 30	mtbiri	$⊢ (x \in (A^{1_{𝑜}}) \land x \in (A^{2_{𝑜}})) \to \neg dom x = 1_{𝑜}$
32	18 31	pm2.65i	$⊢ \neg (x \in (A^{1_{𝑜}}) \land x \in (A^{2_{𝑜}}))$
33		elin	$⊢ x \in ((A^{1_{𝑜}}) \cap (A^{2_{𝑜}})) \leftrightarrow (x \in (A^{1_{𝑜}}) \land x \in (A^{2_{𝑜}}))$
34	32 33	mtbir	$⊢ \neg x \in ((A^{1_{𝑜}}) \cap (A^{2_{𝑜}}))$
35	34	a1i	$⊢ ω ≼ A \to \neg x \in ((A^{1_{𝑜}}) \cap (A^{2_{𝑜}}))$
36	35	eq0rdv	$⊢ ω ≼ A \to (A^{1_{𝑜}}) \cap (A^{2_{𝑜}}) = \emptyset$
37		djuenun	$⊢ (A \approx (A^{1_{𝑜}}) \land (A \times A) \approx (A^{2_{𝑜}}) \land (A^{1_{𝑜}}) \cap (A^{2_{𝑜}}) = \emptyset) \to (A ⊔︀ (A \times A)) \approx ((A^{1_{𝑜}}) \cup (A^{2_{𝑜}}))$
38	12 15 36 37	syl3anc	$⊢ ω ≼ A \to (A ⊔︀ (A \times A)) \approx ((A^{1_{𝑜}}) \cup (A^{2_{𝑜}}))$
39		omex	$⊢ ω \in V$
40		ovex	$⊢ A^{n} \in V$
41	39 40	iunex	$⊢ ⋃_{n \in ω} (A^{n}) \in V$
42		1onn	$⊢ 1_{𝑜} \in ω$
43		oveq2	$⊢ n = 1_{𝑜} \to A^{n} = A^{1_{𝑜}}$
44	43	ssiun2s	$⊢ 1_{𝑜} \in ω \to A^{1_{𝑜}} \subseteq ⋃_{n \in ω} (A^{n})$
45	42 44	ax-mp	$⊢ A^{1_{𝑜}} \subseteq ⋃_{n \in ω} (A^{n})$
46		2onn	$⊢ 2_{𝑜} \in ω$
47		oveq2	$⊢ n = 2_{𝑜} \to A^{n} = A^{2_{𝑜}}$
48	47	ssiun2s	$⊢ 2_{𝑜} \in ω \to A^{2_{𝑜}} \subseteq ⋃_{n \in ω} (A^{n})$
49	46 48	ax-mp	$⊢ A^{2_{𝑜}} \subseteq ⋃_{n \in ω} (A^{n})$
50	45 49	unssi	$⊢ (A^{1_{𝑜}}) \cup (A^{2_{𝑜}}) \subseteq ⋃_{n \in ω} (A^{n})$
51		ssdomg	$⊢ ⋃_{n \in ω} (A^{n}) \in V \to ((A^{1_{𝑜}}) \cup (A^{2_{𝑜}}) \subseteq ⋃_{n \in ω} (A^{n}) \to ((A^{1_{𝑜}}) \cup (A^{2_{𝑜}})) ≼ ⋃_{n \in ω} (A^{n}))$
52	41 50 51	mp2	$⊢ ((A^{1_{𝑜}}) \cup (A^{2_{𝑜}})) ≼ ⋃_{n \in ω} (A^{n})$
53		endomtr	$⊢ ((A ⊔︀ (A \times A)) \approx ((A^{1_{𝑜}}) \cup (A^{2_{𝑜}})) \land ((A^{1_{𝑜}}) \cup (A^{2_{𝑜}})) ≼ ⋃_{n \in ω} (A^{n})) \to (A ⊔︀ (A \times A)) ≼ ⋃_{n \in ω} (A^{n})$
54	38 52 53	sylancl	$⊢ ω ≼ A \to (A ⊔︀ (A \times A)) ≼ ⋃_{n \in ω} (A^{n})$
55		domtr	$⊢ (𝒫 A ≼ (A ⊔︀ (A \times A)) \land (A ⊔︀ (A \times A)) ≼ ⋃_{n \in ω} (A^{n})) \to 𝒫 A ≼ ⋃_{n \in ω} (A^{n})$
56	55	expcom	$⊢ (A ⊔︀ (A \times A)) ≼ ⋃_{n \in ω} (A^{n}) \to (𝒫 A ≼ (A ⊔︀ (A \times A)) \to 𝒫 A ≼ ⋃_{n \in ω} (A^{n}))$
57	54 56	syl	$⊢ ω ≼ A \to (𝒫 A ≼ (A ⊔︀ (A \times A)) \to 𝒫 A ≼ ⋃_{n \in ω} (A^{n}))$
58	1 57	mtod	$⊢ ω ≼ A \to \neg 𝒫 A ≼ (A ⊔︀ (A \times A))$

Metamath Proof Explorer

Theorem pwxpndom2

Proof