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→∃ff:ω⟶1-1A
2 1 adantr ⊢ω≼A∧B∈A→∃ff:ω⟶1-1A
3 reldom ⊢Rel⁡≼
4 3 brrelex2i ⊢ω≼A→A∈V
5 4 ad2antrr ⊢ω≼A∧B∈A∧f:ω⟶1-1A→A∈V
6 simplr ⊢ω≼A∧B∈A∧f:ω⟶1-1A→B∈A
7 f1f ⊢f:ω⟶1-1A→f:ω⟶A
8 7 adantl ⊢ω≼A∧B∈A∧f:ω⟶1-1A→f:ω⟶A
9 peano1 ⊢∅∈ω
10 ffvelcdm ⊢f:ω⟶A∧∅∈ω→f⁡∅∈A
11 8 9 10 sylancl ⊢ω≼A∧B∈A∧f:ω⟶1-1A→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-1A→A∖B≈A∖f⁡∅
14 vex ⊢f∈V
15 f1f1orn ⊢f:ω⟶1-1A→f:ω⟶1-1 ontoran⁡f
16 15 adantl ⊢ω≼A∧B∈A∧f:ω⟶1-1A→f:ω⟶1-1 ontoran⁡f
17 f1oen3g ⊢f∈V∧f:ω⟶1-1 ontoran⁡f→ω≈ran⁡f
18 14 16 17 sylancr ⊢ω≼A∧B∈A∧f:ω⟶1-1A→ω≈ran⁡f
19 18 ensymd ⊢ω≼A∧B∈A∧f:ω⟶1-1A→ran⁡f≈ω
20 3 brrelex1i ⊢ω≼A→ω∈V
21 20 ad2antrr ⊢ω≼A∧B∈A∧f:ω⟶1-1A→ω∈V
22 limom ⊢Lim⁡ω
23 22 limenpsi ⊢ω∈V→ω≈ω∖∅
24 21 23 syl ⊢ω≼A∧B∈A∧f:ω⟶1-1A→ω≈ω∖∅
25 14 resex ⊢f↾ω∖∅∈V
26 simpr ⊢ω≼A∧B∈A∧f:ω⟶1-1A→f:ω⟶1-1A
27 difss ⊢ω∖∅⊆ω
28 f1ores ⊢f:ω⟶1-1A∧ω∖∅⊆ω→f↾ω∖∅:ω∖∅⟶1-1 ontofω∖∅
29 26 27 28 sylancl ⊢ω≼A∧B∈A∧f:ω⟶1-1A→f↾ω∖∅:ω∖∅⟶1-1 ontofω∖∅
30 f1oen3g ⊢f↾ω∖∅∈V∧f↾ω∖∅:ω∖∅⟶1-1 ontofω∖∅→ω∖∅≈fω∖∅
31 25 29 30 sylancr ⊢ω≼A∧B∈A∧f:ω⟶1-1A→ω∖∅≈fω∖∅
32 f1orn ⊢f:ω⟶1-1 ontoran⁡f↔fFnω∧Fun⁡f-1
33 32 simprbi ⊢f:ω⟶1-1 ontoran⁡f→Fun⁡f-1
34 imadif ⊢Fun⁡f-1→fω∖∅=fω∖f∅
35 16 33 34 3syl ⊢ω≼A∧B∈A∧f:ω⟶1-1A→fω∖∅=fω∖f∅
36 f1fn ⊢f:ω⟶1-1A→fFnω
37 36 adantl ⊢ω≼A∧B∈A∧f:ω⟶1-1A→fFnω
38 fnima ⊢fFnω→fω=ran⁡f
39 37 38 syl ⊢ω≼A∧B∈A∧f:ω⟶1-1A→fω=ran⁡f
40 fnsnfv ⊢fFnω∧∅∈ω→f⁡∅=f∅
41 37 9 40 sylancl ⊢ω≼A∧B∈A∧f:ω⟶1-1A→f⁡∅=f∅
42 41 eqcomd ⊢ω≼A∧B∈A∧f:ω⟶1-1A→f∅=f⁡∅
43 39 42 difeq12d ⊢ω≼A∧B∈A∧f:ω⟶1-1A→fω∖f∅=ran⁡f∖f⁡∅
44 35 43 eqtrd ⊢ω≼A∧B∈A∧f:ω⟶1-1A→fω∖∅=ran⁡f∖f⁡∅
45 31 44 breqtrd ⊢ω≼A∧B∈A∧f:ω⟶1-1A→ω∖∅≈ran⁡f∖f⁡∅
46 entr ⊢ω≈ω∖∅∧ω∖∅≈ran⁡f∖f⁡∅→ω≈ran⁡f∖f⁡∅
47 24 45 46 syl2anc ⊢ω≼A∧B∈A∧f:ω⟶1-1A→ω≈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-1A→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-1A→A∖ran⁡f≈A∖ran⁡f
53 disjdif ⊢ran⁡f∩A∖ran⁡f=∅
54 53 a1i ⊢ω≼A∧B∈A∧f:ω⟶1-1A→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-1A→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-1A→ran⁡f∪A∖ran⁡f≈ran⁡f∖f⁡∅∪A∖ran⁡f
63 8 frnd ⊢ω≼A∧B∈A∧f:ω⟶1-1A→ran⁡f⊆A
64 undif ⊢ran⁡f⊆A↔ran⁡f∪A∖ran⁡f=A
65 63 64 sylib ⊢ω≼A∧B∈A∧f:ω⟶1-1A→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 ⊢fFnω∧∅∈ω→f⁡∅∈ran⁡f
69 37 9 68 sylancl ⊢ω≼A∧B∈A∧f:ω⟶1-1A→f⁡∅∈ran⁡f
70 67 69 nsyl3 ⊢ω≼A∧B∈A∧f:ω⟶1-1A→¬f⁡∅∈A∖ran⁡f
71 disjsn ⊢A∖ran⁡f∩f⁡∅=∅↔¬f⁡∅∈A∖ran⁡f
72 70 71 sylibr ⊢ω≼A∧B∈A∧f:ω⟶1-1A→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-1A→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 eqtrid ⊢ω≼A∧B∈A∧f:ω⟶1-1A→A∖ran⁡f∪ran⁡f=A
77 76 difeq1d ⊢ω≼A∧B∈A∧f:ω⟶1-1A→A∖ran⁡f∪ran⁡f∖f⁡∅=A∖f⁡∅
78 74 77 eqtrd ⊢ω≼A∧B∈A∧f:ω⟶1-1A→A∖ran⁡f∪ran⁡f∖f⁡∅=A∖f⁡∅
79 66 78 eqtrid ⊢ω≼A∧B∈A∧f:ω⟶1-1A→ran⁡f∖f⁡∅∪A∖ran⁡f=A∖f⁡∅
80 62 65 79 3brtr3d ⊢ω≼A∧B∈A∧f:ω⟶1-1A→A≈A∖f⁡∅
81 80 ensymd ⊢ω≼A∧B∈A∧f:ω⟶1-1A→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-1A→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