This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 dfss2 ⊢ ( 𝑥 ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 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 ⊢ ( ω ≼ 𝐴 ↔ ω ≼ ( 𝐴 ⊔ 𝐴 ) )