Theorem 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	⊢ ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pwfseq	⊢ ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
2		reldom	⊢ Rel ≼
3	2	brrelex2i	⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
4		df1o2	⊢ 1o = { ∅ }
5	4	oveq2i	⊢ ( 𝐴 ↑m 1o ) = ( 𝐴 ↑m { ∅ } )
6		id	⊢ ( 𝐴 ∈ V → 𝐴 ∈ V )
7		0ex	⊢ ∅ ∈ V
8	7	a1i	⊢ ( 𝐴 ∈ V → ∅ ∈ V )
9	6 8	mapsnend	⊢ ( 𝐴 ∈ V → ( 𝐴 ↑m { ∅ } ) ≈ 𝐴 )
10	5 9	eqbrtrid	⊢ ( 𝐴 ∈ V → ( 𝐴 ↑m 1o ) ≈ 𝐴 )
11		ensym	⊢ ( ( 𝐴 ↑m 1o ) ≈ 𝐴 → 𝐴 ≈ ( 𝐴 ↑m 1o ) )
12	3 10 11	3syl	⊢ ( ω ≼ 𝐴 → 𝐴 ≈ ( 𝐴 ↑m 1o ) )
13		map2xp	⊢ ( 𝐴 ∈ V → ( 𝐴 ↑m 2o ) ≈ ( 𝐴 × 𝐴 ) )
14		ensym	⊢ ( ( 𝐴 ↑m 2o ) ≈ ( 𝐴 × 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ ( 𝐴 ↑m 2o ) )
15	3 13 14	3syl	⊢ ( ω ≼ 𝐴 → ( 𝐴 × 𝐴 ) ≈ ( 𝐴 ↑m 2o ) )
16		elmapi	⊢ ( 𝑥 ∈ ( 𝐴 ↑m 1o ) → 𝑥 : 1o ⟶ 𝐴 )
17	16	fdmd	⊢ ( 𝑥 ∈ ( 𝐴 ↑m 1o ) → dom 𝑥 = 1o )
18	17	adantr	⊢ ( ( 𝑥 ∈ ( 𝐴 ↑m 1o ) ∧ 𝑥 ∈ ( 𝐴 ↑m 2o ) ) → dom 𝑥 = 1o )
19		1oex	⊢ 1o ∈ V
20	19	sucid	⊢ 1o ∈ suc 1o
21		df-2o	⊢ 2o = suc 1o
22	20 21	eleqtrri	⊢ 1o ∈ 2o
23		1on	⊢ 1o ∈ On
24	23	onirri	⊢ ¬ 1o ∈ 1o
25		nelneq2	⊢ ( ( 1o ∈ 2o ∧ ¬ 1o ∈ 1o ) → ¬ 2o = 1o )
26	22 24 25	mp2an	⊢ ¬ 2o = 1o
27		elmapi	⊢ ( 𝑥 ∈ ( 𝐴 ↑m 2o ) → 𝑥 : 2o ⟶ 𝐴 )
28	27	fdmd	⊢ ( 𝑥 ∈ ( 𝐴 ↑m 2o ) → dom 𝑥 = 2o )
29	28	adantl	⊢ ( ( 𝑥 ∈ ( 𝐴 ↑m 1o ) ∧ 𝑥 ∈ ( 𝐴 ↑m 2o ) ) → dom 𝑥 = 2o )
30	29	eqeq1d	⊢ ( ( 𝑥 ∈ ( 𝐴 ↑m 1o ) ∧ 𝑥 ∈ ( 𝐴 ↑m 2o ) ) → ( dom 𝑥 = 1o ↔ 2o = 1o ) )
31	26 30	mtbiri	⊢ ( ( 𝑥 ∈ ( 𝐴 ↑m 1o ) ∧ 𝑥 ∈ ( 𝐴 ↑m 2o ) ) → ¬ dom 𝑥 = 1o )
32	18 31	pm2.65i	⊢ ¬ ( 𝑥 ∈ ( 𝐴 ↑m 1o ) ∧ 𝑥 ∈ ( 𝐴 ↑m 2o ) )
33		elin	⊢ ( 𝑥 ∈ ( ( 𝐴 ↑m 1o ) ∩ ( 𝐴 ↑m 2o ) ) ↔ ( 𝑥 ∈ ( 𝐴 ↑m 1o ) ∧ 𝑥 ∈ ( 𝐴 ↑m 2o ) ) )
34	32 33	mtbir	⊢ ¬ 𝑥 ∈ ( ( 𝐴 ↑m 1o ) ∩ ( 𝐴 ↑m 2o ) )
35	34	a1i	⊢ ( ω ≼ 𝐴 → ¬ 𝑥 ∈ ( ( 𝐴 ↑m 1o ) ∩ ( 𝐴 ↑m 2o ) ) )
36	35	eq0rdv	⊢ ( ω ≼ 𝐴 → ( ( 𝐴 ↑m 1o ) ∩ ( 𝐴 ↑m 2o ) ) = ∅ )
37		djuenun	⊢ ( ( 𝐴 ≈ ( 𝐴 ↑m 1o ) ∧ ( 𝐴 × 𝐴 ) ≈ ( 𝐴 ↑m 2o ) ∧ ( ( 𝐴 ↑m 1o ) ∩ ( 𝐴 ↑m 2o ) ) = ∅ ) → ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ≈ ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) )
38	12 15 36 37	syl3anc	⊢ ( ω ≼ 𝐴 → ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ≈ ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) )
39		omex	⊢ ω ∈ V
40		ovex	⊢ ( 𝐴 ↑m 𝑛 ) ∈ V
41	39 40	iunex	⊢ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∈ V
42		1onn	⊢ 1o ∈ ω
43		oveq2	⊢ ( 𝑛 = 1o → ( 𝐴 ↑m 𝑛 ) = ( 𝐴 ↑m 1o ) )
44	43	ssiun2s	⊢ ( 1o ∈ ω → ( 𝐴 ↑m 1o ) ⊆ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
45	42 44	ax-mp	⊢ ( 𝐴 ↑m 1o ) ⊆ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 )
46		2onn	⊢ 2o ∈ ω
47		oveq2	⊢ ( 𝑛 = 2o → ( 𝐴 ↑m 𝑛 ) = ( 𝐴 ↑m 2o ) )
48	47	ssiun2s	⊢ ( 2o ∈ ω → ( 𝐴 ↑m 2o ) ⊆ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
49	46 48	ax-mp	⊢ ( 𝐴 ↑m 2o ) ⊆ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 )
50	45 49	unssi	⊢ ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) ⊆ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 )
51		ssdomg	⊢ ( ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∈ V → ( ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) ⊆ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) → ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
52	41 50 51	mp2	⊢ ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 )
53		endomtr	⊢ ( ( ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ≈ ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) ∧ ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
54	38 52 53	sylancl	⊢ ( ω ≼ 𝐴 → ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
55		domtr	⊢ ( ( 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ∧ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
56	55	expcom	⊢ ( ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) → ( 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) → 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
57	54 56	syl	⊢ ( ω ≼ 𝐴 → ( 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) → 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
58	1 57	mtod	⊢ ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )