Metamath Proof Explorer

Theorem infdifsn

Description: Removing a singleton from an infinite set does not change the cardinality of the set. (Contributed by Mario Carneiro, 30-Apr-2015) (Revised by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion infdifsn ⊢ ω ≼ A → A ∖ B ≈ A

Proof

Step Hyp Ref Expression
1 brdomi ⊢ ω ≼ A → ∃ f f : ω ⟶ 1-1 A
2 1 adantr ⊢ ω ≼ A ∧ B ∈ A → ∃ f f : ω ⟶ 1-1 A
3 reldom ⊢ Rel ⁡ ≼
4 3 brrelex2i ⊢ ω ≼ A → A ∈ V
5 4 ad2antrr ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → A ∈ V
6 simplr ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → B ∈ A
7 f1f ⊢ f : ω ⟶ 1-1 A → f : ω ⟶ A
8 7 adantl ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → f : ω ⟶ A
9 peano1 ⊢ ∅ ∈ ω
10 ffvelrn ⊢ f : ω ⟶ A ∧ ∅ ∈ ω → f ⁡ ∅ ∈ A
11 8 9 10 sylancl ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → f ⁡ ∅ ∈ A
12 difsnen ⊢ A ∈ V ∧ B ∈ A ∧ f ⁡ ∅ ∈ A → A ∖ B ≈ A ∖ f ⁡ ∅
13 5 6 11 12 syl3anc ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → A ∖ B ≈ A ∖ f ⁡ ∅
14 vex ⊢ f ∈ V
15 f1f1orn ⊢ f : ω ⟶ 1-1 A → f : ω ⟶ 1-1 onto ran ⁡ f
16 15 adantl ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → f : ω ⟶ 1-1 onto ran ⁡ f
17 f1oen3g ⊢ f ∈ V ∧ f : ω ⟶ 1-1 onto ran ⁡ f → ω ≈ ran ⁡ f
18 14 16 17 sylancr ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → ω ≈ ran ⁡ f
19 18 ensymd ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → ran ⁡ f ≈ ω
20 3 brrelex1i ⊢ ω ≼ A → ω ∈ V
21 20 ad2antrr ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → ω ∈ V
22 limom ⊢ Lim ⁡ ω
23 22 limenpsi ⊢ ω ∈ V → ω ≈ ω ∖ ∅
24 21 23 syl ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → ω ≈ ω ∖ ∅
25 14 resex ⊢ f ↾ ω ∖ ∅ ∈ V
26 simpr ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → f : ω ⟶ 1-1 A
27 difss ⊢ ω ∖ ∅ ⊆ ω
28 f1ores ⊢ f : ω ⟶ 1-1 A ∧ ω ∖ ∅ ⊆ ω → f ↾ ω ∖ ∅ : ω ∖ ∅ ⟶ 1-1 onto f ω ∖ ∅
29 26 27 28 sylancl ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → f ↾ ω ∖ ∅ : ω ∖ ∅ ⟶ 1-1 onto f ω ∖ ∅
30 f1oen3g ⊢ f ↾ ω ∖ ∅ ∈ V ∧ f ↾ ω ∖ ∅ : ω ∖ ∅ ⟶ 1-1 onto f ω ∖ ∅ → ω ∖ ∅ ≈ f ω ∖ ∅
31 25 29 30 sylancr ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → ω ∖ ∅ ≈ f ω ∖ ∅
32 f1orn ⊢ f : ω ⟶ 1-1 onto ran ⁡ f ↔ f Fn ω ∧ Fun ⁡ f -1
33 32 simprbi ⊢ f : ω ⟶ 1-1 onto ran ⁡ f → Fun ⁡ f -1
34 imadif ⊢ Fun ⁡ f -1 → f ω ∖ ∅ = f ω ∖ f ∅
35 16 33 34 3syl ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → f ω ∖ ∅ = f ω ∖ f ∅
36 f1fn ⊢ f : ω ⟶ 1-1 A → f Fn ω
37 36 adantl ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → f Fn ω
38 fnima ⊢ f Fn ω → f ω = ran ⁡ f
39 37 38 syl ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → f ω = ran ⁡ f
40 fnsnfv ⊢ f Fn ω ∧ ∅ ∈ ω → f ⁡ ∅ = f ∅
41 37 9 40 sylancl ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → f ⁡ ∅ = f ∅
42 41 eqcomd ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → f ∅ = f ⁡ ∅
43 39 42 difeq12d ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → f ω ∖ f ∅ = ran ⁡ f ∖ f ⁡ ∅
44 35 43 eqtrd ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → f ω ∖ ∅ = ran ⁡ f ∖ f ⁡ ∅
45 31 44 breqtrd ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → ω ∖ ∅ ≈ ran ⁡ f ∖ f ⁡ ∅
46 entr ⊢ ω ≈ ω ∖ ∅ ∧ ω ∖ ∅ ≈ ran ⁡ f ∖ f ⁡ ∅ → ω ≈ ran ⁡ f ∖ f ⁡ ∅
47 24 45 46 syl2anc ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → ω ≈ ran ⁡ f ∖ f ⁡ ∅
48 entr ⊢ ran ⁡ f ≈ ω ∧ ω ≈ ran ⁡ f ∖ f ⁡ ∅ → ran ⁡ f ≈ ran ⁡ f ∖ f ⁡ ∅
49 19 47 48 syl2anc ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → ran ⁡ f ≈ ran ⁡ f ∖ f ⁡ ∅
50 difexg ⊢ A ∈ V → A ∖ ran ⁡ f ∈ V
51 enrefg ⊢ A ∖ ran ⁡ f ∈ V → A ∖ ran ⁡ f ≈ A ∖ ran ⁡ f
52 5 50 51 3syl ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → A ∖ ran ⁡ f ≈ A ∖ ran ⁡ f
53 disjdif ⊢ ran ⁡ f ∩ A ∖ ran ⁡ f = ∅
54 53 a1i ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → ran ⁡ f ∩ A ∖ ran ⁡ f = ∅
55 difss ⊢ ran ⁡ f ∖ f ⁡ ∅ ⊆ ran ⁡ f
56 ssrin ⊢ ran ⁡ f ∖ f ⁡ ∅ ⊆ ran ⁡ f → ran ⁡ f ∖ f ⁡ ∅ ∩ A ∖ ran ⁡ f ⊆ ran ⁡ f ∩ A ∖ ran ⁡ f
57 55 56 ax-mp ⊢ ran ⁡ f ∖ f ⁡ ∅ ∩ A ∖ ran ⁡ f ⊆ ran ⁡ f ∩ A ∖ ran ⁡ f
58 sseq0 ⊢ ran ⁡ f ∖ f ⁡ ∅ ∩ A ∖ ran ⁡ f ⊆ ran ⁡ f ∩ A ∖ ran ⁡ f ∧ ran ⁡ f ∩ A ∖ ran ⁡ f = ∅ → ran ⁡ f ∖ f ⁡ ∅ ∩ A ∖ ran ⁡ f = ∅
59 57 53 58 mp2an ⊢ ran ⁡ f ∖ f ⁡ ∅ ∩ A ∖ ran ⁡ f = ∅
60 59 a1i ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → ran ⁡ f ∖ f ⁡ ∅ ∩ A ∖ ran ⁡ f = ∅
61 unen ⊢ ran ⁡ f ≈ ran ⁡ f ∖ f ⁡ ∅ ∧ A ∖ ran ⁡ f ≈ A ∖ ran ⁡ f ∧ ran ⁡ f ∩ A ∖ ran ⁡ f = ∅ ∧ ran ⁡ f ∖ f ⁡ ∅ ∩ A ∖ ran ⁡ f = ∅ → ran ⁡ f ∪ A ∖ ran ⁡ f ≈ ran ⁡ f ∖ f ⁡ ∅ ∪ A ∖ ran ⁡ f
62 49 52 54 60 61 syl22anc ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → ran ⁡ f ∪ A ∖ ran ⁡ f ≈ ran ⁡ f ∖ f ⁡ ∅ ∪ A ∖ ran ⁡ f
63 8 frnd ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → ran ⁡ f ⊆ A
64 undif ⊢ ran ⁡ f ⊆ A ↔ ran ⁡ f ∪ A ∖ ran ⁡ f = A
65 63 64 sylib ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → ran ⁡ f ∪ A ∖ ran ⁡ f = A
66 uncom ⊢ ran ⁡ f ∖ f ⁡ ∅ ∪ A ∖ ran ⁡ f = A ∖ ran ⁡ f ∪ ran ⁡ f ∖ f ⁡ ∅
67 eldifn ⊢ f ⁡ ∅ ∈ A ∖ ran ⁡ f → ¬ f ⁡ ∅ ∈ ran ⁡ f
68 fnfvelrn ⊢ f Fn ω ∧ ∅ ∈ ω → f ⁡ ∅ ∈ ran ⁡ f
69 37 9 68 sylancl ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → f ⁡ ∅ ∈ ran ⁡ f
70 67 69 nsyl3 ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → ¬ f ⁡ ∅ ∈ A ∖ ran ⁡ f
71 disjsn ⊢ A ∖ ran ⁡ f ∩ f ⁡ ∅ = ∅ ↔ ¬ f ⁡ ∅ ∈ A ∖ ran ⁡ f
72 70 71 sylibr ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → A ∖ ran ⁡ f ∩ f ⁡ ∅ = ∅
73 undif4 ⊢ A ∖ ran ⁡ f ∩ f ⁡ ∅ = ∅ → A ∖ ran ⁡ f ∪ ran ⁡ f ∖ f ⁡ ∅ = A ∖ ran ⁡ f ∪ ran ⁡ f ∖ f ⁡ ∅
74 72 73 syl ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → A ∖ ran ⁡ f ∪ ran ⁡ f ∖ f ⁡ ∅ = A ∖ ran ⁡ f ∪ ran ⁡ f ∖ f ⁡ ∅
75 uncom ⊢ A ∖ ran ⁡ f ∪ ran ⁡ f = ran ⁡ f ∪ A ∖ ran ⁡ f
76 75 65 syl5eq ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → A ∖ ran ⁡ f ∪ ran ⁡ f = A
77 76 difeq1d ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → A ∖ ran ⁡ f ∪ ran ⁡ f ∖ f ⁡ ∅ = A ∖ f ⁡ ∅
78 74 77 eqtrd ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → A ∖ ran ⁡ f ∪ ran ⁡ f ∖ f ⁡ ∅ = A ∖ f ⁡ ∅
79 66 78 syl5eq ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → ran ⁡ f ∖ f ⁡ ∅ ∪ A ∖ ran ⁡ f = A ∖ f ⁡ ∅
80 62 65 79 3brtr3d ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → A ≈ A ∖ f ⁡ ∅
81 80 ensymd ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → A ∖ f ⁡ ∅ ≈ A
82 entr ⊢ A ∖ B ≈ A ∖ f ⁡ ∅ ∧ A ∖ f ⁡ ∅ ≈ A → A ∖ B ≈ A
83 13 81 82 syl2anc ⊢ ω ≼ A ∧ B ∈ A ∧ f : ω ⟶ 1-1 A → A ∖ B ≈ A
84 2 83 exlimddv ⊢ ω ≼ A ∧ B ∈ A → A ∖ B ≈ A
85 difsn ⊢ ¬ B ∈ A → A ∖ B = A
86 85 adantl ⊢ ω ≼ A ∧ ¬ B ∈ A → A ∖ B = A
87 enrefg ⊢ A ∈ V → A ≈ A
88 4 87 syl ⊢ ω ≼ A → A ≈ A
89 88 adantr ⊢ ω ≼ A ∧ ¬ B ∈ A → A ≈ A
90 86 89 eqbrtrd ⊢ ω ≼ A ∧ ¬ B ∈ A → A ∖ B ≈ A
91 84 90 pm2.61dan ⊢ ω ≼ A → A ∖ B ≈ A