Theorem 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	⊢ ( ω ≼ 𝐴 ↔ ω ≼ ( 𝐴 ⊔ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		reldom	⊢ Rel ≼
2	1	brrelex2i	⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
3		djudoml	⊢ ( ( 𝐴 ∈ V ∧ 𝐴 ∈ V ) → 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) )
4	2 2 3	syl2anc	⊢ ( ω ≼ 𝐴 → 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) )
5		domtr	⊢ ( ( ω ≼ 𝐴 ∧ 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) ) → ω ≼ ( 𝐴 ⊔ 𝐴 ) )
6	4 5	mpdan	⊢ ( ω ≼ 𝐴 → ω ≼ ( 𝐴 ⊔ 𝐴 ) )
7	1	brrelex2i	⊢ ( ω ≼ ( 𝐴 ⊔ 𝐴 ) → ( 𝐴 ⊔ 𝐴 ) ∈ V )
8		anidm	⊢ ( ( 𝐴 ∈ V ∧ 𝐴 ∈ V ) ↔ 𝐴 ∈ V )
9		djuexb	⊢ ( ( 𝐴 ∈ V ∧ 𝐴 ∈ V ) ↔ ( 𝐴 ⊔ 𝐴 ) ∈ V )
10	8 9	bitr3i	⊢ ( 𝐴 ∈ V ↔ ( 𝐴 ⊔ 𝐴 ) ∈ V )
11	7 10	sylibr	⊢ ( ω ≼ ( 𝐴 ⊔ 𝐴 ) → 𝐴 ∈ V )
12		domeng	⊢ ( ( 𝐴 ⊔ 𝐴 ) ∈ V → ( ω ≼ ( 𝐴 ⊔ 𝐴 ) ↔ ∃ 𝑥 ( ω ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ⊔ 𝐴 ) ) ) )
13	7 12	syl	⊢ ( ω ≼ ( 𝐴 ⊔ 𝐴 ) → ( ω ≼ ( 𝐴 ⊔ 𝐴 ) ↔ ∃ 𝑥 ( ω ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ⊔ 𝐴 ) ) ) )
14	13	ibi	⊢ ( ω ≼ ( 𝐴 ⊔ 𝐴 ) → ∃ 𝑥 ( ω ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ⊔ 𝐴 ) ) )
15		indi	⊢ ( 𝑥 ∩ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐴 ) ) ) = ( ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ∪ ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) )
16		simpr	⊢ ( ( ω ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ⊔ 𝐴 ) ) → 𝑥 ⊆ ( 𝐴 ⊔ 𝐴 ) )
17		df-dju	⊢ ( 𝐴 ⊔ 𝐴 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐴 ) )
18	16 17	sseqtrdi	⊢ ( ( ω ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ⊔ 𝐴 ) ) → 𝑥 ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐴 ) ) )
19		df-ss	⊢ ( 𝑥 ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐴 ) ) ↔ ( 𝑥 ∩ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐴 ) ) ) = 𝑥 )
20	18 19	sylib	⊢ ( ( ω ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ⊔ 𝐴 ) ) → ( 𝑥 ∩ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐴 ) ) ) = 𝑥 )
21	15 20	eqtr3id	⊢ ( ( ω ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ⊔ 𝐴 ) ) → ( ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ∪ ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ) = 𝑥 )
22		ensym	⊢ ( ω ≈ 𝑥 → 𝑥 ≈ ω )
23	22	adantr	⊢ ( ( ω ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ⊔ 𝐴 ) ) → 𝑥 ≈ ω )
24	21 23	eqbrtrd	⊢ ( ( ω ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ⊔ 𝐴 ) ) → ( ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ∪ ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ) ≈ ω )
25		cdainflem	⊢ ( ( ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ∪ ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ) ≈ ω → ( ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ≈ ω ∨ ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ≈ ω ) )
26		snex	⊢ { ∅ } ∈ V
27		xpexg	⊢ ( ( { ∅ } ∈ V ∧ 𝐴 ∈ V ) → ( { ∅ } × 𝐴 ) ∈ V )
28	26 27	mpan	⊢ ( 𝐴 ∈ V → ( { ∅ } × 𝐴 ) ∈ V )
29		inss2	⊢ ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ⊆ ( { ∅ } × 𝐴 )
30		ssdomg	⊢ ( ( { ∅ } × 𝐴 ) ∈ V → ( ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ⊆ ( { ∅ } × 𝐴 ) → ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ≼ ( { ∅ } × 𝐴 ) ) )
31	28 29 30	mpisyl	⊢ ( 𝐴 ∈ V → ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ≼ ( { ∅ } × 𝐴 ) )
32		0ex	⊢ ∅ ∈ V
33		xpsnen2g	⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ V ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
34	32 33	mpan	⊢ ( 𝐴 ∈ V → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
35		domentr	⊢ ( ( ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ≼ ( { ∅ } × 𝐴 ) ∧ ( { ∅ } × 𝐴 ) ≈ 𝐴 ) → ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ≼ 𝐴 )
36	31 34 35	syl2anc	⊢ ( 𝐴 ∈ V → ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ≼ 𝐴 )
37		domen1	⊢ ( ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ≈ ω → ( ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ≼ 𝐴 ↔ ω ≼ 𝐴 ) )
38	36 37	syl5ibcom	⊢ ( 𝐴 ∈ V → ( ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ≈ ω → ω ≼ 𝐴 ) )
39		snex	⊢ { 1o } ∈ V
40		xpexg	⊢ ( ( { 1o } ∈ V ∧ 𝐴 ∈ V ) → ( { 1o } × 𝐴 ) ∈ V )
41	39 40	mpan	⊢ ( 𝐴 ∈ V → ( { 1o } × 𝐴 ) ∈ V )
42		inss2	⊢ ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ⊆ ( { 1o } × 𝐴 )
43		ssdomg	⊢ ( ( { 1o } × 𝐴 ) ∈ V → ( ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ⊆ ( { 1o } × 𝐴 ) → ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ≼ ( { 1o } × 𝐴 ) ) )
44	41 42 43	mpisyl	⊢ ( 𝐴 ∈ V → ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ≼ ( { 1o } × 𝐴 ) )
45		1on	⊢ 1o ∈ On
46		xpsnen2g	⊢ ( ( 1o ∈ On ∧ 𝐴 ∈ V ) → ( { 1o } × 𝐴 ) ≈ 𝐴 )
47	45 46	mpan	⊢ ( 𝐴 ∈ V → ( { 1o } × 𝐴 ) ≈ 𝐴 )
48		domentr	⊢ ( ( ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ≼ ( { 1o } × 𝐴 ) ∧ ( { 1o } × 𝐴 ) ≈ 𝐴 ) → ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ≼ 𝐴 )
49	44 47 48	syl2anc	⊢ ( 𝐴 ∈ V → ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ≼ 𝐴 )
50		domen1	⊢ ( ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ≈ ω → ( ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ≼ 𝐴 ↔ ω ≼ 𝐴 ) )
51	49 50	syl5ibcom	⊢ ( 𝐴 ∈ V → ( ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ≈ ω → ω ≼ 𝐴 ) )
52	38 51	jaod	⊢ ( 𝐴 ∈ V → ( ( ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ≈ ω ∨ ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ≈ ω ) → ω ≼ 𝐴 ) )
53	25 52	syl5	⊢ ( 𝐴 ∈ V → ( ( ( 𝑥 ∩ ( { ∅ } × 𝐴 ) ) ∪ ( 𝑥 ∩ ( { 1o } × 𝐴 ) ) ) ≈ ω → ω ≼ 𝐴 ) )
54	24 53	syl5	⊢ ( 𝐴 ∈ V → ( ( ω ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ⊔ 𝐴 ) ) → ω ≼ 𝐴 ) )
55	54	exlimdv	⊢ ( 𝐴 ∈ V → ( ∃ 𝑥 ( ω ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐴 ⊔ 𝐴 ) ) → ω ≼ 𝐴 ) )
56	11 14 55	sylc	⊢ ( ω ≼ ( 𝐴 ⊔ 𝐴 ) → ω ≼ 𝐴 )
57	6 56	impbii	⊢ ( ω ≼ 𝐴 ↔ ω ≼ ( 𝐴 ⊔ 𝐴 ) )