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 ( ω ≼ 𝐴 → ( 𝐴 ∖ { 𝐵 } ) ≈ 𝐴 )

Proof

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