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

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