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

Metamath Proof Explorer

Theorem infdiffi

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

Ref Expression
Assertion infdiffi ( ( ω ≼ 𝐴 ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∖ 𝐵 ) ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 difeq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ ∅ ) )
2 dif0 ⊢ ( 𝐴 ∖ ∅ ) = 𝐴
3 1 2 eqtrdi ⊢ ( 𝑥 = ∅ → ( 𝐴 ∖ 𝑥 ) = 𝐴 )
4 3 breq1d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ∖ 𝑥 ) ≈ 𝐴 ↔ 𝐴 ≈ 𝐴 ) )
5 4 imbi2d ⊢ ( 𝑥 = ∅ → ( ( ω ≼ 𝐴 → ( 𝐴 ∖ 𝑥 ) ≈ 𝐴 ) ↔ ( ω ≼ 𝐴 → 𝐴 ≈ 𝐴 ) ) )
6 difeq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝑦 ) )
7 6 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∖ 𝑥 ) ≈ 𝐴 ↔ ( 𝐴 ∖ 𝑦 ) ≈ 𝐴 ) )
8 7 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ω ≼ 𝐴 → ( 𝐴 ∖ 𝑥 ) ≈ 𝐴 ) ↔ ( ω ≼ 𝐴 → ( 𝐴 ∖ 𝑦 ) ≈ 𝐴 ) ) )
9 difeq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ ( 𝑦 ∪ { 𝑧 } ) ) )
10 difun1 ⊢ ( 𝐴 ∖ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( 𝐴 ∖ 𝑦 ) ∖ { 𝑧 } )
11 9 10 eqtrdi ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐴 ∖ 𝑥 ) = ( ( 𝐴 ∖ 𝑦 ) ∖ { 𝑧 } ) )
12 11 breq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐴 ∖ 𝑥 ) ≈ 𝐴 ↔ ( ( 𝐴 ∖ 𝑦 ) ∖ { 𝑧 } ) ≈ 𝐴 ) )
13 12 imbi2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ω ≼ 𝐴 → ( 𝐴 ∖ 𝑥 ) ≈ 𝐴 ) ↔ ( ω ≼ 𝐴 → ( ( 𝐴 ∖ 𝑦 ) ∖ { 𝑧 } ) ≈ 𝐴 ) ) )
14 difeq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝐵 ) )
15 14 breq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∖ 𝑥 ) ≈ 𝐴 ↔ ( 𝐴 ∖ 𝐵 ) ≈ 𝐴 ) )
16 15 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( ω ≼ 𝐴 → ( 𝐴 ∖ 𝑥 ) ≈ 𝐴 ) ↔ ( ω ≼ 𝐴 → ( 𝐴 ∖ 𝐵 ) ≈ 𝐴 ) ) )
17 reldom ⊢ Rel ≼
18 17 brrelex2i ⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
19 enrefg ⊢ ( 𝐴 ∈ V → 𝐴 ≈ 𝐴 )
20 18 19 syl ⊢ ( ω ≼ 𝐴 → 𝐴 ≈ 𝐴 )
21 domen2 ⊢ ( ( 𝐴 ∖ 𝑦 ) ≈ 𝐴 → ( ω ≼ ( 𝐴 ∖ 𝑦 ) ↔ ω ≼ 𝐴 ) )
22 21 biimparc ⊢ ( ( ω ≼ 𝐴 ∧ ( 𝐴 ∖ 𝑦 ) ≈ 𝐴 ) → ω ≼ ( 𝐴 ∖ 𝑦 ) )
23 infdifsn ⊢ ( ω ≼ ( 𝐴 ∖ 𝑦 ) → ( ( 𝐴 ∖ 𝑦 ) ∖ { 𝑧 } ) ≈ ( 𝐴 ∖ 𝑦 ) )
24 22 23 syl ⊢ ( ( ω ≼ 𝐴 ∧ ( 𝐴 ∖ 𝑦 ) ≈ 𝐴 ) → ( ( 𝐴 ∖ 𝑦 ) ∖ { 𝑧 } ) ≈ ( 𝐴 ∖ 𝑦 ) )
25 entr ⊢ ( ( ( ( 𝐴 ∖ 𝑦 ) ∖ { 𝑧 } ) ≈ ( 𝐴 ∖ 𝑦 ) ∧ ( 𝐴 ∖ 𝑦 ) ≈ 𝐴 ) → ( ( 𝐴 ∖ 𝑦 ) ∖ { 𝑧 } ) ≈ 𝐴 )
26 24 25 sylancom ⊢ ( ( ω ≼ 𝐴 ∧ ( 𝐴 ∖ 𝑦 ) ≈ 𝐴 ) → ( ( 𝐴 ∖ 𝑦 ) ∖ { 𝑧 } ) ≈ 𝐴 )
27 26 ex ⊢ ( ω ≼ 𝐴 → ( ( 𝐴 ∖ 𝑦 ) ≈ 𝐴 → ( ( 𝐴 ∖ 𝑦 ) ∖ { 𝑧 } ) ≈ 𝐴 ) )
28 27 a2i ⊢ ( ( ω ≼ 𝐴 → ( 𝐴 ∖ 𝑦 ) ≈ 𝐴 ) → ( ω ≼ 𝐴 → ( ( 𝐴 ∖ 𝑦 ) ∖ { 𝑧 } ) ≈ 𝐴 ) )
29 28 a1i ⊢ ( 𝑦 ∈ Fin → ( ( ω ≼ 𝐴 → ( 𝐴 ∖ 𝑦 ) ≈ 𝐴 ) → ( ω ≼ 𝐴 → ( ( 𝐴 ∖ 𝑦 ) ∖ { 𝑧 } ) ≈ 𝐴 ) ) )
30 5 8 13 16 20 29 findcard2 ⊢ ( 𝐵 ∈ Fin → ( ω ≼ 𝐴 → ( 𝐴 ∖ 𝐵 ) ≈ 𝐴 ) )
31 30 impcom ⊢ ( ( ω ≼ 𝐴 ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∖ 𝐵 ) ≈ 𝐴 )