Metamath Proof Explorer


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 ω A ω A ⊔︀ A

Proof

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